Skip to content

Commit e6f73b8

Browse files
MirceaSMirceaS
committed
wip
1 parent 5ebf6d3 commit e6f73b8

File tree

4 files changed

+186
-80
lines changed

4 files changed

+186
-80
lines changed

‎01-propositional.mm1‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -773,3 +773,6 @@ theorem iand4 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -
773773

774774
theorem iand5 (h1: $ aa -> bb $) (h2: $ aa -> c $) (h3: $ aa -> d $) (h4: $ aa -> e $) (h5: $ aa -> f $): $ aa -> bb /\ c /\ d /\ e /\ f $ =
775775
'(iand (iand (iand (iand h1 h2) h3) h4) h5);
776+
777+
theorem imp_or_extract: $ (aa -> bb) \/ (aa -> c) <-> (aa -> (bb \/ c)) $ =
778+
'(ibii (eori (imim2 orl) (imim2 orr)) imp_or_split);

‎12-proof-system-p.mm1‎

Lines changed: 65 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,10 @@ theorem subset_imp_or_subset_r:
365365
theorem subset_and: $ (phi C= (psi1 /\ psi2)) -> (phi C= psi1) /\ (phi C= psi2) $ =
366366
'(iand (framing_subset id anl) (framing_subset id anr));
367367

368+
theorem and_subset: $ (phi1 C= psi) /\ (phi2 C= psi) <-> (phi1 \/ phi2 C= psi) $ =
369+
'(ibii (rsyl (anr propag_and_floor) @ framing_floor @ curry eor) @
370+
iand (framing_floor @ imim1 orl) (framing_floor @ imim1 orr));
371+
368372
theorem taut_equiv_top (h: $ phi $): $ phi <-> top $ =
369373
'(ibii imp_top @ a1i h);
370374
theorem taut_and_equiv (h: $ phi $): $ phi /\ psi <-> psi $ =
@@ -1052,12 +1056,12 @@ theorem ceil_appCtx_dual (phi: Pattern) {box: SVar} (ctx: Pattern box):
10521056
$ |^ phi ^| -> ~ (app[ (~ (|^ phi ^|)) / box ] ctx) $ =
10531057
'(rsyl (anr floor_ceil_ceil) @ rsyl floor_appCtx_dual @ con3 @ framing @ con3 @ anl floor_ceil_ceil);
10541058

1055-
theorem ceil_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
1059+
theorem floor_imp_in_appCtx (phi psi: Pattern) {box: SVar} (ctx: Pattern box):
10561060
$ (app[ |_ phi _| -> psi / box ] ctx) -> |_ phi _| -> app[ psi / box ] ctx $ =
10571061
'(exp @ rsyl (anim propag_or floor_appCtx_dual) @ rsyl (anl andir) @ eori (syl absurdum @ rsyl (anim1 @ framing notnot1) @ notnot1 notnot1) anl);
10581062

10591063
do {
1060-
(def (ceil_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) ceil_imp_in_appCtx))
1064+
(def (floor_imp_in_appCtx_subst subst) '(norm (norm_imp ,subst @ norm_imp_r ,subst) floor_imp_in_appCtx))
10611065
};
10621066

10631067
theorem alpha_exists {x y: EVar} (phi: Pattern x y)
@@ -1291,6 +1295,21 @@ theorem ceil_is_pred: $ (|^ phi ^| == bot) \/ (|^ phi ^| == top) $ =
12911295
@ rsyl anr @ mpcom taut)
12921296
emr);
12931297

