(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_3_3.ma".
+include "ground_2/xoa/ex_4_3.ma".
+include "ground_2/xoa/ex_5_5.ma".
+include "ground_2/xoa/ex_5_6.ma".
+include "ground_2/xoa/ex_6_5.ma".
+include "ground_2/xoa/ex_7_6.ma".
include "static_2/notation/relations/lrsubeqf_4.ma".
include "ground_2/relocation/nstream_sor.ma".
include "static_2/static/frees.ma".
āf1,f2,L1,L2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦ ā
āg1,I,K1,X. f1 = āg1 ā L1 = K1.ā{I}X ā
āØāØ āāg2,K2. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f2 = āg2 & L2 = K2.ā{I}X
- | āāg,g0,g2,K2,W,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g2,K2,W,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Vā¦ ā g & g0 ā g ā g1 & f2 = āg2 &
I = Abbr & X = āW.V & L2 = K2.āW
- | āāg,g0,g2,J,K2. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g2,J,K2. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Xā¦ ā g & g0 ā g ā g1 & f2 = āg2 & L2 = K2.ā¤{J}.
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g1 #J #K1 #X #_ #H destruct
lemma lsubf_inv_pair1:
āg1,f2,I,K1,L2,X. ā¦K1.ā{I}X,āg1ā¦ ā«š
+ ā¦L2,f2ā¦ ā
āØāØ āāg2,K2. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f2 = āg2 & L2 = K2.ā{I}X
- | āāg,g0,g2,K2,W,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g2,K2,W,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Vā¦ ā g & g0 ā g ā g1 & f2 = āg2 &
I = Abbr & X = āW.V & L2 = K2.āW
- | āāg,g0,g2,J,K2. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g2,J,K2. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Xā¦ ā g & g0 ā g ā g1 & f2 = āg2 & L2 = K2.ā¤{J}.
/2 width=5 by lsubf_inv_pair1_aux/ qed-.
āf1,f2,L1,L2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦ ā
āg2,I,K2. f2 = āg2 ā L2 = K2.ā¤{I} ā
āØāØ āāg1,K1. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f1 = āg1 & L1 = K1.ā¤{I}
- | āāg,g0,g1,J,K1,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g1,J,K1,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Vā¦ ā g & g0 ā g ā g1 & f1 = āg1 & L1 = K1.ā{J}V.
#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
[ #f1 #f2 #_ #g2 #J #K2 #_ #H destruct
lemma lsubf_inv_unit2:
āf1,g2,I,L1,K2. ā¦L1,f1ā¦ ā«š
+ ā¦K2.ā¤{I},āg2ā¦ ā
āØāØ āāg1,K1. ā¦K1,g1ā¦ ā«š
+ ā¦K2,g2ā¦ & f1 = āg1 & L1 = K1.ā¤{I}
- | āāg,g0,g1,J,K1,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
+ | āāg,g0,g1,J,K1,V. ā¦K1,g0ā¦ ā«š
+ ā¦K2,g2ā¦ &
K1 ā¢ š
+ā¦Vā¦ ā g & g0 ā g ā g1 & f1 = āg1 & L1 = K1.ā{J}V.
/2 width=5 by lsubf_inv_unit2_aux/ qed-.
(* Basic properties *********************************************************)
-axiom lsubf_eq_repl_back1: āf2,L1,L2. eq_repl_back ā¦ (Ī»f1. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
+lemma lsubf_eq_repl_back1: āf2,L1,L2. eq_repl_back ā¦ (Ī»f1. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
+#f2 #L1 #L2 #f #H elim H -f -f2 -L1 -L2
+[ #f1 #f2 #Hf12 #g1 #Hfg1
+ /3 width=3 by lsubf_atom, eq_canc_sn/
+| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
+ elim (eq_inv_px ā¦ H) -H [|*: // ] #g1 #Hfg1 #H destruct
+ /3 width=1 by lsubf_push/
+| #f1 #f2 #I #K1 #K2 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g1 #Hfg1 #H destruct
+ /3 width=1 by lsubf_bind/
+| #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g1 #Hfg1 #H destruct
+ /3 width=5 by lsubf_beta, sor_eq_repl_back3/
+| #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g1 #Hfg1 #H destruct
+ /3 width=5 by lsubf_unit, sor_eq_repl_back3/
+]
+qed-.
lemma lsubf_eq_repl_fwd1: āf2,L1,L2. eq_repl_fwd ā¦ (Ī»f1. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
#f2 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back1/
qed-.
-axiom lsubf_eq_repl_back2: āf1,L1,L2. eq_repl_back ā¦ (Ī»f2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
+lemma lsubf_eq_repl_back2: āf1,L1,L2. eq_repl_back ā¦ (Ī»f2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
+#f1 #L1 #L2 #f #H elim H -f1 -f -L1 -L2
+[ #f1 #f2 #Hf12 #g2 #Hfg2
+ /3 width=3 by lsubf_atom, eq_trans/
+| #f1 #f2 #I1 #I2 #K1 #K2 #_ #IH #g #H
+ elim (eq_inv_px ā¦ H) -H [|*: // ] #g2 #Hfg2 #H destruct
+ /3 width=1 by lsubf_push/
+| #f1 #f2 #I #K1 #K2 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g2 #Hfg2 #H destruct
+ /3 width=1 by lsubf_bind/
+| #f #f0 #f1 #f2 #K1 #L2 #W #V #Hf #Hf1 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g2 #Hfg2 #H destruct
+ /3 width=5 by lsubf_beta/
+| #f #f0 #f1 #f2 #I1 #I2 #K1 #K2 #V #Hf #Hf1 #_ #IH #g #H
+ elim (eq_inv_nx ā¦ H) -H [|*: // ] #g2 #Hfg2 #H destruct
+ /3 width=5 by lsubf_unit/
+]
+qed-.
lemma lsubf_eq_repl_fwd2: āf1,L1,L2. eq_repl_fwd ā¦ (Ī»f2. ā¦L1,f1ā¦ ā«š
+ ā¦L2,f2ā¦).
#f1 #L1 #L2 @eq_repl_sym /2 width=3 by lsubf_eq_repl_back2/
#f #f0 #g1 #L1 #V #Hf #Hg1 #f2
elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
-| @(ex2_intro ā¦ (āg1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
+| @(ex2_intro ā¦ (āg1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *)
]
qed-.