(* *)
(**************************************************************************)
+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-.
#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-.