(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(* This contribution was updated for Coq V5.10 by the COQ workgroup.        *)
(* January 1995                                                             *)
(****************************************************************************)
(*                                                                          *)
(*      Coq V5.8                                                            *)
(*                                                                          *)
(*                                                                          *)
(*      Alternating Bit Protocol                                            *)
(*                                                                          *)
(*      Jan Friso Groote                                                    *)
(*      Utrecht University                                                  *)
(*                                                                          *)
(*      November 1992                                                       *)
(*                                                                          *)
(* From bezem@phil.ruu.nl Fri Apr  2 13:14:31 1993                          *)
(*                                                                          *)
(****************************************************************************)
(*                                abp_lem2.v                                *)
(****************************************************************************)

Require Import abp_base.
Require Import abp_defs.
Require Import abp_lem1.

Theorem Lem1 : D + (fun d : D => seq (ia D r1 d) (X1 d)) = X.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (X1 d))) X *)
unfold X at 1 in |- *.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (X1 d))) (enc H (mer (S i) (mer (K i) (mer (L i) (R i))))) *)
elim ProcS; elim ProcR.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) *)
elim EXPH4.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (enc H (Lmer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (K i) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (L i) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)))) (alt (enc H (Lmer (comm (K i) (L i)) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) (R i))) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim LmerSn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) Delta))))))))) *)
elim CommKRn.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnK.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnL.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
elim
 (A6
    (D +
     (fun d : D =>
      seq (ia D r1 d)
        (enc H
           (mer (seq (Sn_d d e0) (seq (Sn e1) (S i)))
              (mer (K i) (mer (L i) (seq (Rn e1) (seq (Rn e0) (R i)))))))))).
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (X1 d))) (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (seq (Rn e1) (seq (Rn e0) (R i))))))))) *)
unfold X1 in |- *.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
pattern (R i) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.


Theorem Lem2 : D + (fun d : D => seq (ia D r1 d) (Y1 d)) = Y.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) Y *)
unfold Y in |- *.
(* Goal: (fun p : proc => @eq proc (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) p) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i))))))))) (S i) *)
elim ProcS.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) *)
elim EXPH4.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (enc H (Lmer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (K i) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (L i) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)))) (alt (enc H (Lmer (comm (K i) (L i)) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) (R i))) (mer (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim LmerSn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) Delta))))))))) *)
elim CommKRn.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnK.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnL.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (alt (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (Sn e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (seq (Rn e0) (R i))) (mer (K i) (L i))))))))))))) *)
elim CommSnRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
elim
 (A6
    (D +
     (fun d : D =>
      seq (ia D r1 d)
        (enc H
           (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i))))
              (mer (K i) (mer (L i) (seq (Rn e0) (R i))))))))).

(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (Y1 d))) (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) *)
unfold Y1 in |- *.
(* Goal: @eq proc (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (S i)) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) *)
pattern (S i) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) p) (mer (K i) (mer (L i) (seq (Rn e0) (R i)))))))) (sum D (fun d : D => seq (ia D r1 d) (enc H (mer (seq (Sn_d d e1) (seq (Sn e0) (seq (Sn e1) (S i)))) (mer (K i) (mer (L i) (seq (Rn e0) (R i))))))))) (S i) *)
elim ProcS.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.


Theorem Lem3 :
 forall d : D,
 seq (ia Frame c2 (Tuple e0 d))
   (enc H
      (mer (seq (Tn_d d e0) (seq (Sn e1) (S i)))
         (mer
            (seq
               (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d)))
                  (seq (ia one int i) (ia Frame s3 lce))) 
               (K i)) (mer (L i) (R i))))) = X1 d.
