(* 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_lem25.v                                *)
(****************************************************************************)

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

Theorem Lem10 :
 forall d : D,
 seq (ia frame c6 (tuple e1)) (X1 d) =
 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)))))).

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia D s4 d) (Y2 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))) *)
elim EXPH4.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt (enc H (Lmer (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 (seq (ia frame s6 sce) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (K i) (mer (seq (ia frame s6 sce) (L i)) (mer (R 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 (seq (ia frame s6 sce) (L i)) (mer (R i) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (R i)))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (R i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim Lmers6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt (enc H (Lmer (R i) (mer (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 (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (R i)))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (R i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
pattern (R i) at 1 3 4 5 in |- *.
(* Goal: (fun p : proc => @eq proc (seq (ia Frame c2 (Tuple e1 d)) (enc H (mer (seq (Tn_d d e1) (S i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (seq (Rn e0) (R i))))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (seq (Rn e0) p) (mer (seq (Sn_d d e1) (S i)) (mer (K i) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) p)) (mer (seq (Sn_d d e1) (S i)) (K i)))) (alt (enc H (Lmer (comm (K i) (L i)) (mer (seq (Sn_d d e1) (S i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) p)) (mer (seq (Sn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (seq (Rn e0) p)) (mer (K i) (L i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_dK.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) Delta))))))))) *)
elim CommKRn.
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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim CommKs6.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim CommRns6.
(* Goal: @eq proc (seq (ia frame c6 (tuple e1)) (X1 d)) (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 s6 (tuple e1)) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
pattern e1 at 1 2 in |- *.
(* Goal: (fun b : bit => @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))))))))))) e1 *)
elimtype (toggle e0 = e1).
(* Goal: @eq proc (seq (ia frame c6 (tuple (toggle e0))) (X1 d)) (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 s6 (tuple (toggle e0))) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
(* Goal: @eq bit (toggle e0) e1 *)
elim CommTn_ds6_b.

(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (seq (ia frame c6 sce) (enc H (mer (L i) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (K i)))))) *)
unfold X1 in |- *.
elim
 (SC6 (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (K i))) (L i)).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (mer (K i) (mer (L i) (R i))) (mer (R i) (mer (K i) (L i))) *)
elim (SC6 (mer (K i) (L i)) (R i)).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
(* Goal: @eq bit (toggle e0) e1 *)
elim Toggle1.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

Theorem Lem11 :
 forall d : D,
 seq (ia frame c6 sce) (X1 d) =
 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)))))).

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia D s4 d) (Y2 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))) *)
elim EXPH4.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt (enc H (Lmer (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 (seq (ia frame s6 sce) (L i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i))))))) (alt (enc H (Lmer (K i) (mer (seq (ia frame s6 sce) (L i)) (mer (R 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 (seq (ia frame s6 sce) (L i)) (mer (R i) (K i))))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (R i)))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (R i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim Lmers6.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerTnd.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt (enc H (Lmer (R i) (mer (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 (enc H (Lmer (comm (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (R i)))) (alt (enc H (Lmer (comm (R i) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (R i)) (mer (K i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
pattern (R i) at 1 3 4 5 in |- *.
(* Goal: (fun p : proc => @eq proc (seq (ia Frame c2 (Tuple e1 d)) (enc H (mer (seq (Tn_d d e1) (S i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (seq (Rn e0) (R i))))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (seq (Rn e0) p) (mer (seq (Sn_d d e1) (S i)) (mer (K i) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) p)) (mer (seq (Sn_d d e1) (S i)) (K i)))) (alt (enc H (Lmer (comm (K i) (L i)) (mer (seq (Sn_d d e1) (S i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) p)) (mer (seq (Sn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (K i)) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (L i)) (mer (K i) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Sn_d d e1) (S i)) (seq (Rn e0) p)) (mer (K i) (L i)))))))))))))) (R i) *)
elim ProcR.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt Delta (alt Delta (alt Delta Delta))))))))) *)
elim CommTn_dK.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (K i)) (mer (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Rn e1) (seq (Rn e0) (R i))) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (seq (ia frame s6 sce) (L i)) (K i)))) (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) Delta))))))))) *)
elim CommKRn.
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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (K i)) (mer (R i) (seq (Tn_d d e0) (seq (Sn e1) (S i)))))) (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim CommKs6.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (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 (enc H (Lmer (comm (seq (ia frame s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim CommRns6.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (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 s6 sce) (L i)) (seq (Tn_d d e0) (seq (Sn e1) (S i)))) (mer (R i) (K i))))))))))))) *)
elim CommTn_ds6_sce.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (seq (ia frame c6 sce) (X1 d)) (seq (ia frame c6 sce) (enc H (mer (L i) (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (K i)))))) *)
unfold X1 in |- *.
elim
 (SC6 (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (K i))) (L i)).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (seq (ia frame c6 sce) (enc H (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (K i) (mer (L i) (R i)))))) (seq (ia frame c6 sce) (enc H (mer (seq (Sn_d d e0) (seq (Sn e1) (S i))) (mer (R i) (mer (K i) (L i)))))) *)