1298+
theorem floor_is_pred: $ (|_ phi _| == bot) \/ (|_ phi _| == top) $ =
1299+
'(orim
1300+
(anl
1301+
@ bitr (bicom @ cong_of_equiv_not @ ceil_floor_floor)
1302+
@ bitr not_ceil_floor_bi
1303+
@ cong_of_equiv_floor
1304+
@ ibii (iand id @ a1i absurdum)
1305+
anl)
1306+
(anl
1307+
@ bitr (bicom floor_idem)
1308+
@ cong_of_equiv_floor
1309+
@ ibii (iand (a1i imp_top) @ com12 @ a1i id)
1310+
@ rsyl anr @ mpcom taut)
1311+
emr);
1312+
12941313
theorem ceil_idempotency_for_pred (phi: Pattern): $ ((phi == bot) \/ (phi == top)) <-> (phi == |^ phi ^|) $ =
12951314
(named '(ibii
12961315
(eori
@@ -1543,3 +1562,47 @@ do {
15431562
[_ 'biid]
15441563
)
15451564
};
1565+
1566+
theorem is_pred_floor: $ (is_pred phi) <-> (phi == |_ phi _|) $ =
1567+
'(ibii
1568+
(rsyl (anl floor_of_floor_or) @ framing_floor @ eori (rsyl (rsyl corollary_57_floor anl) @ iand (imim2 absurdum) @ a1i corollary_57_floor) @ iand (rsyl ,(func_subst_explicit_helper 'x $ (eVar x) -> |_ eVar x _| $) @ rsyl anr @ mpcom @ a1i @ lemma_46_floor taut) @ a1i corollary_57_floor)
1569+
(rsyl ,(func_subst_explicit_helper 'x $((eVar x) == bot) \/ ((eVar x) == top)$) @ rsyl anr @ mpcom floor_is_pred));
1570+
1571+
theorem KT_imp {X: SVar} (ctx ante phi: Pattern X)
1572+
(pos: $ _Positive X ctx $)
1573+
(propag: $ (s[ ante -> phi / X ] ctx) -> ante -> s[ phi / X ] ctx $)
1574+
(h: $ ante -> (s[ phi / X ] ctx) -> phi $):
1575+
$ ante -> (mu X ctx) -> phi $ =
1576+
'(com12 @ KT pos @ rsyl propag (prop_2 h));
1577+
1578+
theorem KT_subset {X: SVar} (ctx phi: Pattern X)
1579+
(pos: $ _Positive X ctx $)
1580+
(propag: $ (s[ ((s[ phi / X ] ctx) C= phi) -> phi / X ] ctx) -> ((s[ phi / X ] ctx) C= phi) -> s[ phi / X ] ctx $):
1581+
$ ((s[ phi / X ] ctx) C= phi) -> ((mu X ctx) C= phi) $ =
1582+
'(rsyl (anr floor_idem) @ framing_floor @ KT_imp pos propag corollary_57_floor);
1583+
1584+
do {
1585+
(def (KT_subset_subst subst pos propag) '(norm (norm_imp_l @ norm_subset ,subst norm_refl) @ KT_subset ,pos @ norm (norm_sym @ norm_imp (norm_trans (norm_svSubst_pt norm_refl @ norm_imp_l @ norm_subset ,subst norm_refl) ,subst) @ norm_imp (norm_subset ,subst norm_refl) ,subst) ,propag))
1586+
};
1587+
1588+
1589+
theorem floor_extract_app
1590+
(h1: $ phi1 -> |_ psi _| -> rho1 $)
1591+
(h2: $ phi2 -> |_ psi _| -> rho2 $):
1592+
$ (app phi1 phi2) -> |_ psi _| -> app rho1 rho2 $ =
1593+
(named '(rsyl ,(framing_subst 'h1 'appCtxLVar) @ rsyl ,(floor_imp_in_appCtx_subst 'appCtxLVar) @ rsyl (imim2 (rsyl ,(framing_subst 'h2 'appCtxRVar) ,(floor_imp_in_appCtx_subst 'appCtxRVar))) imidm));
1594+
1595+
theorem floor_extract_or
1596+
(h1: $ phi1 -> |_ psi _| -> rho1 $)
1597+
(h2: $ phi2 -> |_ psi _| -> rho2 $):
1598+
$ phi1 \/ phi2 -> |_ psi _| -> rho1 \/ rho2 $ =
1599+
'(rsyl (orim h1 h2) @ anl imp_or_extract);
1600+
1601+
do {
1602+
(def (floor_extract x ctx) @ match ctx
1603+
[$eVar ,y$ (if (== x y) 'id 'prop_1)]
1604+
[$app ,phi1 ,phi2$ '(floor_extract_app ,(floor_extract x phi1) ,(floor_extract x phi2))]
1605+
[$or ,phi1 ,phi2$ '(floor_extract_or ,(floor_extract x phi1) ,(floor_extract x phi2))]
1606+
[_ 'prop_1]
1607+
)
1608+
};

‎nominal/core.mm1‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,15 @@ axiom EV_abstraction {a b: EVar} (alpha tau: Pattern) (phi psi: Pattern a b):
5656
(is_of_sort phi alpha) ->
5757
(is_of_sort psi tau) ->
5858
((swap (eVar a) (eVar b) (abstraction phi psi)) == abstraction (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
59-
-- add EV axiom for swap
59+
60+
axiom EV_swap {a b c d: EVar} (alpha tau: Pattern) (phi: Pattern a b c d):
61+
$ is_atom_sort alpha $ >
62+
$ is_nominal_sort tau $ >
63+
$ s_forall alpha a (s_forall alpha b (s_forall alpha c (s_forall alpha d (
64+
(is_of_sort phi alpha) ->
65+
(is_of_sort psi tau) ->
66+
((swap (eVar a) (eVar b) (swap (eVar c) (eVar d) phi)) == swap (swap (eVar a) (eVar b) (eVar c)) (swap (eVar a) (eVar b) (eVar d)) (swap (eVar a) (eVar b) phi)))))) $;
67+
6068
axiom EV_supp {a b: EVar} (tau: Pattern) (phi: Pattern a b):
6169
$ is_atom_sort alpha $ >
6270
$ is_nominal_sort tau $ >

‎nominal/lambda.mm1‎

Lines changed: 109 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,11 @@ axiom EV_lc_var {a b: EVar} (c: Pattern a b):
2323
term lc_app_sym: Symbol;
2424
def lc_app (phi rho: Pattern): Pattern = $ (sym lc_app_sym) @@ phi @@ rho $;
2525
axiom function_lc_app: $ ,(is_function '(sym lc_var_app) '[Exp Exp] 'Exp) $;
26+
axiom EV_lc_app {a b: EVar} (phi psi: Pattern a b):
27+
$ s_forall Var a (s_forall Var b (
28+
(is_of_sort phi Exp) ->
29+
(is_of_sort psi Exp) ->
30+
((swap (eVar a) (eVar b) (lc_app phi psi)) == lc_app (swap (eVar a) (eVar b) phi) (swap (eVar a) (eVar b) psi)))) $;
2631

2732
term lc_lam_sym: Symbol;
2833
def lc_lam (phi: Pattern): Pattern = $ (sym lc_lam_sym) @@ phi $;
@@ -276,6 +281,24 @@ theorem freshness_irrelevance_var (exp_pred exp_suff_fresh: Pattern):
276281
imim2 (rsyl (anr imp_r_forall_disjoint) @ imim2 ,(pointwise_decomposition_imp_subst 'appCtxRVar)) @ anr imp_r_forall_disjoint @ univ_gene lc_lemma_2_var
277282
) lc_lmma_1_var));
278283

284+
theorem simple_induction_principle (exp_pred: Pattern):
285+
$ (is_exp exp_pred) ->
286+
((lc_var Vars) C= exp_pred) ->
287+
((lc_app exp_pred exp_pred) C= exp_pred) ->
288+
((lc_lam (abstraction Vars exp_pred)) C= exp_pred) ->
289+
(Exps == exp_pred) $ =
290+
(named '(exp @ exp @ exp @
291+
syl (curry @ com12 subset_to_eq) @
292+
iand an3l @
293+
syl (subset_trans @ eq_imp_subset no_junk) @
294+
rsyl (anim1 @ anim1 anr) @
295+
rsyl (anim1 @ anl and_subset) @
296+
rsyl (anl and_subset)
297+
,(KT_subset_subst
298+
(propag_s_subst 'X $bot \/ (bot @@ (sVar X) @@ (sVar X)) \/ (bot @@ (bot @@ bot @@ (sVar X)))$)
299+
'(positive_in_or (positive_in_or positive_disjoint @ positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_in_same_sVar) @ positive_in_app positive_disjoint @ positive_in_app positive_disjoint positive_in_same_sVar)
300+
(floor_extract 'x $_ \/ (_ @@ (eVar x) @@ (eVar x)) \/ (_ @@ (_ @@ _ @@ (eVar x)))$))));
301+
279302
theorem induction_principle (exp_pred exp_suff_fresh_var exp_suff_fresh_lam: Pattern):
280303
$ (is_var exp_suff_fresh_var) ->
281304
|^ exp_suff_fresh_var ^| ->
@@ -318,12 +341,12 @@ theorem induction_principle (exp_pred exp_suff_fresh_var exp_suff_fresh_lam: Pat
318341
(syl imidm @ imim2 (imim2 @ syl imidm @ imim2 (imim2 @ com12 @ rsyl corollary_57_floor @ syl corollary_57_floor @
319342
anlr
320343
)
321-
,(ceil_imp_in_appCtx_subst 'appCtxLRVar))
322-
,(ceil_imp_in_appCtx_subst 'appCtxRVar)))
344+
,(floor_imp_in_appCtx_subst 'appCtxLRVar))
345+
,(floor_imp_in_appCtx_subst 'appCtxRVar)))
323346
(syl imidm @ imim2 (imim2 @ com12 @ rsyl corollary_57_floor @ syl corollary_57_floor @
324347
prop_2 (prop_2 (prop_2 (prop_2 (prop_2 (prop_1 freshness_irrelevance_lam) an6lr) an5lr) anr) an4lr) an3lr
325348
)
326-
,(ceil_imp_in_appCtx_subst @ appCtx_constructor '[1 1]))
349+
,(floor_imp_in_appCtx_subst @ appCtx_constructor '[1 1]))
327350
)
328351
an4lr));
329352

@@ -454,6 +477,24 @@ theorem curried_function_swap_atom {a b c: EVar}:
454477
theorem satisfying_exps2_is_exp: $ is_exp satisfying_exps2 $ =
455478
(named '(imp_to_subset @ exists_generalization_disjoint @ rsyl (anim2 anl) @ curry subset_to_imp));
456479

480+
theorem subset_trans_var_lemma {x: EVar} (phi psi: Pattern x):
481+
$ (phi C= psi) -> (x in phi) -> ((eVar x) C= psi) $ =
482+
'(rsyl (com12 subset_trans) @ imim1 eVar_in_subset_forward);
483+
484+
theorem var_in_satisfying_exps2:
485+
$(x in satisfying_exps2) <-> (is_exp (eVar x)) /\ s_forall Var a (s_forall Var b (s_forall Exp plug1 (s_forall Exp plug2 ((fresh_for (eVar a) (eVar plug2)) /\ (eVar a != eVar b) -> subst_induction_pred (eVar a) (eVar b) (eVar x) (eVar plug1) (eVar plug2)))))$ =
486+
(named '(ibii
487+
(iand (subset_trans_var_lemma satisfying_exps2_is_exp) @
488+
rsyl (anl ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
489+
exists_generalization_disjoint @
490+
rsyl anr @
491+
curry @
492+
syl anr ,(func_subst_explicit_helper 'x $forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))$)) @
493+
494+
syl (anr ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
495+
syl ,(exists_intro_subst @ propag_e_subst 'x $((eVar x) C= bot) /\ ((bot == (eVar x)) /\ (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))))$) @
496+
anim2 @ ian eq_refl));
497+
457498
theorem EV_set: $ EV_pattern Var satisfying_exps2 $ =
458499
(named '(univ_gene @ anr imp_r_forall_disjoint @ univ_gene @ exp @ syl (curry subset_to_eq) @ syl
459500
(iand anr @ rsyl (anim
@@ -586,11 +627,9 @@ theorem mem_func_lemma_neg:
586627
(named '(com12 ,(func_subst_explicit_thm 'y2 $~(z in (eVar y2)) -> ~((eVar z) == (eVar y2))$) @ univ_gene @ con3 membership_var_reverse));
587628

588629
theorem subst_induction_var2: $ (lc_var Vars) C= satisfying_exps2 $ =
589-
(named '(imp_to_subset @ membership_elim @ forall_framing membership_imp_reverse @ univ_gene @
590-
syl (anr ,(propag_mem 'x $exists y (|_ _ _| /\ (eVar y /\ (forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> forall _ (|_ _ _| -> ((~(|_ _ _|)) /\ ~(|_ _ _|)) -> |_ _ _|)))))))$)) @
591-
syl ,(exists_intro_subst @ propag_e_subst 'x $((eVar x) C= bot) /\ ((bot == (eVar x)) /\ (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> (forall _ (bot -> bot -> ((app (app bot (app (app bot (eVar x)) bot)) bot) == (app (app bot (app (app bot (eVar x)) bot)) bot)))))))))))$) @
592-
iand (rsyl eVar_in_subset_forward @ com12 subset_trans @ mp ,(function_sorting_full 1) function_lc_var) @
593-
iand (a1i eq_refl) @
630+
(named '(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
631+
syl (anr var_in_satisfying_exps2) @
632+
iand (subset_trans_var_lemma @ mp ,(function_sorting_full 1) function_lc_var) @
594633
anr ,(forall_extract $_ -> _$) @ univ_gene @
595634
anr ,(forall_extract $_ -> _ -> _$) @ univ_gene @
596635
anr ,(forall_extract $_ -> _ -> _ -> _$) @ univ_gene @
@@ -682,77 +721,70 @@ theorem subst_induction_var2: $ (lc_var Vars) C= satisfying_exps2 $ =
682721
a1i eq_refl));
683722

684723
theorem subst_induction_app2: $ (lc_app satisfying_exps2 satisfying_exps2) C= satisfying_exps2 $ =
685-
'(imp_to_subset _);
686-
687-
theorem subst_induction_app_lemma
688-
(a_var: $ is_sorted_func Var a $)
689-
(b_var: $ is_sorted_func Var b $)
690-
(plug1_exp: $ is_exp plug1 $)
691-
(plug2_exp: $ is_exp plug2 $):
692-
$ (is_exp (eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) /\ (is_exp (eVar y) /\ subst_induction_pred a b (eVar y) plug1 plug2) -> subst_induction_pred a b (lc_app (eVar x) (eVar y)) plug1 plug2 $ =
693-
(named '(rsyl (anl an4) @ rsyl (anim2 @
694-
syl (curry eq_trans) @
695-
iand
696-
(rsyl anl @ eq_equiv_to_eq_eq ,(func_subst_explicit_helper 'z $_ @@ (eVar z) @@ _$))
697-
(rsyl anr @ eq_equiv_to_eq_eq ,(func_subst_explicit_helper 'z $_ @@ (eVar z)$))
698-
) @
699-
rsyl (anim1 @ iand id id) @
700-
rsyl (anl anass) @
701-
rsyl (anim2 @ anim1 @ syl (curry @ subst_app b_var plug2_exp) (anim
702-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
703-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting a_var)) plug1_exp)
704-
)) @
705-
rsyl (anim2 @ curry eq_trans) @
706-
rsyl (anim1 @ iand id id) @
707-
rsyl (anl anass) @
708-
rsyl (anim2 @ anim1 @ syl ,(imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app a_var plug1_exp) @
709-
rsyl (anim2 @ curry eq_trans) @
710-
rsyl (anim1 @ iand id id) @
711-
rsyl (anl anass) @
712-
rsyl (anim2 @ anim1 @ syl eq_sym @ syl (curry @ subst_app a_var (mp (mp (mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug1_exp) plug2_exp)) (anim
713-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
714-
(mp (com12 @ mp ,(function_sorting 3 'function_subst) (domain_func_sorting b_var)) plug2_exp)
715-
)) @
716-
rsyl (anim2 @ impcom eq_trans) @
717-
rsyl (anim1 @ iand id id) @
718-
rsyl (anl anass) @
719-
rsyl (anim2 @ anim1 @ syl eq_sym @ syl ,(imp_eq_framing_subst 'appCtxLRVar) @ curry @ subst_app b_var plug2_exp) @
720-
rsyl (anim2 @ impcom eq_trans) @
721-
anr));
722-
723-
theorem subst_induction_app (a b plug1 plug2: Pattern)
724-
(lemma: $ (is_exp (eVar x) /\ subst_induction_pred a b (eVar x) plug1 plug2) /\ (is_exp (eVar y) /\ subst_induction_pred a b (eVar y) plug1 plug2) -> subst_induction_pred a b (lc_app (eVar x) (eVar y)) plug1 plug2 $):
725-
$ (lc_app (satisfying_exps a b plug1 plug2) (satisfying_exps a b plug1 plug2)) C= (satisfying_exps a b plug1 plug2) $ =
726-
(named '(imp_to_subset @
727-
rsyl (anl ,(ex_appCtx_subst 'appCtxLRVar)) @
724+
(named '(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
725+
syl (anr var_in_satisfying_exps2) @
726+
iand (subset_trans_var_lemma @ mp ,(function_sorting 2 'function_lc_app) satisfying_exps2_is_exp satisfying_exps2_is_exp) @
727+
anr ,(forall_extract $_ -> _$) @ univ_gene @
728+
anr ,(forall_extract $_ -> _ -> _$) @ univ_gene @
729+
anr ,(forall_extract $_ -> _ -> _ -> _$) @ univ_gene @
730+
anr ,(forall_extract $_ -> _ -> _ -> _ -> _$) @ univ_gene @
731+
rsyl (anl ,(membership_appCtx_subst 'appCtxLRVar)) @
732+
rsyl (exists_framing @ anim2 @ anl ,(membership_appCtx_subst 'appCtxRVar)) @
728733
exists_generalization_disjoint @
729-
rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @
734+
rsyl and_exists_disjoint_reverse @
730735
exists_generalization_disjoint @
731-
rsyl ,(appCtx_floor_commute_b_subst 'appCtxLRVar) @
732-
rsyl (anim1 @ iand id id) @
733-
rsyl (anl anass) @
734-
rsyl (anim2 @
735-
rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxLRVar)) @
736-
rsyl (anim2 ancom) @
737-
rsyl (anr anass) @
738-
rsyl (anim2 @
739-
rsyl ,(appCtx_floor_commute_b_subst 'appCtxRVar) @
740-
rsyl (anim1 @ iand id id) @
741-
rsyl (anl anass) @
742-
anim2 @
743-
rsyl (anim2 ,(appCtx_floor_commute_subst 'appCtxRVar)) @
744-
rsyl (anim2 ancom) @
745-
anr anass
746-
) @
747-
rsyl (anl anlass) @
748-
anim2 @
749-
anr anass) @
750736
rsyl (anr anass) @
751-
rsyl (anim2 @ anim1 lemma) @
752-
rsyl (anim2 @ ancom) @
753-
rsyl (anim1 @ curry @ mp ,(inst_foralls 2) function_lc_app) @
754-
curry ,(func_subst_alt_thm_sorted 'x $(eVar x) /\ ((app (app _ (app (app _ (eVar x)) _)) _) == (app (app _ (app (app _ (eVar x)) _)) _))$)
755-
));
737+
rsyl (iand anl @ iand anr anl) @
738+
rsyl (anim2 @ syl appl @ anim2 @ syl mem_func_lemma @ syl (exists_framing anr) @ syl (curry @ mp ,(inst_foralls 2) function_lc_app) @ anim (subset_trans_var_lemma satisfying_exps2_is_exp) (subset_trans_var_lemma satisfying_exps2_is_exp)) @
739+
impcom @
740+
mp ,(func_subst_imp_to_var 'y3 $bot -> bot -> bot -> bot -> bot -> bot -> ((bot @@ bot @@ (bot @@ bot @@ (eVar y3) @@ bot) @@ bot) == (bot @@ bot @@ (bot @@ bot @@ (eVar y3) @@ bot) @@ bot))$) @
741+
exp @ exp @ exp @ exp @ exp @
742+
sylc eq_trans (
743+
syl ,(imp_eq_framing_subst @ appCtx_constructor '[0 1]) @
744+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
745+
iand4 an4lr anllr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp)) @
746+
sylc eq_trans (
747+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
748+
iand4 an3lr anlr (syl (curry @ curry subst_sorting) @ iand3 an4lr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) anllr)
749+
(syl (curry @ curry subst_sorting) @ iand3 an4lr (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp) anllr)) @
750+
syl eq_sym @
751+
sylc eq_trans (
752+
syl ,(imp_eq_framing_subst @ appCtx_constructor '[0 1]) @
753+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
754+
iand4 an3lr anlr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp)) @
755+
sylc eq_trans (
756+
syl (curry @ curry @ curry @ mp ,(inst_foralls 1) subst_app) @
757+
iand4 an4lr (syl (curry @ curry subst_sorting) @ iand3 an3lr anllr anlr) (syl (curry @ curry subst_sorting) @ iand3 an3lr (rsyl an6l @ subset_trans_var_lemma satisfying_exps2_is_exp) anlr)
758+
(syl (curry @ curry subst_sorting) @ iand3 an3lr (rsyl an5lr @ subset_trans_var_lemma satisfying_exps2_is_exp) anlr)) @
759+
syl (curry eq_trans) @
760+
syl (anim ,(eq_framing_imp_subst 'appCtxLRVar) ,(eq_framing_imp_subst 'appCtxRVar)) @
761+
iand
762+
(curry @ curry @ curry @ curry @ curry @
763+
rsyl anl @
764+
rsyl (anl var_in_satisfying_exps2) @
765+
rsyl anr @
766+
rsyl var_subst_same_var @ imim2 @
767+
rsyl var_subst_same_var @ imim2 @
768+
rsyl var_subst_same_var @ imim2 @
769+
rsyl var_subst_same_var @ imim2 @
770+
imim2 eq_sym)
771+
(curry @ curry @ curry @ curry @ curry @
772+
rsyl anr @
773+
rsyl (anl var_in_satisfying_exps2) @
774+
rsyl anr @
775+
rsyl var_subst_same_var @ imim2 @
776+
rsyl var_subst_same_var @ imim2 @
777+
rsyl var_subst_same_var @ imim2 @
778+
rsyl var_subst_same_var @ imim2 @
779+
imim2 eq_sym)));
780+
781+
782+
theorem subst_induction_lam2: $ (lc_lam (abstraction Vars satisfying_exps2)) C= satisfying_exps2 $ =
783+
'(imp_to_subset @ membership_elim_implicit @ membership_imp_reverse @
784+
syl (anr var_in_satisfying_exps2) @
785+
iand (subset_trans_var_lemma @ mp ,(function_sorting 1 'function_lc_lam) @ mp ,(function_sorting 2 '(function_abstraction Var_atom Exp_sort)) subset_refl satisfying_exps2_is_exp) @
786+
_);
787+
756788

757789
theorem subst_induction_lam_lemma (a b c plug1 plug2: Pattern)
758790
(diff_atoms_ab: $ a != b $)
@@ -823,7 +855,7 @@ theorem subst_induction_lemma:
823855
satisfying_exps2_is_exp
824856
EV_set
825857
subst_induction_var2
826-
_
858+
subst_induction_app2
827859
_);
828860

829861
do {

0 commit comments

Comments
 (0)