(* Goal: forall d : D, @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (X1 d) *)
intro.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (X1 d) *)
unfold X1 at 1 in |- *.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (enc H (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (R i))))) *)
elim (EXPH4 (seq (Sn_d d e0) (seq (Sn e1) (S i))) (K i) (L i) (R i) H).
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (alt (enc H (Lmer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (R i))))) (alt (enc H (Lmer (K i) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))) (alt (enc H (Lmer (L i) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (R i))))) (alt (enc H (Lmer (R i) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (K i)))) (alt (enc H (Lmer (comm (K i) (L i)) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (R i)))) (alt (enc H (Lmer (comm (K i) (R i)) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (K i)) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (R i)))) (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (K i) (L i))))))))))))) *)
elim LmerSnd.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (R i) (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (ia Frame s3 lce) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 lce) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (ia Frame s3 lce) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
pattern (R i) at 2 3 5 8 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) Delta))))))))) *)
elim CommKRn.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (K i)) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (R i)))) (enc H (Lmer (comm (seq (Sn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (K i) (L i))))))))))))) *)
elim ProcSn_d.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim A5.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (K i)) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (R i)))) (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (K i) (L i))))))))))))) *)
elim Comms2K.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))) (mer (L i) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (R i)))) (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (K i) (L i))))))))))))) *)
elim Comms2Rn.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (R i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia Frame c2 (Tuple e0 d)) (enc H (mer (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))) (mer (L i) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s2 (Tuple e0 d)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i)) (mer (K i) (R i)))) Delta))))))))) *)
elim Comms2L.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem4 :
 forall d : D,
 alt
   (seq (ia one int i)
      (enc H
         (mer (seq (ia Frame s3 (Tuple e0 d)) (K i))
            (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))
   (seq (ia one int i)
      (enc H
         (mer (seq (ia Frame s3 lce) (K i))
            (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) =
 enc H
   (mer (seq (Tn_d d e0) (seq (Sn e1) (S i)))
      (mer
         (seq
            (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d)))
               (seq (ia one int i) (ia Frame s3 lce))) 
            (K i)) (mer (L i) (R i)))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros. 
elim
 (EXPH4 (seq (Tn_d d e0) (seq (Sn e1) (S i)))
    (seq
       (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d)))
          (seq (ia one int i) (ia Frame s3 lce))) (K i)) 
    (L i) (R i)).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))) (alt Delta (alt (enc H (Lmer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))) (alt Delta (alt (enc H (Lmer (R i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))))) (alt (enc H (Lmer (comm (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (alt (enc H (Lmer (comm (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (R i)))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e0 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i))))))))))))) *)