elimtype (mer (K i) (mer (L i) (R i)) = mer (R i) (mer (K i) (L i))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
(* Goal: @eq proc (mer (K i) (mer (L i) (R i))) (mer (R i) (mer (K i) (L i))) *)
elim (SC6 (mer (K i) (L i)) (R i)).
(* Goal: @eq proc (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim SC7.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

Theorem Lem12 :
 forall d : D,
 seq (ia Frame c2 (Tuple e0 d))
   (alt
      (seq (ia one int i)
         (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d))))
      (seq (ia one int i)
         (seq (ia Frame c3 lce)
            (seq (ia frame c5 (tuple e1))
               (seq
                  (alt (seq (ia one int i) (ia frame c6 (tuple e1)))
                     (seq (ia one int i) (ia frame c6 sce))) 
                  (X1 d)))))) = X1 d.
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (X1 d) *)
pattern (X1 d) at 2 in |- *.
(* Goal: (fun p : proc => @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) p) (X1 d) *)
elim Lem3.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 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)))))) *)
elim Lem4.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 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)))))))) *)
elim Lem5.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 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) (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))))))))) *)
elim Lem6.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int 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))))))) (seq (ia one int i) (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))))))))) *)
elim Lem7.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (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))))))))) *)
elim Lem8.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (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)))))))))))) *)
elim Lem9.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (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)))))))))))))) *)
elim Lem10.
(* Goal: @eq proc (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (seq (alt (seq (ia one int i) (ia frame c6 (tuple e1))) (seq (ia one int i) (ia frame c6 sce))) (X1 d))))))) (seq (ia Frame c2 (Tuple e0 d)) (alt (seq (ia one int i) (seq (ia Frame c3 (Tuple e0 d)) (seq (ia D s4 d) (X2 d)))) (seq (ia one int i) (seq (ia Frame c3 lce) (seq (ia frame c5 (tuple e1)) (alt (seq (ia one int i) (seq (ia frame c6 (tuple e1)) (X1 d))) (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)))))))))))))) *)
elim Lem11.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt (enc H (Lmer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt Delta (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (Tn_d d e1) (S i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 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 e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e0)) (Rn e0)) (R i)) (mer (seq (Tn_d d 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e0)) (Rn e0)) (R i)) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim A5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

Theorem Lem13 :
 forall d : D,
 seq (ia Frame c2 (Tuple e1 d))
   (enc H
      (mer (seq (Tn_d d e1) (S i))
         (mer
            (seq
               (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d)))
                  (seq (ia one int i) (ia Frame s3 lce))) 
               (K i)) (mer (L i) (seq (Rn e0) (R i)))))) = 
 Y1 d.

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