elim A4.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim A5.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim A5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim Lmeri.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))) (alt Delta (alt (enc H (Lmer (R i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i))))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (R i)))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i))))))))))))) *)
pattern (R i) at 5 6 8 11 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i))))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (R i)))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e0 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i))))))))))))) *)
elim CommiL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta Delta))))))))) *)
elim CommiRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (R i) (K i)))) (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_di.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim CommTn_dRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem5 :
 forall d : D,
 seq (ia Frame c3 lce)
   (enc H
      (mer (K i)
         (mer (seq (ia frame s5 (tuple e1)) (R i))
            (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) =
 enc H
   (mer (seq (ia Frame s3 lce) (K i))
      (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros.
elim
 (EXPH4 (seq (ia Frame s3 lce) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))
    (L i) (R i)).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt (enc H (Lmer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (L i) (R i))))) (alt (enc H (Lmer (L i) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i))))) (alt (enc H (Lmer (R i) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Lmers3.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (R i) (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (ia Frame s3 lce) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 lce) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (ia Frame s3 lce) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
pattern (R i) at 2 3 5 8 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim CommTn_dRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Comms3Tn_d.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Comms3L.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (ia Frame s3 lce) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Comms3Rn_lce.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
pattern (R i) at 1 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e1)) (Rn e1)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim A5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem6 :
 forall d : D,
 seq (ia Frame c3 (Tuple e0 d))
   (enc H
      (mer (K i)
         (mer
            (seq (ia D s4 d)
               (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))
            (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) =
 enc H
   (mer (seq (ia Frame s3 (Tuple e0 d)) (K i))
      (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i)))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros.
elim
 (EXPH4 (seq (ia Frame s3 (Tuple e0 d)) (K i))
    (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i) (R i)).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt (enc H (Lmer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (L i) (R i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (L i) (R i))))) (alt (enc H (Lmer (L i) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i))))) (alt (enc H (Lmer (R i) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Lmers3.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (R i) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (comm (L i) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
pattern (R i) at 1 2 3 5 8 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (R i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim CommTn_dRn.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (L i) (R i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Comms3Tn_d.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (L i)) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (R i)))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
elim Comms3L.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e0 d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
pattern e0 at 6 in |- *.
(* Goal: (fun b : bit => @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (ia Frame s3 (Tuple b d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))))))))))) e0 *)
elimtype (toggle e1 = e0).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (enc H (Lmer (comm (seq (ia Frame s3 (Tuple (toggle e1) d)) (K i)) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))))))))))) *)
(* Goal: @eq bit (toggle e1) e0 *)
elim Comms3Rn_b.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq bit (toggle e1) e0 *)
elim Toggle2.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (seq (Rn e1) (seq (Rn e0) (R i)))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (seq (ia Frame c3 (Tuple e0 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
(* Goal: @eq bit (toggle e1) e0 *)
pattern (R i) at 2 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
(* Goal: @eq bit (toggle e1) e0 *)
elim Toggle2.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem7 :
 forall d : D,
 seq (ia D s4 d) (X2 d) =
 enc H
   (mer (K i)
      (mer
         (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))
         (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))).

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) *)
elim EXPH4.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (alt Delta (alt (enc H (Lmer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))))) (alt (enc H (Lmer (comm (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim Lmers4.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (alt Delta (alt (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_ds4.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (alt Delta (alt (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommLs4.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (alt Delta (alt (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKs4.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_dK.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (seq (ia D s4 d) (X2 d)) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
unfold X2 in |- *.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim (SC6 (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)).
elim
 (SC6 (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (K i)).
elim
 (SC6
    (mer (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (K i))
    (seq (Tn_d d e0) (seq (Sn e1) (S i)))).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (L i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim (SC6 (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i)).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem8 :
 forall d : D,
 seq (ia frame c5 (tuple e1))
   (enc H
      (mer (R i)
         (mer
            (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i)))
               (seq (ia one int i) (seq (ia frame s6 sce) (L i))))
            (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) =
 enc H
   (mer (K i)
      (mer (seq (ia frame s5 (tuple e1)) (R i))
         (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))).

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros.
elim
 (EXPH4 (K i) (seq (ia frame s5 (tuple e1)) (R i))
    (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt (enc H (Lmer (L i) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i))))) (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim Lmers5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)) (mer (K i) (seq (ia frame s5 (tuple e1)) (R i))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommTn_ds5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e1)) (R i)) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommLs5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKs5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e1)) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s5 (tuple e1)) (R i)) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e1)) (R i)) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_dK.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.

Theorem Lem9 :
 forall d : D,
 alt
   (seq (ia one int i)
      (enc H
         (mer (seq (ia frame s6 (tuple e1)) (L i))
            (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))
   (seq (ia one int i)
      (enc H
         (mer (seq (ia frame s6 sce) (L i))
            (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) =
 enc H
   (mer (R i)
      (mer
         (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i)))
            (seq (ia one int i) (seq (ia frame s6 sce) (L i))))
         (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))).

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (enc H (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) *)
intros.
elim
 (EXPH4 (R i)
    (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i)))
       (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) 
    (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim Lmeri.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (K i) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerK.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (R i) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
pattern (R i) at 3 9 10 11 in |- *.
(* Goal: (fun p : proc => @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer p (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm p (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm p (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm p (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (enc H (Lmer (seq (Rn e1) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
elim
 (SC3 (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim CommTn_dRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) Delta))))))))) *)
elim (SC3 (seq (Rn e1) (seq (Rn e0) (R i))) (K i)).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) Delta))))))))) *)
elim CommKRn.
elim
 (SC3 (seq (Rn e1) (seq (Rn e0) (R i)))
    (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i)))
       (seq (ia one int i) (seq (ia frame s6 sce) (L i))))).

(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Rn e1) (seq (Rn e0) (R i)))) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta Delta))))))))) *)
elim CommiRn.
elim
 (SC3
    (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i)))
       (seq (ia one int i) (seq (ia frame s6 sce) (L i))))
    (seq (Tn_d d e0) (seq (Sn e1) (S i)))).

(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e0) (seq (Sn e1) (S i))) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (R i) (K i)))) (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_di.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_dK.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e1)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommiK.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta Delta))))))))) *)
repeat elim A6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e1)) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (R i) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))))) *)
apply refl_equal.
Qed.