Theorem Lem14 :
 forall d : D,
 alt
   (seq (ia one int i)
      (enc H
         (mer (seq (ia Frame s3 (Tuple e1 d)) (K i))
            (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))
   (seq (ia one int i)
      (enc H
         (mer (seq (ia Frame s3 lce) (K i))
            (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) =
 enc H
   (mer (seq (Tn_d d e1) (S i))
      (mer
         (seq
            (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d)))
               (seq (ia one int i) (ia Frame s3 lce))) 
            (K i)) (mer (L i) (seq (Rn e0) (R i))))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))) (enc H (mer (seq (Tn_d d e1) (S i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (L i) (seq (Rn e0) (R i)))))) *)
elim (EXPH4 (seq (Tn_d d e1) (S i))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (K i) (mer (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 frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt (enc H (Lmer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt Delta (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (Tn_d d e1) (S i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 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 e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 d))) (seq (ia one int i) (ia Frame s3 lce))) (K i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (alt (seq (ia one int i) (ia Frame s3 (Tuple e1 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e0)) (Rn e0)) (R i)) (mer (seq (Tn_d d 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e0)) (Rn e0)) (R i)) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim A5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))))) (seq (ia one int i) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))))) (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e1 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e1 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e1 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i))))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e1 d)) (K i))) (seq (ia one int i) (seq (ia Frame s3 lce) (K i)))) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia Frame s3 (Tuple e1 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Rn e0) (R i))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt Delta Delta))))))))) *)
elim CommiRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (seq (Rn e0) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

Theorem Lem15 :
 forall d : D,
 seq (ia Frame c3 lce)
   (enc H
      (mer (K i)
         (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))
            (mer (seq (Tn_d d e1) (S i)) (L i))))) =
 enc H
   (mer (seq (ia Frame s3 lce) (K i))
      (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (enc H (mer (seq (ia Frame s3 lce) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) *)
elim (EXPH4 (seq (ia Frame s3 lce) (K i))).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (alt (enc H (Lmer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (L i) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim Lmers3.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (K i) (mer (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 frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim Comms3Tn_d.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d 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 e0) (R i))) (mer (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e1)) (R i)) (mer (mer (K i) (seq (Tn_d d e1) (S i))) (L i))))) (seq (ia D s4 d) (enc H (mer (seq (ia frame s5 (tuple e1)) (R i)) (mer (K i) (mer (seq (Tn_d d 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 e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (seq (ia Frame c3 lce) (enc H (mer (K i) (mer (seq (seq (ia frame s5 (tuple e0)) (Rn e0)) (R i)) (mer (seq (Tn_d d e1) (S i)) (L i)))))) *)
elim A5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

 
Theorem Lem16 :
 forall d : D,
 seq (ia Frame c3 (Tuple e1 d))
   (enc H
      (mer (K i)
         (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i)))
            (mer (seq (Tn_d d e1) (S i)) (L i))))) =
 enc H
   (mer (seq (ia Frame s3 (Tuple e1 d)) (K i))
      (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i))))).
(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (enc H (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) *)
elim (EXPH4 (seq (ia Frame s3 (Tuple e1 d)) (K i))).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (alt (enc H (Lmer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (L i) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (L i) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim Lmers3.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (K i) (mer (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 frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (L i) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim CommLRn.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e1 d)) (K i)) (seq (Tn_d d e1) (S i))) (mer (L i) (seq (Rn e0) (R i))))) (alt (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim Comms3Tn_d.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e1 d)) (K i)) (L i)) (mer (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))))) (enc H (Lmer (comm (seq (ia Frame s3 (Tuple e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
elim Comms3L.
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e1 d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
pattern e1 at 4 in |- *.
(* Goal: (fun b : bit => @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i)))))))))))))) e1 *)
elimtype (toggle e0 = e1).
(* Goal: @eq proc (seq (ia Frame c3 (Tuple e1 d)) (enc H (mer (K i) (mer (seq (ia D s4 d) (seq (ia frame s5 (tuple e1)) (R i))) (mer (seq (Tn_d d 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 e0) d)) (K i)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))))))))))) *)
(* Goal: @eq bit (toggle e0) e1 *)
elim Comms3Rn_b.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq bit (toggle e0) e1 *)
elim Toggle1.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
(* Goal: @eq bit (toggle e0) e1 *)
elim Toggle1.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

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

Theorem Lem18 :
 forall d : D,
 seq (ia frame c5 (tuple e0))
   (enc H
      (mer (seq (Rn e0) (R i))
         (mer
            (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i)))
               (seq (ia one int i) (seq (ia frame s6 sce) (L i))))
            (mer (K i) (seq (Tn_d d e1) (S i)))))) =
 enc H
   (mer (K i)
      (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))
         (mer (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (enc H (mer (K i) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (seq (Tn_d d e1) (S i)) (L i))))) *)
elim (EXPH4 (K i)).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (K i) (mer (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 frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim LmerL.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (mer (K i) (mer (seq (Tn_d d e1) (S i)) (L i))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (K i) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i))))) (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim Lmers5.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (L i)) (mer (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommTn_dL.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i))) (mer (K i) (L i)))) (alt (enc H (Lmer (comm (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommTn_ds5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d 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 e0)) (seq (Rn e0) (R i))) (L i)) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommLs5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt (enc H (Lmer (comm (K i) (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i)))) (mer (seq (Tn_d d e1) (S i)) (L i)))) (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommKs5.
(* Goal: @eq proc (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt Delta (alt (seq (ia frame c5 (tuple e0)) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i))))))) (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (L i)))) (enc H (Lmer (comm (K i) (L i)) (mer (seq (ia frame s5 (tuple e0)) (seq (Rn e0) (R i))) (seq (Tn_d d e1) (S i)))))))))))))) *)
elim CommKL.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.

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

(* Goal: forall d : D, @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
intros.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (enc H (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) *)
elim (EXPH4 (seq (Rn e0) (R i))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (K i) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i)))))) (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (enc H (Lmer (seq (Tn_d d e1) (S i)) (mer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (enc H (Lmer (seq (Rn e0) (R i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (mer (K i) (seq (Tn_d d e1) (S i)))))) (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim LmerRn.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i))))))))))))) *)
elim (SC3 (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (K i)) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) Delta))))))))) *)
elim (SC3 (seq (Rn e0) (R i)) (K i)).
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (K i) (seq (Rn e0) (R i))) (mer (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))))) Delta))))))))) *)
elim CommKRn.
elim
 (SC3 (seq (Rn e0) (R i))
    (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (K i)))) (alt (enc H (Lmer (comm (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (seq (Rn e0) (R i))) (mer (K i) (seq (Tn_d d e1) (S i))))) (alt Delta Delta))))))))) *)
elim CommiRn.
elim
 (SC3
    (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i)))
       (seq (ia one int i) (seq (ia frame s6 sce) (L i))))
    (seq (Tn_d d e1) (S i))).
 
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d e1) (S i))))) (alt (enc H (Lmer (comm (seq (Tn_d d e1) (S i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i))))) (mer (seq (Rn e0) (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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt Delta (alt (enc H (Lmer (comm (K i) (seq (Tn_d d e1) (S i))) (mer (seq (Rn e0) (R i)) (alt (seq (ia one int i) (seq (ia frame s6 (tuple e0)) (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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i))) (seq (ia one int i) (seq (ia frame s6 sce) (L i)))) (K i)) (mer (seq (Rn e0) (R i)) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d 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 e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt Delta (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))))) *)
repeat elim A6'.
(* Goal: @eq proc (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) (alt (seq (ia one int i) (enc H (mer (seq (ia frame s6 (tuple e0)) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i))))))) (seq (ia one int i) (enc H (mer (seq (ia frame s6 sce) (L i)) (mer (seq (Rn e0) (R i)) (mer (K i) (seq (Tn_d d e1) (S i)))))))) *)
apply refl_equal.
Qed.
