diff --git a/01-propositional.mm1 b/01-propositional.mm1 index 814f8c7..ab12f84 100644 --- a/01-propositional.mm1 +++ b/01-propositional.mm1 @@ -349,345 +349,345 @@ do { @ refine tgt (foldl ps (verb e) @ fn (acc p2) @ copy-span e '(mp ,acc ,p2))) }; -theorem a1i (h: $ b $): $ a -> b $ = '(prop_1 h); -theorem a2i (h: $ a -> b -> c $): $ (a -> b) -> (a -> c) $ = '(prop_2 h); -theorem mpd (h1: $ a -> b $) (h2: $ a -> b -> c $): $ a -> c $ = '(prop_2 h2 h1); -theorem mpi (h1: $ b $) (h2: $ a -> b -> c $): $ a -> c $ = '(mpd (a1i h1) h2); -theorem id: $ a -> a $ = '(mpd (! prop_1 _ a) prop_1); -theorem idd: $ a -> b -> b $ = '(a1i id); -theorem syl (h1: $ b -> c $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (a1i h1)); -theorem rsyl (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 h1); -theorem a1d (h: $ a -> b $): $ a -> c -> b $ = '(syl prop_1 h); -theorem a2d (h: $ a -> b -> c -> d $): $ a -> (b -> c) -> (b -> d) $ = '(syl prop_2 h); -theorem a3d (h: $ a -> ~b -> ~c $): $ a -> c -> b $ = '(syl prop_3 h); -theorem sylc (h: $ b -> c -> d $) (h1: $ a -> b $) (h2: $ a -> c $): $ a -> d $ = '(mpd h2 @ syl h h1); -theorem syld (h1: $ a -> b -> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(mpd h1 @ a2d @ a1d h2); -theorem syl5 (h1: $ b -> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (a1i h1) h2); -theorem syl6 (h1: $ c -> d $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syld h2 (a1i h1)); -theorem imim2: $ (b -> c) -> (a -> b) -> (a -> c) $ = '(a2d prop_1); -theorem imim2i (h: $ b -> c $): $ (a -> b) -> (a -> c) $ = '(imim2 h); -theorem imim2d (h: $ a -> c -> d $): $ a -> (b -> c) -> (b -> d) $ = '(syl imim2 h); -theorem absurd: $ ~a -> a -> b $ = '(a3d prop_1); -theorem com12 (h: $ a -> b -> c $): $ b -> a -> c $ = '(syl (a2i h) prop_1); -theorem mpcom: $ a -> (a -> b) -> b $ = '(com12 id); -theorem com23 (h: $ a -> b -> c -> d $): $ a -> c -> b -> d $ = '(syl (com12 @ imim2d mpcom) h); -theorem eimd (h1: $ a -> b $) (h2: $ a -> c -> d $): $ a -> (b -> c) -> d $ = '(syld (rsyl h1 mpcom) h2); -theorem absurdr: $ a -> ~a -> b $ = '(com12 absurd); -theorem imim1: $ (a -> b) -> (b -> c) -> (a -> c) $ = '(com12 imim2); -theorem imim1i (h: $ a -> b $): $ (b -> c) -> (a -> c) $ = '(imim1 h); -theorem imim1d (h: $ a -> b -> c $): $ a -> (c -> d) -> (b -> d) $ = '(syl imim1 h); -theorem imimd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $): - $ a -> (c -> d) -> (b -> e) $ = '(syld (imim1d h1) (imim2d h2)); -theorem imim: $ (a -> b) -> (c -> d) -> (b -> c) -> (a -> d) $ = '(syl5 imim2 (imim2d imim1)); -theorem imidm: $ (a -> a -> b) -> a -> b $ = '(a2i mpcom); -theorem eim: $ a -> (b -> c) -> (a -> b) -> c $ = '(imim1d mpcom); -theorem contra: $ (~a -> a) -> a $ = '(imidm (a3d (a2i absurd))); -theorem dne: $ ~~a -> a $ = '(syl contra absurd); -theorem inot: $ (a -> ~a) -> ~a $ = '(syl contra (imim1 dne)); -theorem con2: $ (a -> ~b) -> (b -> ~a) $ = '(a3d (syl5 dne id)); -theorem notnot1: $ a -> ~~a $ = '(con2 id); -theorem con3: $ (a -> b) -> (~b -> ~a) $ = '(syl con2 (imim2i notnot1)); -theorem con1: $ (~a -> b) -> (~b -> a) $ = '(a3d (imim2i notnot1)); -theorem cases (h1: $ a -> b $) (h2: $ ~a -> b $): $ b $ = '(contra @ syl h1 @ con1 h2); -theorem casesd (h1: $ a -> b -> c $) (h2: $ a -> ~b -> c $): $ a -> c $ = +theorem a1i (h: $ bb $): $ aa -> bb $ = '(prop_1 h); +theorem a2i (h: $ aa -> bb -> c $): $ (aa -> bb) -> (aa -> c) $ = '(prop_2 h); +theorem mpd (h1: $ aa -> bb $) (h2: $ aa -> bb -> c $): $ aa -> c $ = '(prop_2 h2 h1); +theorem mpi (h1: $ bb $) (h2: $ aa -> bb -> c $): $ aa -> c $ = '(mpd (a1i h1) h2); +theorem id: $ aa -> aa $ = '(mpd (! prop_1 _ aa) prop_1); +theorem idd: $ aa -> bb -> bb $ = '(a1i id); +theorem syl (h1: $ bb -> c $) (h2: $ aa -> bb $): $ aa -> c $ = '(mpd h2 (a1i h1)); +theorem rsyl (h1: $ aa -> bb $) (h2: $ bb -> c $): $ aa -> c $ = '(syl h2 h1); +theorem a1d (h: $ aa -> bb $): $ aa -> c -> bb $ = '(syl prop_1 h); +theorem a2d (h: $ aa -> bb -> c -> d $): $ aa -> (bb -> c) -> (bb -> d) $ = '(syl prop_2 h); +theorem a3d (h: $ aa -> ~bb -> ~c $): $ aa -> c -> bb $ = '(syl prop_3 h); +theorem sylc (h: $ bb -> c -> d $) (h1: $ aa -> bb $) (h2: $ aa -> c $): $ aa -> d $ = '(mpd h2 @ syl h h1); +theorem syld (h1: $ aa -> bb -> c $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(mpd h1 @ a2d @ a1d h2); +theorem syl5 (h1: $ bb -> c $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(syld (a1i h1) h2); +theorem syl6 (h1: $ c -> d $) (h2: $ aa -> bb -> c $): $ aa -> bb -> d $ = '(syld h2 (a1i h1)); +theorem imim2: $ (bb -> c) -> (aa -> bb) -> (aa -> c) $ = '(a2d prop_1); +theorem imim2i (h: $ bb -> c $): $ (aa -> bb) -> (aa -> c) $ = '(imim2 h); +theorem imim2d (h: $ aa -> c -> d $): $ aa -> (bb -> c) -> (bb -> d) $ = '(syl imim2 h); +theorem absurd: $ ~aa -> aa -> bb $ = '(a3d prop_1); +theorem com12 (h: $ aa -> bb -> c $): $ bb -> aa -> c $ = '(syl (a2i h) prop_1); +theorem mpcom: $ aa -> (aa -> bb) -> bb $ = '(com12 id); +theorem com23 (h: $ aa -> bb -> c -> d $): $ aa -> c -> bb -> d $ = '(syl (com12 @ imim2d mpcom) h); +theorem eimd (h1: $ aa -> bb $) (h2: $ aa -> c -> d $): $ aa -> (bb -> c) -> d $ = '(syld (rsyl h1 mpcom) h2); +theorem absurdr: $ aa -> ~aa -> bb $ = '(com12 absurd); +theorem imim1: $ (aa -> bb) -> (bb -> c) -> (aa -> c) $ = '(com12 imim2); +theorem imim1i (h: $ aa -> bb $): $ (bb -> c) -> (aa -> c) $ = '(imim1 h); +theorem imim1d (h: $ aa -> bb -> c $): $ aa -> (c -> d) -> (bb -> d) $ = '(syl imim1 h); +theorem imimd (h1: $ aa -> bb -> c $) (h2: $ aa -> d -> e $): + $ aa -> (c -> d) -> (bb -> e) $ = '(syld (imim1d h1) (imim2d h2)); +theorem imim: $ (aa -> bb) -> (c -> d) -> (bb -> c) -> (aa -> d) $ = '(syl5 imim2 (imim2d imim1)); +theorem imidm: $ (aa -> aa -> bb) -> aa -> bb $ = '(a2i mpcom); +theorem eim: $ aa -> (bb -> c) -> (aa -> bb) -> c $ = '(imim1d mpcom); +theorem contra: $ (~aa -> aa) -> aa $ = '(imidm (a3d (a2i absurd))); +theorem dne: $ ~~aa -> aa $ = '(syl contra absurd); +theorem inot: $ (aa -> ~aa) -> ~aa $ = '(syl contra (imim1 dne)); +theorem con2: $ (aa -> ~bb) -> (bb -> ~aa) $ = '(a3d (syl5 dne id)); +theorem notnot1: $ aa -> ~~aa $ = '(con2 id); +theorem con3: $ (aa -> bb) -> (~bb -> ~aa) $ = '(syl con2 (imim2i notnot1)); +theorem con1: $ (~aa -> bb) -> (~bb -> aa) $ = '(a3d (imim2i notnot1)); +theorem cases (h1: $ aa -> bb $) (h2: $ ~aa -> bb $): $ bb $ = '(contra @ syl h1 @ con1 h2); +theorem casesd (h1: $ aa -> bb -> c $) (h2: $ aa -> ~bb -> c $): $ aa -> c $ = '(cases (com12 h1) (com12 h2)); -theorem con1d (h: $ a -> ~b -> c $): $ a -> ~c -> b $ = '(syl con1 h); -theorem con2d (h: $ a -> b -> ~c $): $ a -> c -> ~b $ = '(syl con2 h); -theorem con3d (h: $ a -> b -> c $): $ a -> ~c -> ~b $ = '(syl con3 h); -theorem con4d (h: $ a -> ~b -> ~c $): $ a -> c -> b $ = '(syl prop_3 h); -theorem mt (h1: $ b -> a $) (h2: $ ~a $): $ ~b $ = '(con3 h1 h2); -theorem mt2 (h1: $ b -> ~a $) (h2: $ a $): $ ~b $ = '(con2 h1 h2); -theorem mtd (h1: $ a -> ~b $) (h2: $ a -> c -> b $): $ a -> ~c $ = '(mpd h1 (con3d h2)); -theorem mti (h1: $ ~b $) (h2: $ a -> c -> b $): $ a -> ~c $ = '(mtd (a1i h1) h2); -theorem mt2d (h1: $ a -> c $) (h2: $ a -> b -> ~c $): $ a -> ~b $ = '(sylc con2 h2 h1); - -theorem anl: $ a /\ b -> a $ = '(con1 absurd); -theorem anr: $ a /\ b -> b $ = '(con1 prop_1); -theorem anli (h: $ a /\ b $): $ a $ = '(anl h); -theorem anri (h: $ a /\ b $): $ b $ = '(anr h); -theorem ian: $ a -> b -> a /\ b $ = '(con2d mpcom); -theorem iand (h1: $ a -> b $) (h2: $ a -> c $): $ a -> b /\ c $ = '(sylc ian h1 h2); -theorem anld (h: $ a -> b /\ c $): $ a -> b $ = '(syl anl h); -theorem anrd (h: $ a -> b /\ c $): $ a -> c $ = '(syl anr h); -theorem iani (h1: $ a $) (h2: $ b $): $ a /\ b $ = '(ian h1 h2); -theorem anwl (h: $ a -> c $): $ a /\ b -> c $ = '(syl h anl); -theorem anwr (h: $ b -> c $): $ a /\ b -> c $ = '(syl h anr); -theorem anll: $ a /\ b /\ c -> a $ = '(anwl anl); -theorem anlr: $ a /\ b /\ c -> b $ = '(anwl anr); -theorem anrl: $ a /\ (b /\ c) -> b $ = '(anwr anl); -theorem anrr: $ a /\ (b /\ c) -> c $ = '(anwr anr); -theorem anwll (h: $ a -> d $): $ a /\ b /\ c -> d $ = '(anwl (anwl h)); -theorem anw3l (h: $ a -> e $): $ a /\ b /\ c /\ d -> e $ = '(anwll (anwl h)); -theorem anw4l (h: $ a -> f $): $ a /\ b /\ c /\ d /\ e -> f $ = '(anw3l (anwl h)); -theorem anw5l (h: $ a -> g $): $ a /\ b /\ c /\ d /\ e /\ f -> g $ = '(anw4l (anwl h)); -theorem anw6l (x: $ a -> h $): $ a /\ b /\ c /\ d /\ e /\ f /\ g -> h $ = '(anw5l (anwl x)); -theorem anw7l (x: $ a -> i $): $ a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> i $ = '(anw6l (anwl x)); -theorem anllr: $ a /\ b /\ c /\ d -> b $ = '(anwll anr); -theorem an3l: $ a /\ b /\ c /\ d -> a $ = '(anwll anl); -theorem an3lr: $ a /\ b /\ c /\ d /\ e -> b $ = '(anwl anllr); -theorem an4l: $ a /\ b /\ c /\ d /\ e -> a $ = '(anwl an3l); -- TODO: automate these -theorem an4lr: $ a /\ b /\ c /\ d /\ e /\ f -> b $ = '(anwl an3lr); -theorem an5l: $ a /\ b /\ c /\ d /\ e /\ f -> a $ = '(anwl an4l); -theorem an5lr: $ a /\ b /\ c /\ d /\ e /\ f /\ g -> b $ = '(anwl an4lr); -theorem an6l: $ a /\ b /\ c /\ d /\ e /\ f /\ g -> a $ = '(anwl an5l); -theorem an6lr: $ a /\ b /\ c /\ d /\ e /\ f /\ g /\ h -> b $ = '(anwl an5lr); -theorem curry (h: $ a -> b -> c $): $ a /\ b -> c $ = '(sylc h anl anr); -theorem exp (h: $ a /\ b -> c $): $ a -> b -> c $ = '(syl6 h ian); -theorem impcom (h: $ a -> b -> c $): $ b /\ a -> c $ = '(curry (com12 h)); -theorem expcom (h: $ a /\ b -> c $): $ b -> a -> c $ = '(com12 (exp h)); -theorem syla (h1: $ (b -> c) -> d $) (h2: $ a /\ b -> c $): $ a -> d $ = '(syl h1 @ exp h2); -theorem sylan (h: $ b /\ c -> d $) (h1: $ a -> b $) (h2: $ a -> c $): - $ a -> d $ = '(syl h @ iand h1 h2); -theorem animd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $): $ a -> b /\ d -> c /\ e $ = +theorem con1d (h: $ aa -> ~bb -> c $): $ aa -> ~c -> bb $ = '(syl con1 h); +theorem con2d (h: $ aa -> bb -> ~c $): $ aa -> c -> ~bb $ = '(syl con2 h); +theorem con3d (h: $ aa -> bb -> c $): $ aa -> ~c -> ~bb $ = '(syl con3 h); +theorem con4d (h: $ aa -> ~bb -> ~c $): $ aa -> c -> bb $ = '(syl prop_3 h); +theorem mt (h1: $ bb -> aa $) (h2: $ ~aa $): $ ~bb $ = '(con3 h1 h2); +theorem mt2 (h1: $ bb -> ~aa $) (h2: $ aa $): $ ~bb $ = '(con2 h1 h2); +theorem mtd (h1: $ aa -> ~bb $) (h2: $ aa -> c -> bb $): $ aa -> ~c $ = '(mpd h1 (con3d h2)); +theorem mti (h1: $ ~bb $) (h2: $ aa -> c -> bb $): $ aa -> ~c $ = '(mtd (a1i h1) h2); +theorem mt2d (h1: $ aa -> c $) (h2: $ aa -> bb -> ~c $): $ aa -> ~bb $ = '(sylc con2 h2 h1); + +theorem anl: $ aa /\ bb -> aa $ = '(con1 absurd); +theorem anr: $ aa /\ bb -> bb $ = '(con1 prop_1); +theorem anli (h: $ aa /\ bb $): $ aa $ = '(anl h); +theorem anri (h: $ aa /\ bb $): $ bb $ = '(anr h); +theorem ian: $ aa -> bb -> aa /\ bb $ = '(con2d mpcom); +theorem iand (h1: $ aa -> bb $) (h2: $ aa -> c $): $ aa -> bb /\ c $ = '(sylc ian h1 h2); +theorem anld (h: $ aa -> bb /\ c $): $ aa -> bb $ = '(syl anl h); +theorem anrd (h: $ aa -> bb /\ c $): $ aa -> c $ = '(syl anr h); +theorem iani (h1: $ aa $) (h2: $ bb $): $ aa /\ bb $ = '(ian h1 h2); +theorem anwl (h: $ aa -> c $): $ aa /\ bb -> c $ = '(syl h anl); +theorem anwr (h: $ bb -> c $): $ aa /\ bb -> c $ = '(syl h anr); +theorem anll: $ aa /\ bb /\ c -> aa $ = '(anwl anl); +theorem anlr: $ aa /\ bb /\ c -> bb $ = '(anwl anr); +theorem anrl: $ aa /\ (bb /\ c) -> bb $ = '(anwr anl); +theorem anrr: $ aa /\ (bb /\ c) -> c $ = '(anwr anr); +theorem anwll (h: $ aa -> d $): $ aa /\ bb /\ c -> d $ = '(anwl (anwl h)); +theorem anw3l (h: $ aa -> e $): $ aa /\ bb /\ c /\ d -> e $ = '(anwll (anwl h)); +theorem anw4l (h: $ aa -> f $): $ aa /\ bb /\ c /\ d /\ e -> f $ = '(anw3l (anwl h)); +theorem anw5l (h: $ aa -> g $): $ aa /\ bb /\ c /\ d /\ e /\ f -> g $ = '(anw4l (anwl h)); +theorem anw6l (x: $ aa -> h $): $ aa /\ bb /\ c /\ d /\ e /\ f /\ g -> h $ = '(anw5l (anwl x)); +theorem anw7l (x: $ aa -> i $): $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h -> i $ = '(anw6l (anwl x)); +theorem anllr: $ aa /\ bb /\ c /\ d -> bb $ = '(anwll anr); +theorem an3l: $ aa /\ bb /\ c /\ d -> aa $ = '(anwll anl); +theorem an3lr: $ aa /\ bb /\ c /\ d /\ e -> bb $ = '(anwl anllr); +theorem an4l: $ aa /\ bb /\ c /\ d /\ e -> aa $ = '(anwl an3l); -- TODO: automate these +theorem an4lr: $ aa /\ bb /\ c /\ d /\ e /\ f -> bb $ = '(anwl an3lr); +theorem an5l: $ aa /\ bb /\ c /\ d /\ e /\ f -> aa $ = '(anwl an4l); +theorem an5lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g -> bb $ = '(anwl an4lr); +theorem an6l: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g -> aa $ = '(anwl an5l); +theorem an6lr: $ aa /\ bb /\ c /\ d /\ e /\ f /\ g /\ h -> bb $ = '(anwl an5lr); +theorem curry (h: $ aa -> bb -> c $): $ aa /\ bb -> c $ = '(sylc h anl anr); +theorem exp (h: $ aa /\ bb -> c $): $ aa -> bb -> c $ = '(syl6 h ian); +theorem impcom (h: $ aa -> bb -> c $): $ bb /\ aa -> c $ = '(curry (com12 h)); +theorem expcom (h: $ aa /\ bb -> c $): $ bb -> aa -> c $ = '(com12 (exp h)); +theorem syla (h1: $ (bb -> c) -> d $) (h2: $ aa /\ bb -> c $): $ aa -> d $ = '(syl h1 @ exp h2); +theorem sylan (h: $ bb /\ c -> d $) (h1: $ aa -> bb $) (h2: $ aa -> c $): + $ aa -> d $ = '(syl h @ iand h1 h2); +theorem animd (h1: $ aa -> bb -> c $) (h2: $ aa -> d -> e $): $ aa -> bb /\ d -> c /\ e $ = '(exp (iand (curry (syl5 anl h1)) (curry (syl5 anr h2)))); -theorem anim1d (h: $ a -> b -> c $): $ a -> b /\ d -> c /\ d $ = '(animd h idd); -theorem anim2d (h: $ a -> c -> d $): $ a -> b /\ c -> b /\ d $ = '(animd idd h); -theorem anim1: $ (a -> b) -> a /\ c -> b /\ c $ = '(anim1d id); -theorem anim2: $ (b -> c) -> a /\ b -> a /\ c $ = '(anim2d id); -theorem anim: $ (a -> b) -> (c -> d) -> a /\ c -> b /\ d $ = +theorem anim1d (h: $ aa -> bb -> c $): $ aa -> bb /\ d -> c /\ d $ = '(animd h idd); +theorem anim2d (h: $ aa -> c -> d $): $ aa -> bb /\ c -> bb /\ d $ = '(animd idd h); +theorem anim1: $ (aa -> bb) -> aa /\ c -> bb /\ c $ = '(anim1d id); +theorem anim2: $ (bb -> c) -> aa /\ bb -> aa /\ c $ = '(anim2d id); +theorem anim: $ (aa -> bb) -> (c -> d) -> aa /\ c -> bb /\ d $ = '(exp @ syld (anim1d anl) (anim2d anr)); -theorem anim2a: $ (a -> b -> c) -> (a /\ b -> a /\ c) $ = +theorem anim2a: $ (aa -> bb -> c) -> (aa /\ bb -> aa /\ c) $ = '(exp @ iand anrl @ mpd anrr @ mpd anrl anl); -theorem ancom: $ a /\ b -> b /\ a $ = '(iand anr anl); -theorem anrasss (h: $ a /\ b /\ c -> d $): $ a /\ c /\ b -> d $ = +theorem ancom: $ aa /\ bb -> bb /\ aa $ = '(iand anr anl); +theorem anrasss (h: $ aa /\ bb /\ c -> d $): $ aa /\ c /\ bb -> d $ = '(sylan h (iand anll anr) anlr); -theorem anim1a: $ (a -> b -> c) -> (b /\ a -> c /\ a) $ = +theorem anim1a: $ (aa -> bb -> c) -> (bb /\ aa -> c /\ aa) $ = '(syl6 ancom @ syl5 ancom anim2a); -theorem casesda (h1: $ a /\ b -> c $) (h2: $ a /\ ~b -> c $): $ a -> c $ = +theorem casesda (h1: $ aa /\ bb -> c $) (h2: $ aa /\ ~bb -> c $): $ aa -> c $ = '(casesd (exp h1) (exp h2)); -theorem inotda (h: $ a /\ b -> ~b $): $ a -> ~b $ = '(syla inot h); -theorem mpand (h1: $ a -> b $) (h2: $ a /\ b -> c $): $ a -> c $ = '(mpd h1 (exp h2)); -theorem mtand (h1: $ a -> ~b $) (h2: $ a /\ c -> b $): $ a -> ~c $ = '(mtd h1 (exp h2)); -theorem mtani (h1: $ ~b $) (h2: $ a /\ c -> b $): $ a -> ~c $ = '(mtand (a1i h1) h2); - -theorem bi1: $ (a <-> b) -> a -> b $ = 'anl; -theorem bi1i (h: $ a <-> b $): $ a -> b $ = '(bi1 h); -theorem bi1d (h: $ a -> (b <-> c) $): $ a -> b -> c $ = '(syl bi1 h); -theorem bi1a (h: $ a -> (b <-> c) $): $ a /\ b -> c $ = '(curry @ bi1d h); -theorem bi2: $ (a <-> b) -> b -> a $ = 'anr; -theorem bi2i (h: $ a <-> b $): $ b -> a $ = '(bi2 h); -theorem bi2d (h: $ a -> (b <-> c) $): $ a -> c -> b $ = '(syl bi2 h); -theorem bi2a (h: $ a -> (b <-> c) $): $ a /\ c -> b $ = '(curry @ bi2d h); -theorem ibii (h1: $ a -> b $) (h2: $ b -> a $): $ a <-> b $ = '(iani h1 h2); -theorem ibid (h1: $ a -> b -> c $) (h2: $ a -> c -> b $): $ a -> (b <-> c) $ = '(iand h1 h2); -theorem ibida (h1: $ a /\ b -> c $) (h2: $ a /\ c -> b $): $ a -> (b <-> c) $ = '(ibid (exp h1) (exp h2)); -theorem biid: $ a <-> a $ = '(ibii id id); -theorem biidd: $ a -> (b <-> b) $ = '(a1i biid); -theorem mpbi (h1: $ a <-> b $) (h2: $ a $): $ b $ = '(bi1i h1 h2); -theorem mpbir (h1: $ b <-> a $) (h2: $ a $): $ b $ = '(bi2i h1 h2); -theorem mpbid (h1: $ a -> (b <-> c) $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (bi1d h1)); -theorem mpbird (h1: $ a -> (c <-> b) $) (h2: $ a -> b $): $ a -> c $ = '(mpd h2 (bi2d h1)); -theorem mpbii (h1: $ b $) (h2: $ a -> (b <-> c) $): $ a -> c $ = '(mpbid h2 (a1i h1)); -theorem mpbiri (h1: $ b $) (h2: $ a -> (c <-> b) $): $ a -> c $ = '(mpbird h2 (a1i h1)); -theorem mtbi (h1: $ a <-> b $) (h2: $ ~a $): $ ~b $ = '(mt (bi2 h1) h2); -theorem mtbir (h1: $ b <-> a $) (h2: $ ~a $): $ ~b $ = '(mt (bi1 h1) h2); -theorem mtbid (h1: $ a -> (b <-> c) $) (h2: $ a -> ~b $): $ a -> ~c $ = '(mtd h2 (bi2d h1)); -theorem mtbird (h1: $ a -> (c <-> b) $) (h2: $ a -> ~b $): $ a -> ~c $ = '(mtd h2 (bi1d h1)); -theorem con1b: $ (~a <-> b) -> (~b <-> a) $ = '(ibid (con1d bi1) (con2d bi2)); -theorem con2b: $ (a <-> ~b) -> (b <-> ~a) $ = '(ibid (con2d bi1) (con1d bi2)); -theorem con3b: $ (a <-> b) -> (~a <-> ~b) $ = '(ibid (con3d bi2) (con3d bi1)); -theorem con4b: $ (~a <-> ~b) -> (a <-> b) $ = '(ibid (con4d bi2) (con4d bi1)); -theorem con1bb: $ (~a <-> b) <-> (~b <-> a) $ = '(ibii con1b con1b); -theorem con2bb: $ (a <-> ~b) <-> (b <-> ~a) $ = '(ibii con2b con2b); -theorem con3bb: $ (a <-> b) <-> (~a <-> ~b) $ = '(ibii con3b con4b); -theorem con1bi: $ (~a -> b) <-> (~b -> a) $ = '(ibii con1 con1); -theorem con2bi: $ (a -> ~b) <-> (b -> ~a) $ = '(ibii con2 con2); -theorem con3bi: $ (a -> b) <-> (~b -> ~a) $ = '(ibii con3 prop_3); -theorem notnot: $ a <-> ~~a $ = '(ibii notnot1 dne); -theorem bithd (h1: $ a -> b $) (h2: $ a -> c $): $ a -> (b <-> c) $ = '(ibid (a1d h2) (a1d h1)); -theorem binthd (h1: $ a -> ~b $) (h2: $ a -> ~c $): $ a -> (b <-> c) $ = '(syl con4b @ bithd h1 h2); -theorem bith: $ a -> b -> (a <-> b) $ = '(exp @ bithd anl anr); -theorem binth: $ ~a -> ~b -> (a <-> b) $ = '(exp @ binthd anl anr); -theorem bicom: $ (a <-> b) -> (b <-> a) $ = '(ibid bi2 bi1); -theorem bicomb: $ (a <-> b) <-> (b <-> a) $ = '(ibii bicom bicom); -theorem bicomd (h: $ a -> (b <-> c) $): $ a -> (c <-> b) $ = '(syl bicom h); -theorem bitrd (h1: $ a -> (b <-> c) $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = +theorem inotda (h: $ aa /\ bb -> ~bb $): $ aa -> ~bb $ = '(syla inot h); +theorem mpand (h1: $ aa -> bb $) (h2: $ aa /\ bb -> c $): $ aa -> c $ = '(mpd h1 (exp h2)); +theorem mtand (h1: $ aa -> ~bb $) (h2: $ aa /\ c -> bb $): $ aa -> ~c $ = '(mtd h1 (exp h2)); +theorem mtani (h1: $ ~bb $) (h2: $ aa /\ c -> bb $): $ aa -> ~c $ = '(mtand (a1i h1) h2); + +theorem bi1: $ (aa <-> bb) -> aa -> bb $ = 'anl; +theorem bi1i (h: $ aa <-> bb $): $ aa -> bb $ = '(bi1 h); +theorem bi1d (h: $ aa -> (bb <-> c) $): $ aa -> bb -> c $ = '(syl bi1 h); +theorem bi1a (h: $ aa -> (bb <-> c) $): $ aa /\ bb -> c $ = '(curry @ bi1d h); +theorem bi2: $ (aa <-> bb) -> bb -> aa $ = 'anr; +theorem bi2i (h: $ aa <-> bb $): $ bb -> aa $ = '(bi2 h); +theorem bi2d (h: $ aa -> (bb <-> c) $): $ aa -> c -> bb $ = '(syl bi2 h); +theorem bi2a (h: $ aa -> (bb <-> c) $): $ aa /\ c -> bb $ = '(curry @ bi2d h); +theorem ibii (h1: $ aa -> bb $) (h2: $ bb -> aa $): $ aa <-> bb $ = '(iani h1 h2); +theorem ibid (h1: $ aa -> bb -> c $) (h2: $ aa -> c -> bb $): $ aa -> (bb <-> c) $ = '(iand h1 h2); +theorem ibida (h1: $ aa /\ bb -> c $) (h2: $ aa /\ c -> bb $): $ aa -> (bb <-> c) $ = '(ibid (exp h1) (exp h2)); +theorem biid: $ aa <-> aa $ = '(ibii id id); +theorem biidd: $ aa -> (bb <-> bb) $ = '(a1i biid); +theorem mpbi (h1: $ aa <-> bb $) (h2: $ aa $): $ bb $ = '(bi1i h1 h2); +theorem mpbir (h1: $ bb <-> aa $) (h2: $ aa $): $ bb $ = '(bi2i h1 h2); +theorem mpbid (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> bb $): $ aa -> c $ = '(mpd h2 (bi1d h1)); +theorem mpbird (h1: $ aa -> (c <-> bb) $) (h2: $ aa -> bb $): $ aa -> c $ = '(mpd h2 (bi2d h1)); +theorem mpbii (h1: $ bb $) (h2: $ aa -> (bb <-> c) $): $ aa -> c $ = '(mpbid h2 (a1i h1)); +theorem mpbiri (h1: $ bb $) (h2: $ aa -> (c <-> bb) $): $ aa -> c $ = '(mpbird h2 (a1i h1)); +theorem mtbi (h1: $ aa <-> bb $) (h2: $ ~aa $): $ ~bb $ = '(mt (bi2 h1) h2); +theorem mtbir (h1: $ bb <-> aa $) (h2: $ ~aa $): $ ~bb $ = '(mt (bi1 h1) h2); +theorem mtbid (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> ~bb $): $ aa -> ~c $ = '(mtd h2 (bi2d h1)); +theorem mtbird (h1: $ aa -> (c <-> bb) $) (h2: $ aa -> ~bb $): $ aa -> ~c $ = '(mtd h2 (bi1d h1)); +theorem con1b: $ (~aa <-> bb) -> (~bb <-> aa) $ = '(ibid (con1d bi1) (con2d bi2)); +theorem con2b: $ (aa <-> ~bb) -> (bb <-> ~aa) $ = '(ibid (con2d bi1) (con1d bi2)); +theorem con3b: $ (aa <-> bb) -> (~aa <-> ~bb) $ = '(ibid (con3d bi2) (con3d bi1)); +theorem con4b: $ (~aa <-> ~bb) -> (aa <-> bb) $ = '(ibid (con4d bi2) (con4d bi1)); +theorem con1bb: $ (~aa <-> bb) <-> (~bb <-> aa) $ = '(ibii con1b con1b); +theorem con2bb: $ (aa <-> ~bb) <-> (bb <-> ~aa) $ = '(ibii con2b con2b); +theorem con3bb: $ (aa <-> bb) <-> (~aa <-> ~bb) $ = '(ibii con3b con4b); +theorem con1bi: $ (~aa -> bb) <-> (~bb -> aa) $ = '(ibii con1 con1); +theorem con2bi: $ (aa -> ~bb) <-> (bb -> ~aa) $ = '(ibii con2 con2); +theorem con3bi: $ (aa -> bb) <-> (~bb -> ~aa) $ = '(ibii con3 prop_3); +theorem notnot: $ aa <-> ~~aa $ = '(ibii notnot1 dne); +theorem bithd (h1: $ aa -> bb $) (h2: $ aa -> c $): $ aa -> (bb <-> c) $ = '(ibid (a1d h2) (a1d h1)); +theorem binthd (h1: $ aa -> ~bb $) (h2: $ aa -> ~c $): $ aa -> (bb <-> c) $ = '(syl con4b @ bithd h1 h2); +theorem bith: $ aa -> bb -> (aa <-> bb) $ = '(exp @ bithd anl anr); +theorem binth: $ ~aa -> ~bb -> (aa <-> bb) $ = '(exp @ binthd anl anr); +theorem bicom: $ (aa <-> bb) -> (bb <-> aa) $ = '(ibid bi2 bi1); +theorem bicomb: $ (aa <-> bb) <-> (bb <-> aa) $ = '(ibii bicom bicom); +theorem bicomd (h: $ aa -> (bb <-> c) $): $ aa -> (c <-> bb) $ = '(syl bicom h); +theorem bitrd (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (c <-> d) $): $ aa -> (bb <-> d) $ = '(ibid (syld (bi1d h1) (bi1d h2)) (syld (bi2d h2) (bi2d h1))); -theorem bitr2d (h1: $ a -> (b <-> c) $) (h2: $ a -> (c <-> d) $): $ a -> (d <-> b) $ = '(bicomd (bitrd h1 h2)); -theorem bitr3d (h1: $ a -> (c <-> b) $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(bitrd (bicomd h1) h2); -theorem bitr4d (h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> c) $): $ a -> (b <-> d) $ = '(bitrd h1 (bicomd h2)); -theorem bitr: $ (a <-> b) -> (b <-> c) -> (a <-> c) $ = '(exp (bitrd anl anr)); -theorem bitr2: $ (a <-> b) -> (b <-> c) -> (c <-> a) $ = '(exp (bitr2d anl anr)); -theorem bitr3: $ (b <-> a) -> (b <-> c) -> (a <-> c) $ = '(exp (bitr3d anl anr)); -theorem bitr4: $ (a <-> b) -> (c <-> b) -> (a <-> c) $ = '(exp (bitr4d anl anr)); -theorem bisylr: $ (c <-> b) -> (a <-> b) -> (a <-> c) $ = '(rsyl bicom @ com23 id bitr); -theorem sylib (h1: $ b <-> c $) (h2: $ a -> b $): $ a -> c $ = '(syl (bi1i h1) h2); -theorem sylibr (h1: $ c <-> b $) (h2: $ a -> b $): $ a -> c $ = '(syl (bi2i h1) h2); -theorem sylbi (h1: $ a <-> b $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 (bi1i h1)); -theorem sylbir (h1: $ b <-> a $) (h2: $ b -> c $): $ a -> c $ = '(syl h2 (bi2i h1)); -theorem syl5bb (h1: $ b <-> c $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(bitrd (a1i h1) h2); -theorem syl5bbr (h1: $ c <-> b $) (h2: $ a -> (c <-> d) $): $ a -> (b <-> d) $ = '(syl5bb (bicom h1) h2); -theorem syl6bb (h1: $ c <-> d $) (h2: $ a -> (b <-> c) $): $ a -> (b <-> d) $ = '(bitrd h2 (a1i h1)); -theorem syl6bbr (h1: $ d <-> c $) (h2: $ a -> (b <-> c) $): $ a -> (b <-> d) $ = '(syl6bb (bicom h1) h2); -theorem syl5bi (h1: $ b <-> c $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syl5 (bi1 h1) h2); -theorem syl5bir (h1: $ c <-> b $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syl5bi (bicom h1) h2); -theorem syl6ib (h1: $ c <-> d $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syl6 (bi1 h1) h2); -theorem syl6ibr (h1: $ d <-> c $) (h2: $ a -> b -> c $): $ a -> b -> d $ = '(syl6 (bi2 h1) h2); -theorem syl5ibrcom (h1: $ c -> (b <-> d) $) (h2: $ a -> d $): $ a -> c -> b $ = '(com12 @ syl5 h2 (bi2d h1)); -theorem sylbid (h1: $ a -> (b <-> c) $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (bi1d h1) h2); -theorem sylibd (h1: $ a -> b -> c $) (h2: $ a -> (c <-> d) $): $ a -> b -> d $ = '(syld h1 (bi1d h2)); -theorem sylbird (h1: $ a -> (c <-> b) $) (h2: $ a -> c -> d $): $ a -> b -> d $ = '(syld (bi2d h1) h2); -theorem sylibrd (h1: $ a -> b -> c $) (h2: $ a -> (d <-> c) $): $ a -> b -> d $ = '(syld h1 (bi2d h2)); -theorem bitr3g (h1: $ b <-> d $) (h2: $ c <-> e $) (h: $ a -> (b <-> c) $): - $ a -> (d <-> e) $ = '(syl5bb (bicom h1) @ syl6bb h2 h); -theorem bitr4g (h1: $ d <-> b $) (h2: $ e <-> c $) (h: $ a -> (b <-> c) $): - $ a -> (d <-> e) $ = '(syl5bb h1 @ syl6bb (bicom h2) h); -theorem bitr3gi (h1: $ a <-> c $) (h2: $ b <-> d $) (h: $ a <-> b $): $ c <-> d $ = '(bitr3 h1 @ bitr h h2); -theorem bitr4gi (h1: $ c <-> a $) (h2: $ d <-> b $) (h: $ a <-> b $): $ c <-> d $ = '(bitr h1 @ bitr4 h h2); -theorem impbi (h: $ a -> (b <-> c) $): $ a /\ b -> c $ = '(curry @ bi1d h); -theorem impbir (h: $ a -> (c <-> b) $): $ a /\ b -> c $ = '(curry @ bi2d h); -theorem ancomb: $ a /\ b <-> b /\ a $ = '(ibii ancom ancom); -theorem anass: $ a /\ b /\ c <-> a /\ (b /\ c) $ = +theorem bitr2d (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (c <-> d) $): $ aa -> (d <-> bb) $ = '(bicomd (bitrd h1 h2)); +theorem bitr3d (h1: $ aa -> (c <-> bb) $) (h2: $ aa -> (c <-> d) $): $ aa -> (bb <-> d) $ = '(bitrd (bicomd h1) h2); +theorem bitr4d (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (d <-> c) $): $ aa -> (bb <-> d) $ = '(bitrd h1 (bicomd h2)); +theorem bitr: $ (aa <-> bb) -> (bb <-> c) -> (aa <-> c) $ = '(exp (bitrd anl anr)); +theorem bitr2: $ (aa <-> bb) -> (bb <-> c) -> (c <-> aa) $ = '(exp (bitr2d anl anr)); +theorem bitr3: $ (bb <-> aa) -> (bb <-> c) -> (aa <-> c) $ = '(exp (bitr3d anl anr)); +theorem bitr4: $ (aa <-> bb) -> (c <-> bb) -> (aa <-> c) $ = '(exp (bitr4d anl anr)); +theorem bisylr: $ (c <-> bb) -> (aa <-> bb) -> (aa <-> c) $ = '(rsyl bicom @ com23 id bitr); +theorem sylib (h1: $ bb <-> c $) (h2: $ aa -> bb $): $ aa -> c $ = '(syl (bi1i h1) h2); +theorem sylibr (h1: $ c <-> bb $) (h2: $ aa -> bb $): $ aa -> c $ = '(syl (bi2i h1) h2); +theorem sylbi (h1: $ aa <-> bb $) (h2: $ bb -> c $): $ aa -> c $ = '(syl h2 (bi1i h1)); +theorem sylbir (h1: $ bb <-> aa $) (h2: $ bb -> c $): $ aa -> c $ = '(syl h2 (bi2i h1)); +theorem syl5bb (h1: $ bb <-> c $) (h2: $ aa -> (c <-> d) $): $ aa -> (bb <-> d) $ = '(bitrd (a1i h1) h2); +theorem syl5bbr (h1: $ c <-> bb $) (h2: $ aa -> (c <-> d) $): $ aa -> (bb <-> d) $ = '(syl5bb (bicom h1) h2); +theorem syl6bb (h1: $ c <-> d $) (h2: $ aa -> (bb <-> c) $): $ aa -> (bb <-> d) $ = '(bitrd h2 (a1i h1)); +theorem syl6bbr (h1: $ d <-> c $) (h2: $ aa -> (bb <-> c) $): $ aa -> (bb <-> d) $ = '(syl6bb (bicom h1) h2); +theorem syl5bi (h1: $ bb <-> c $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(syl5 (bi1 h1) h2); +theorem syl5bir (h1: $ c <-> bb $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(syl5bi (bicom h1) h2); +theorem syl6ib (h1: $ c <-> d $) (h2: $ aa -> bb -> c $): $ aa -> bb -> d $ = '(syl6 (bi1 h1) h2); +theorem syl6ibr (h1: $ d <-> c $) (h2: $ aa -> bb -> c $): $ aa -> bb -> d $ = '(syl6 (bi2 h1) h2); +theorem syl5ibrcom (h1: $ c -> (bb <-> d) $) (h2: $ aa -> d $): $ aa -> c -> bb $ = '(com12 @ syl5 h2 (bi2d h1)); +theorem sylbid (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(syld (bi1d h1) h2); +theorem sylibd (h1: $ aa -> bb -> c $) (h2: $ aa -> (c <-> d) $): $ aa -> bb -> d $ = '(syld h1 (bi1d h2)); +theorem sylbird (h1: $ aa -> (c <-> bb) $) (h2: $ aa -> c -> d $): $ aa -> bb -> d $ = '(syld (bi2d h1) h2); +theorem sylibrd (h1: $ aa -> bb -> c $) (h2: $ aa -> (d <-> c) $): $ aa -> bb -> d $ = '(syld h1 (bi2d h2)); +theorem bitr3g (h1: $ bb <-> d $) (h2: $ c <-> e $) (h: $ aa -> (bb <-> c) $): + $ aa -> (d <-> e) $ = '(syl5bb (bicom h1) @ syl6bb h2 h); +theorem bitr4g (h1: $ d <-> bb $) (h2: $ e <-> c $) (h: $ aa -> (bb <-> c) $): + $ aa -> (d <-> e) $ = '(syl5bb h1 @ syl6bb (bicom h2) h); +theorem bitr3gi (h1: $ aa <-> c $) (h2: $ bb <-> d $) (h: $ aa <-> bb $): $ c <-> d $ = '(bitr3 h1 @ bitr h h2); +theorem bitr4gi (h1: $ c <-> aa $) (h2: $ d <-> bb $) (h: $ aa <-> bb $): $ c <-> d $ = '(bitr h1 @ bitr4 h h2); +theorem impbi (h: $ aa -> (bb <-> c) $): $ aa /\ bb -> c $ = '(curry @ bi1d h); +theorem impbir (h: $ aa -> (c <-> bb) $): $ aa /\ bb -> c $ = '(curry @ bi2d h); +theorem ancomb: $ aa /\ bb <-> bb /\ aa $ = '(ibii ancom ancom); +theorem anass: $ aa /\ bb /\ c <-> aa /\ (bb /\ c) $ = '(ibii (iand anll (anim1 anr)) (iand (anim2 anl) anrr)); -theorem bian2a: $ (a -> b) -> (a /\ b <-> a) $ = '(ibid (a1i anl) (a2i ian)); -theorem bian1a: $ (b -> a) -> (a /\ b <-> b) $ = '(syl5bb ancomb bian2a); -theorem bian1: $ a -> (a /\ b <-> b) $ = '(syl bian1a prop_1); -theorem bian2: $ b -> (a /\ b <-> a) $ = '(syl bian2a prop_1); -theorem bibi1: $ a -> ((a <-> b) <-> b) $ = '(ibid (com12 bi1) bith); -theorem bibi2: $ b -> ((a <-> b) <-> a) $ = '(syl5bb bicomb bibi1); -theorem noteq: $ (a <-> b) -> (~a <-> ~b) $ = 'con3b; -theorem noteqi (h: $ a <-> b $): $ ~a <-> ~b $ = '(noteq h); -theorem noteqd (h: $ a -> (b <-> c) $): $ a -> (~b <-> ~c) $ = '(syl noteq h); +theorem bian2a: $ (aa -> bb) -> (aa /\ bb <-> aa) $ = '(ibid (a1i anl) (a2i ian)); +theorem bian1a: $ (bb -> aa) -> (aa /\ bb <-> bb) $ = '(syl5bb ancomb bian2a); +theorem bian1: $ aa -> (aa /\ bb <-> bb) $ = '(syl bian1a prop_1); +theorem bian2: $ bb -> (aa /\ bb <-> aa) $ = '(syl bian2a prop_1); +theorem bibi1: $ aa -> ((aa <-> bb) <-> bb) $ = '(ibid (com12 bi1) bith); +theorem bibi2: $ bb -> ((aa <-> bb) <-> aa) $ = '(syl5bb bicomb bibi1); +theorem noteq: $ (aa <-> bb) -> (~aa <-> ~bb) $ = 'con3b; +theorem noteqi (h: $ aa <-> bb $): $ ~aa <-> ~bb $ = '(noteq h); +theorem noteqd (h: $ aa -> (bb <-> c) $): $ aa -> (~bb <-> ~c) $ = '(syl noteq h); theorem imeqd - (h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> (b -> d <-> c -> e) $ = + (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (d <-> e) $): $ aa -> (bb -> d <-> c -> e) $ = '(ibid (imimd (bi2d h1) (bi1d h2)) (imimd (bi1d h1) (bi2d h2))); -theorem bibin1: $ ~a -> ((a <-> b) <-> ~b) $ = '(ibid (com12 @ bi1d noteq) binth); -theorem bibin2: $ ~b -> ((a <-> b) <-> ~a) $ = '(syl5bb bicomb bibin1); -theorem imeq1d (h: $ a -> (b <-> c) $): $ a -> (b -> d <-> c -> d) $ = '(imeqd h biidd); -theorem imeq2d (h: $ a -> (c <-> d) $): $ a -> (b -> c <-> b -> d) $ = '(imeqd biidd h); -theorem imeq1i (h: $ a <-> b $): $ a -> c <-> b -> c $ = '(imeq1d id h); -theorem imeq2i (h: $ b <-> c $): $ a -> b <-> a -> c $ = '(imeq2d id h); -theorem imeqi (h1: $ a <-> b $) (h2: $ c <-> d $): $ a -> c <-> b -> d $ = '(bitr (imeq1i h1) (imeq2i h2)); +theorem bibin1: $ ~aa -> ((aa <-> bb) <-> ~bb) $ = '(ibid (com12 @ bi1d noteq) binth); +theorem bibin2: $ ~bb -> ((aa <-> bb) <-> ~aa) $ = '(syl5bb bicomb bibin1); +theorem imeq1d (h: $ aa -> (bb <-> c) $): $ aa -> (bb -> d <-> c -> d) $ = '(imeqd h biidd); +theorem imeq2d (h: $ aa -> (c <-> d) $): $ aa -> (bb -> c <-> bb -> d) $ = '(imeqd biidd h); +theorem imeq1i (h: $ aa <-> bb $): $ aa -> c <-> bb -> c $ = '(imeq1d id h); +theorem imeq2i (h: $ bb <-> c $): $ aa -> bb <-> aa -> c $ = '(imeq2d id h); +theorem imeqi (h1: $ aa <-> bb $) (h2: $ c <-> d $): $ aa -> c <-> bb -> d $ = '(bitr (imeq1i h1) (imeq2i h2)); theorem aneqd - (h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> (b /\ d <-> c /\ e) $ = + (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (d <-> e) $): $ aa -> (bb /\ d <-> c /\ e) $ = '(ibid (animd (bi1d h1) (bi1d h2)) (animd (bi2d h1) (bi2d h2))); -theorem imeq2a: $ (a -> (b <-> c)) -> (a -> b <-> a -> c) $ = '(ibid (a2d @ imim2i bi1) (a2d @ imim2i bi2)); -theorem imeq1a: $ (~c -> (a <-> b)) -> (a -> c <-> b -> c) $ = '(bitr4g con3bi con3bi @ syl imeq2a @ imim2i noteq); -theorem imeq2da (h: $ G /\ a -> (b <-> c) $): $ G -> (a -> b <-> a -> c) $ = '(syl imeq2a @ exp h); -theorem aneq1d (h: $ a -> (b <-> c) $): $ a -> (b /\ d <-> c /\ d) $ = '(aneqd h biidd); -theorem aneq2d (h: $ a -> (c <-> d) $): $ a -> (b /\ c <-> b /\ d) $ = '(aneqd biidd h); -theorem aneq: $ (a <-> b) -> (c <-> d) -> (a /\ c <-> b /\ d) $ = '(exp @ aneqd anl anr); -theorem aneq1i (h: $ a <-> b $): $ a /\ c <-> b /\ c $ = '(aneq1d id h); -theorem aneq2i (h: $ b <-> c $): $ a /\ b <-> a /\ c $ = '(aneq2d id h); -theorem aneq2a: $ (a -> (b <-> c)) -> (a /\ b <-> a /\ c) $ = +theorem imeq2a: $ (aa -> (bb <-> c)) -> (aa -> bb <-> aa -> c) $ = '(ibid (a2d @ imim2i bi1) (a2d @ imim2i bi2)); +theorem imeq1a: $ (~c -> (aa <-> bb)) -> (aa -> c <-> bb -> c) $ = '(bitr4g con3bi con3bi @ syl imeq2a @ imim2i noteq); +theorem imeq2da (h: $ G /\ aa -> (bb <-> c) $): $ G -> (aa -> bb <-> aa -> c) $ = '(syl imeq2a @ exp h); +theorem aneq1d (h: $ aa -> (bb <-> c) $): $ aa -> (bb /\ d <-> c /\ d) $ = '(aneqd h biidd); +theorem aneq2d (h: $ aa -> (c <-> d) $): $ aa -> (bb /\ c <-> bb /\ d) $ = '(aneqd biidd h); +theorem aneq: $ (aa <-> bb) -> (c <-> d) -> (aa /\ c <-> bb /\ d) $ = '(exp @ aneqd anl anr); +theorem aneq1i (h: $ aa <-> bb $): $ aa /\ c <-> bb /\ c $ = '(aneq1d id h); +theorem aneq2i (h: $ bb <-> c $): $ aa /\ bb <-> aa /\ c $ = '(aneq2d id h); +theorem aneq2a: $ (aa -> (bb <-> c)) -> (aa /\ bb <-> aa /\ c) $ = '(ibid (syl anim2a @ imim2i bi1) (syl anim2a @ imim2i bi2)); -theorem aneq1a: $ (c -> (a <-> b)) -> (a /\ c <-> b /\ c) $ = '(syl5bb ancomb @ syl6bb ancomb aneq2a); -theorem aneq1da (h: $ G /\ c -> (a <-> b) $): $ G -> (a /\ c <-> b /\ c) $ = '(syl aneq1a @ exp h); -theorem aneq2da (h: $ G /\ a -> (b <-> c) $): $ G -> (a /\ b <-> a /\ c) $ = '(syl aneq2a @ exp h); -theorem anlass: $ a /\ (b /\ c) <-> b /\ (a /\ c) $ = +theorem aneq1a: $ (c -> (aa <-> bb)) -> (aa /\ c <-> bb /\ c) $ = '(syl5bb ancomb @ syl6bb ancomb aneq2a); +theorem aneq1da (h: $ G /\ c -> (aa <-> bb) $): $ G -> (aa /\ c <-> bb /\ c) $ = '(syl aneq1a @ exp h); +theorem aneq2da (h: $ G /\ aa -> (bb <-> c) $): $ G -> (aa /\ bb <-> aa /\ c) $ = '(syl aneq2a @ exp h); +theorem anlass: $ aa /\ (bb /\ c) <-> bb /\ (aa /\ c) $ = '(bitr3 anass @ bitr (aneq1i ancomb) anass); -theorem anrass: $ a /\ b /\ c <-> a /\ c /\ b $ = +theorem anrass: $ aa /\ bb /\ c <-> aa /\ c /\ bb $ = '(bitr anass @ bitr4 (aneq2i ancomb) anass); -theorem an4: $ (a /\ b) /\ (c /\ d) <-> (a /\ c) /\ (b /\ d) $ = +theorem an4: $ (aa /\ bb) /\ (c /\ d) <-> (aa /\ c) /\ (bb /\ d) $ = '(bitr4 anass @ bitr4 anass @ aneq2i anlass); -theorem anroti (h: $ a -> b /\ d $): $ a /\ c -> b /\ c /\ d $ = '(sylib anrass @ anim1 h); -theorem anrotri (h: $ b /\ d -> a $): $ b /\ c /\ d -> a /\ c $ = '(sylbi anrass @ anim1 h); -theorem bian11i (h: $ a <-> b /\ c $): $ a /\ d <-> b /\ (c /\ d) $ = '(bitr (aneq1i h) anass); -theorem bian21i (h: $ a <-> b /\ c $): $ a /\ d <-> (b /\ d) /\ c $ = '(bitr (aneq1i h) anrass); -theorem bian12i (h: $ a <-> b /\ c $): $ d /\ a <-> b /\ (d /\ c) $ = '(bitr (aneq2i h) anlass); -theorem bian22i (h: $ a <-> b /\ c $): $ d /\ a <-> (d /\ b) /\ c $ = '(bitr4 (aneq2i h) anass); -theorem bian11d (h: $ G -> (a <-> b /\ c) $): $ G -> (a /\ d <-> b /\ (c /\ d)) $ = '(syl6bb anass (aneq1d h)); -theorem bian21d (h: $ G -> (a <-> b /\ c) $): $ G -> (a /\ d <-> (b /\ d) /\ c) $ = '(syl6bb anrass (aneq1d h)); -theorem bian12d (h: $ G -> (a <-> b /\ c) $): $ G -> (d /\ a <-> b /\ (d /\ c)) $ = '(syl6bb anlass (aneq2d h)); -theorem bian22d (h: $ G -> (a <-> b /\ c) $): $ G -> (d /\ a <-> (d /\ b) /\ c) $ = '(syl6bbr anass (aneq2d h)); -theorem bian11da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (a /\ d <-> b /\ (c /\ d)) $ = '(syl6bb anass (aneq1da h)); -theorem bian21da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (a /\ d <-> (b /\ d) /\ c) $ = '(syl6bb anrass (aneq1da h)); -theorem bian12da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (d /\ a <-> b /\ (d /\ c)) $ = '(syl6bb anlass (aneq2da h)); -theorem bian22da (h: $ G /\ d -> (a <-> b /\ c) $): $ G -> (d /\ a <-> (d /\ b) /\ c) $ = '(syl6bbr anass (aneq2da h)); -theorem anidm: $ a /\ a <-> a $ = '(ibii anl (iand id id)); -theorem anandi: $ a /\ (b /\ c) <-> (a /\ b) /\ (a /\ c) $ = '(bitr3 (aneq1i anidm) an4); -theorem anandir: $ (a /\ b) /\ c <-> (a /\ c) /\ (b /\ c) $ = '(bitr3 (aneq2i anidm) an4); -theorem imandi: $ (a -> b /\ c) <-> (a -> b) /\ (a -> c) $ = +theorem anroti (h: $ aa -> bb /\ d $): $ aa /\ c -> bb /\ c /\ d $ = '(sylib anrass @ anim1 h); +theorem anrotri (h: $ bb /\ d -> aa $): $ bb /\ c /\ d -> aa /\ c $ = '(sylbi anrass @ anim1 h); +theorem bian11i (h: $ aa <-> bb /\ c $): $ aa /\ d <-> bb /\ (c /\ d) $ = '(bitr (aneq1i h) anass); +theorem bian21i (h: $ aa <-> bb /\ c $): $ aa /\ d <-> (bb /\ d) /\ c $ = '(bitr (aneq1i h) anrass); +theorem bian12i (h: $ aa <-> bb /\ c $): $ d /\ aa <-> bb /\ (d /\ c) $ = '(bitr (aneq2i h) anlass); +theorem bian22i (h: $ aa <-> bb /\ c $): $ d /\ aa <-> (d /\ bb) /\ c $ = '(bitr4 (aneq2i h) anass); +theorem bian11d (h: $ G -> (aa <-> bb /\ c) $): $ G -> (aa /\ d <-> bb /\ (c /\ d)) $ = '(syl6bb anass (aneq1d h)); +theorem bian21d (h: $ G -> (aa <-> bb /\ c) $): $ G -> (aa /\ d <-> (bb /\ d) /\ c) $ = '(syl6bb anrass (aneq1d h)); +theorem bian12d (h: $ G -> (aa <-> bb /\ c) $): $ G -> (d /\ aa <-> bb /\ (d /\ c)) $ = '(syl6bb anlass (aneq2d h)); +theorem bian22d (h: $ G -> (aa <-> bb /\ c) $): $ G -> (d /\ aa <-> (d /\ bb) /\ c) $ = '(syl6bbr anass (aneq2d h)); +theorem bian11da (h: $ G /\ d -> (aa <-> bb /\ c) $): $ G -> (aa /\ d <-> bb /\ (c /\ d)) $ = '(syl6bb anass (aneq1da h)); +theorem bian21da (h: $ G /\ d -> (aa <-> bb /\ c) $): $ G -> (aa /\ d <-> (bb /\ d) /\ c) $ = '(syl6bb anrass (aneq1da h)); +theorem bian12da (h: $ G /\ d -> (aa <-> bb /\ c) $): $ G -> (d /\ aa <-> bb /\ (d /\ c)) $ = '(syl6bb anlass (aneq2da h)); +theorem bian22da (h: $ G /\ d -> (aa <-> bb /\ c) $): $ G -> (d /\ aa <-> (d /\ bb) /\ c) $ = '(syl6bbr anass (aneq2da h)); +theorem anidm: $ aa /\ aa <-> aa $ = '(ibii anl (iand id id)); +theorem anandi: $ aa /\ (bb /\ c) <-> (aa /\ bb) /\ (aa /\ c) $ = '(bitr3 (aneq1i anidm) an4); +theorem anandir: $ (aa /\ bb) /\ c <-> (aa /\ c) /\ (bb /\ c) $ = '(bitr3 (aneq2i anidm) an4); +theorem imandi: $ (aa -> bb /\ c) <-> (aa -> bb) /\ (aa -> c) $ = '(ibii (iand (imim2i anl) (imim2i anr)) (com12 @ animd mpcom mpcom)); -theorem imancom: $ a /\ (b -> c) -> b -> a /\ c $ = '(com12 @ anim2d mpcom); -theorem rbida (h1: $ a /\ c -> b $) (h2: $ a /\ d -> b $) - (h: $ a /\ b -> (c <-> d) $): $ a -> (c <-> d) $ = +theorem imancom: $ aa /\ (bb -> c) -> bb -> aa /\ c $ = '(com12 @ anim2d mpcom); +theorem rbida (h1: $ aa /\ c -> bb $) (h2: $ aa /\ d -> bb $) + (h: $ aa /\ bb -> (c <-> d) $): $ aa -> (c <-> d) $ = '(bitr3d (syla bian2a h1) @ bitrd (syla aneq1a h) (syla bian2a h2)); -theorem rbid (h1: $ b -> a $) (h2: $ c -> a $) (h: $ a -> (b <-> c) $): $ b <-> c $ = +theorem rbid (h1: $ bb -> aa $) (h2: $ c -> aa $) (h: $ aa -> (bb <-> c) $): $ bb <-> c $ = '(bitr3 (bian2a h1) @ bitr (aneq1a h) (bian2a h2)); theorem bieqd - (h1: $ a -> (b <-> c) $) (h2: $ a -> (d <-> e) $): $ a -> ((b <-> d) <-> (c <-> e)) $ = + (h1: $ aa -> (bb <-> c) $) (h2: $ aa -> (d <-> e) $): $ aa -> ((bb <-> d) <-> (c <-> e)) $ = '(aneqd (imeqd h1 h2) (imeqd h2 h1)); -theorem bieq1d (h: $ a -> (b <-> c) $): $ a -> ((b <-> d) <-> (c <-> d)) $ = '(bieqd h biidd); -theorem bieq2d (h: $ a -> (c <-> d) $): $ a -> ((b <-> c) <-> (b <-> d)) $ = '(bieqd biidd h); -theorem bieq: $ (a <-> b) -> (c <-> d) -> ((a <-> c) <-> (b <-> d)) $ = '(exp (bieqd anl anr)); -theorem bieq1: $ (a <-> b) -> ((a <-> c) <-> (b <-> c)) $ = '(bieq1d id); -theorem bieq2: $ (b <-> c) -> ((a <-> b) <-> (a <-> c)) $ = '(bieq2d id); -theorem impexp: $ (a /\ b -> c) <-> (a -> b -> c) $ = +theorem bieq1d (h: $ aa -> (bb <-> c) $): $ aa -> ((bb <-> d) <-> (c <-> d)) $ = '(bieqd h biidd); +theorem bieq2d (h: $ aa -> (c <-> d) $): $ aa -> ((bb <-> c) <-> (bb <-> d)) $ = '(bieqd biidd h); +theorem bieq: $ (aa <-> bb) -> (c <-> d) -> ((aa <-> c) <-> (bb <-> d)) $ = '(exp (bieqd anl anr)); +theorem bieq1: $ (aa <-> bb) -> ((aa <-> c) <-> (bb <-> c)) $ = '(bieq1d id); +theorem bieq2: $ (bb <-> c) -> ((aa <-> bb) <-> (aa <-> c)) $ = '(bieq2d id); +theorem impexp: $ (aa /\ bb -> c) <-> (aa -> bb -> c) $ = '(ibii (exp @ exp @ mpd (anim1 anr) anll) (exp @ mpd anrr @ mpd anrl anl)); -theorem impd (h: $ a -> b -> c -> d $): $ a -> b /\ c -> d $ = '(sylibr impexp h); -theorem expd (h: $ a -> b /\ c -> d $): $ a -> b -> c -> d $ = '(sylib impexp h); -theorem com12b: $ (a -> b -> c) <-> (b -> a -> c) $ = '(ibii (com23 id) (com23 id)); +theorem impd (h: $ aa -> bb -> c -> d $): $ aa -> bb /\ c -> d $ = '(sylibr impexp h); +theorem expd (h: $ aa -> bb /\ c -> d $): $ aa -> bb -> c -> d $ = '(sylib impexp h); +theorem com12b: $ (aa -> bb -> c) <-> (bb -> aa -> c) $ = '(ibii (com23 id) (com23 id)); -theorem orl: $ a -> a \/ b $ = 'absurdr; -theorem orr: $ b -> a \/ b $ = 'prop_1; -theorem eori (h1: $ a -> c $) (h2: $ b -> c $): $ a \/ b -> c $ = +theorem orl: $ aa -> aa \/ bb $ = 'absurdr; +theorem orr: $ bb -> aa \/ bb $ = 'prop_1; +theorem eori (h1: $ aa -> c $) (h2: $ bb -> c $): $ aa \/ bb -> c $ = '(casesd (a1i h1) (imim2i h2)); -theorem eord (h1: $ a -> b -> d $) (h2: $ a -> c -> d $): - $ a -> b \/ c -> d $ = '(com12 (eori (com12 h1) (com12 h2))); -theorem eorda (h1: $ a /\ b -> d $) (h2: $ a /\ c -> d $): - $ a -> b \/ c -> d $ = '(eord (exp h1) (exp h2)); -theorem orld (h: $ a -> b $): $ a -> b \/ c $ = '(syl orl h); -theorem orrd (h: $ a -> c $): $ a -> b \/ c $ = '(syl orr h); -theorem eor: $ (a -> c) -> (b -> c) -> a \/ b -> c $ = '(exp (eord anl anr)); -theorem orimd (h1: $ a -> b -> c $) (h2: $ a -> d -> e $): $ a -> b \/ d -> c \/ e $ = +theorem eord (h1: $ aa -> bb -> d $) (h2: $ aa -> c -> d $): + $ aa -> bb \/ c -> d $ = '(com12 (eori (com12 h1) (com12 h2))); +theorem eorda (h1: $ aa /\ bb -> d $) (h2: $ aa /\ c -> d $): + $ aa -> bb \/ c -> d $ = '(eord (exp h1) (exp h2)); +theorem orld (h: $ aa -> bb $): $ aa -> bb \/ c $ = '(syl orl h); +theorem orrd (h: $ aa -> c $): $ aa -> bb \/ c $ = '(syl orr h); +theorem eor: $ (aa -> c) -> (bb -> c) -> aa \/ bb -> c $ = '(exp (eord anl anr)); +theorem orimd (h1: $ aa -> bb -> c $) (h2: $ aa -> d -> e $): $ aa -> bb \/ d -> c \/ e $ = '(eord (syl6 orl h1) (syl6 orr h2)); -theorem orim1d (h: $ a -> b -> c $): $ a -> b \/ d -> c \/ d $ = '(orimd h idd); -theorem orim2d (h: $ a -> c -> d $): $ a -> b \/ c -> b \/ d $ = '(orimd idd h); -theorem orim1: $ (a -> b) -> a \/ c -> b \/ c $ = '(orim1d id); -theorem orim2: $ (b -> c) -> a \/ b -> a \/ c $ = '(orim2d id); -theorem oreq1d: $ (a <-> b) -> (a \/ c <-> b \/ c) $ = '(anim orim1 orim1); -theorem oreq2d: $ (a <-> b) -> (c \/ a <-> c \/ b) $ = '(anim orim2 orim2); -theorem oreq1i (h: $ a <-> b $): $ a \/ c <-> b \/ c $ = '(oreq1d h); -theorem oreq2i (h: $ b <-> c $): $ a \/ b <-> a \/ c $ = '(oreq2d h); -theorem orim: $ (a -> b) -> (c -> d) -> a \/ c -> b \/ d $ = '(exp @ syld (anwl orim1) (anwr orim2)); -theorem oreq: $ (a <-> b) -> (c <-> d) -> (a \/ c <-> b \/ d) $ = '(syl5 oreq2d @ syl bitr oreq1d); -theorem oreqi (h1: $ a <-> b $) (h2: $ c <-> d $): $ a \/ c <-> b \/ d $ = '(bitr (oreq1i h1) (oreq2i h2)); -theorem orcom: $ a \/ b -> b \/ a $ = 'con1; -theorem orcomb: $ a \/ b <-> b \/ a $ = '(ibii orcom orcom); -theorem or12: $ a \/ (b \/ c) <-> b \/ (a \/ c) $ = '(bitr3 impexp @ bitr (imeq1i ancomb) impexp); -theorem orass: $ a \/ b \/ c <-> a \/ (b \/ c) $ = '(bitr orcomb @ bitr or12 @ imeq2i orcomb); --- theorem or4: $ (a \/ b) \/ (c \/ d) <-> (a \/ c) \/ (b \/ d) $ = '(bitr4 orass @ bitr4 orass @ oreq2 or12); -theorem oridm: $ a \/ a <-> a $ = '(ibii (eor id id) orl); -theorem notan2: $ ~(a /\ b) <-> a -> ~b $ = '(bicom notnot); -theorem notan: $ ~(a /\ b) <-> (~a \/ ~b) $ = '(bitr notan2 (imeq1i notnot)); -theorem notor: $ ~(a \/ b) <-> (~a /\ ~b) $ = '(con1b (bitr4 notan (oreqi notnot notnot))); -theorem iman: $ a -> b <-> ~(a /\ ~b) $ = '(bitr4 (imeq2i notnot) notan2); -theorem imor: $ ((a \/ b) -> c) <-> ((a -> c) /\ (b -> c)) $ = +theorem orim1d (h: $ aa -> bb -> c $): $ aa -> bb \/ d -> c \/ d $ = '(orimd h idd); +theorem orim2d (h: $ aa -> c -> d $): $ aa -> bb \/ c -> bb \/ d $ = '(orimd idd h); +theorem orim1: $ (aa -> bb) -> aa \/ c -> bb \/ c $ = '(orim1d id); +theorem orim2: $ (bb -> c) -> aa \/ bb -> aa \/ c $ = '(orim2d id); +theorem oreq1d: $ (aa <-> bb) -> (aa \/ c <-> bb \/ c) $ = '(anim orim1 orim1); +theorem oreq2d: $ (aa <-> bb) -> (c \/ aa <-> c \/ bb) $ = '(anim orim2 orim2); +theorem oreq1i (h: $ aa <-> bb $): $ aa \/ c <-> bb \/ c $ = '(oreq1d h); +theorem oreq2i (h: $ bb <-> c $): $ aa \/ bb <-> aa \/ c $ = '(oreq2d h); +theorem orim: $ (aa -> bb) -> (c -> d) -> aa \/ c -> bb \/ d $ = '(exp @ syld (anwl orim1) (anwr orim2)); +theorem oreq: $ (aa <-> bb) -> (c <-> d) -> (aa \/ c <-> bb \/ d) $ = '(syl5 oreq2d @ syl bitr oreq1d); +theorem oreqi (h1: $ aa <-> bb $) (h2: $ c <-> d $): $ aa \/ c <-> bb \/ d $ = '(bitr (oreq1i h1) (oreq2i h2)); +theorem orcom: $ aa \/ bb -> bb \/ aa $ = 'con1; +theorem orcomb: $ aa \/ bb <-> bb \/ aa $ = '(ibii orcom orcom); +theorem or12: $ aa \/ (bb \/ c) <-> bb \/ (aa \/ c) $ = '(bitr3 impexp @ bitr (imeq1i ancomb) impexp); +theorem orass: $ aa \/ bb \/ c <-> aa \/ (bb \/ c) $ = '(bitr orcomb @ bitr or12 @ imeq2i orcomb); +-- theorem or4: $ (aa \/ bb) \/ (c \/ d) <-> (aa \/ c) \/ (bb \/ d) $ = '(bitr4 orass @ bitr4 orass @ oreq2 or12); +theorem oridm: $ aa \/ aa <-> aa $ = '(ibii (eor id id) orl); +theorem notan2: $ ~(aa /\ bb) <-> aa -> ~bb $ = '(bicom notnot); +theorem notan: $ ~(aa /\ bb) <-> (~aa \/ ~bb) $ = '(bitr notan2 (imeq1i notnot)); +theorem notor: $ ~(aa \/ bb) <-> (~aa /\ ~bb) $ = '(con1b (bitr4 notan (oreqi notnot notnot))); +theorem iman: $ aa -> bb <-> ~(aa /\ ~bb) $ = '(bitr4 (imeq2i notnot) notan2); +theorem imor: $ ((aa \/ bb) -> c) <-> ((aa -> c) /\ (bb -> c)) $ = '(ibii (iand (imim1i orl) (imim1i orr)) (curry eor)); -theorem andi: $ a /\ (b \/ c) <-> a /\ b \/ a /\ c $ = +theorem andi: $ aa /\ (bb \/ c) <-> aa /\ bb \/ aa /\ c $ = '(ibii (curry @ orimd ian ian) @ eor (anim2 orl) (anim2 orr)); -theorem andir: $ (a \/ b) /\ c <-> a /\ c \/ b /\ c $ = +theorem andir: $ (aa \/ bb) /\ c <-> aa /\ c \/ bb /\ c $ = '(bitr ancomb @ bitr andi @ oreqi ancomb ancomb); -theorem ordi: $ a \/ (b /\ c) <-> (a \/ b) /\ (a \/ c) $ = +theorem ordi: $ aa \/ (bb /\ c) <-> (aa \/ bb) /\ (aa \/ c) $ = '(ibii (iand (orim2 anl) (orim2 anr)) @ com12 @ animd mpcom mpcom); -theorem ordir: $ (a /\ b) \/ c <-> (a \/ c) /\ (b \/ c) $ = +theorem ordir: $ (aa /\ bb) \/ c <-> (aa \/ c) /\ (bb \/ c) $ = '(bitr orcomb @ bitr ordi @ aneq orcomb orcomb); -theorem oreq2a: $ (~a -> (b <-> c)) -> (a \/ b <-> a \/ c) $ = 'imeq2a; -theorem oreq1a: $ (~c -> (a <-> b)) -> (a \/ c <-> b \/ c) $ = '(syl5bb orcomb @ syl6bb orcomb oreq2a); -theorem biim1a: $ (~a -> b) -> (a -> b <-> b) $ = '(ibid (exp @ casesd anr anl) (a1i prop_1)); -theorem biim2a: $ (b -> ~a) -> (a -> b <-> ~a) $ = '(ibid (exp @ syl inot @ curry imim2) (a1i absurd)); -theorem bior1a: $ (a -> b) -> (a \/ b <-> b) $ = '(sylbi (imeq1i notnot) biim1a); -theorem bior2a: $ (b -> a) -> (a \/ b <-> a) $ = '(syl5bb orcomb bior1a); -theorem biim1: $ a -> (a -> b <-> b) $ = '(syl biim1a absurdr); -theorem biim2: $ ~b -> (a -> b <-> ~a) $ = '(syl biim2a absurd); -theorem bior1: $ ~a -> (a \/ b <-> b) $ = '(syl bior1a absurd); -theorem bior2: $ ~b -> (a \/ b <-> a) $ = '(syl bior2a absurd); +theorem oreq2a: $ (~aa -> (bb <-> c)) -> (aa \/ bb <-> aa \/ c) $ = 'imeq2a; +theorem oreq1a: $ (~c -> (aa <-> bb)) -> (aa \/ c <-> bb \/ c) $ = '(syl5bb orcomb @ syl6bb orcomb oreq2a); +theorem biim1a: $ (~aa -> bb) -> (aa -> bb <-> bb) $ = '(ibid (exp @ casesd anr anl) (a1i prop_1)); +theorem biim2a: $ (bb -> ~aa) -> (aa -> bb <-> ~aa) $ = '(ibid (exp @ syl inot @ curry imim2) (a1i absurd)); +theorem bior1a: $ (aa -> bb) -> (aa \/ bb <-> bb) $ = '(sylbi (imeq1i notnot) biim1a); +theorem bior2a: $ (bb -> aa) -> (aa \/ bb <-> aa) $ = '(syl5bb orcomb bior1a); +theorem biim1: $ aa -> (aa -> bb <-> bb) $ = '(syl biim1a absurdr); +theorem biim2: $ ~bb -> (aa -> bb <-> ~aa) $ = '(syl biim2a absurd); +theorem bior1: $ ~aa -> (aa \/ bb <-> bb) $ = '(syl bior1a absurd); +theorem bior2: $ ~bb -> (aa \/ bb <-> aa) $ = '(syl bior2a absurd); theorem em: $ p \/ ~p $ = 'id; theorem emr: $ ~p \/ p $ = '(orcom em); -theorem ian2: $ a -> b -> b /\ a $ = '(exp ancom); +theorem ian2: $ aa -> bb -> bb /\ aa $ = '(exp ancom); theorem absurdum: $ bot -> phi $ = '(prop_3 idd); theorem taut: $ top $ = 'absurdum; theorem imp_top: $ phi -> top $ = '(a1i taut); theorem top_or: $ top \/ phi $ = '(syl absurdum dne); -theorem bot_or: $ (bot \/ a) -> a $ = '(mpcom taut); +theorem bot_or: $ (bot \/ aa) -> aa $ = '(mpcom taut); theorem top_and: $ phi -> top /\ phi $ = '(com12 bot_or); -theorem imp_to_or (h: $(~a \/ b) -> c$): $(a -> b) -> c$ = '(rsyl con3 (rsyl orcom h)) ; +theorem imp_to_or (h: $(~aa \/ bb) -> c$): $(aa -> bb) -> c$ = '(rsyl con3 (rsyl orcom h)) ; -theorem not_distr_or: $ ~(a \/ b) <-> ~a /\ ~b $ = 'notor; -theorem and_distr: $ a /\ (b /\ c) <-> (a /\ b) /\ (a /\ c) $ = +theorem not_distr_or: $ ~(aa \/ bb) <-> ~aa /\ ~bb $ = 'notor; +theorem and_distr: $ aa /\ (bb /\ c) <-> (aa /\ bb) /\ (aa /\ c) $ = '(ibii ( rsyl (anim1 @ anr anidm) @ rsyl (anl anass) @@ -695,44 +695,44 @@ theorem and_distr: $ a /\ (b /\ c) <-> (a /\ b) /\ (a /\ c) $ = (anr anass)) (rsyl (rsyl (anl anass) anr) (anl anlass))); -theorem appl: $ (a /\ (a -> b)) -> b $ = '(con1 @ anl com12b @ con3d mpcom); +theorem appl: $ (aa /\ (aa -> bb)) -> bb $ = '(con1 @ anl com12b @ con3d mpcom); ---- analogs to anl and anr; Would prefer: $~(a -> b) <-> (a /\ ~b)$ -theorem neg_imp_left: $ ~(a -> b) -> a $ = '(con1 absurd); -theorem neg_imp_right: $~(a -> b) -> ~b $ = '(con1 (rsyl dne (a1d id))); -theorem neg_imp_wl(h: $ a -> c $): $ ~(a -> b) -> c $ = '(syl h neg_imp_left); -theorem neg_imp_wr(h: $ ~b -> c $): $ ~(a -> b) -> c $ = '(syl h neg_imp_right); +--- analogs to anl and anr; Would prefer: $~(aa -> bb) <-> (aa /\ ~bb)$ +theorem neg_imp_left: $ ~(aa -> bb) -> aa $ = '(con1 absurd); +theorem neg_imp_right: $~(aa -> bb) -> ~bb $ = '(con1 (rsyl dne (a1d id))); +theorem neg_imp_wl(h: $ aa -> c $): $ ~(aa -> bb) -> c $ = '(syl h neg_imp_left); +theorem neg_imp_wr(h: $ ~bb -> c $): $ ~(aa -> bb) -> c $ = '(syl h neg_imp_right); -theorem or_imp_xor_and: $ a \/ b -> (~(a <-> b) \/ (a /\ b)) $ = - '( eori (! cases b _ (expcom orr) +theorem or_imp_xor_and: $ aa \/ bb -> (~(aa <-> bb) \/ (aa /\ bb)) $ = + '( eori (! cases bb _ (expcom orr) @ expcom @ syl orl @ com12 @ curry @ com23 @ impd @ a2i @ a1i absurdr ) - (! cases a _ (exp orr) + (! cases aa _ (exp orr) @ expcom @ syl orl @ com12 @ curry @ com12 @ com23 @ impd @ a2i @ a1i absurdr ) ); -theorem xor_and_imp_or: $ (~(a <-> b) \/ (a /\ b)) -> a \/ b $ = +theorem xor_and_imp_or: $ (~(aa <-> bb) \/ (aa /\ bb)) -> aa \/ bb $ = '(eori (syl (imp_to_or (eori (neg_imp_wl orl) (neg_imp_wl orr))) dne) (anwl orl) ); -theorem lemma_51: $ ((a /\ ~b) \/ (b /\ ~a)) <-> ~(a <-> b) $ = '(iani +theorem lemma_51: $ ((aa /\ ~bb) \/ (bb /\ ~aa)) <-> ~(aa <-> bb) $ = '(iani (eori (con3 @ rsyl anl @ imim2i notnot1) (rsyl ancom @ con3 @ rsyl anr con3)) (con1 @ rsyl (anl not_distr_or) @ anim (anr iman) (anr iman))); -theorem lemma_in_in_reverse_helper: $ (~a \/ b) -> (~a \/ (b /\ a)) $ = +theorem lemma_in_in_reverse_helper: $ (~aa \/ bb) -> (~aa \/ (bb /\ aa)) $ = '(syl (orim2 @ anim2 dne) @ syl anr bian1a); -theorem lemma_60_helper_1: $ a -> (a /\ ~b) \/ (a /\ b) $ = +theorem lemma_60_helper_1: $ aa -> (aa /\ ~bb) \/ (aa /\ bb) $ = '(syl (anl andi) @ iand id @ a1i emr); -theorem lemma_60_helper_2: $ a -> ~b \/ (a /\ b) $ = +theorem lemma_60_helper_2: $ aa -> ~bb \/ (aa /\ bb) $ = '(syl (imim1i dne) ian); -theorem bisquare (h1: $a <-> b$) (h2: $d <-> c$) (h3: $b <-> c$): $a <-> d$ = +theorem bisquare (h1: $aa <-> bb$) (h2: $d <-> c$) (h3: $bb <-> c$): $aa <-> d$ = '(bitr h1 @ bisylr h2 h3); -theorem Fprop: $ (a -> b) -> (c -> d) -> (b -> d -> e) -> (a -> c -> e) $ = +theorem Fprop: $ (aa -> bb) -> (c -> d) -> (bb -> d -> e) -> (aa -> c -> e) $ = '(syl (anl impexp) @ com12 @ imim2d @ curry @ imim2d imim1); theorem an_top_bi_l: $ phi /\ top <-> phi $ = '(ibii anl @ syl ancom top_and); @@ -743,8 +743,8 @@ theorem an_bot_bi_r: $ bot /\ phi <-> bot $ = '(ibii anl absurdum); theorem or_bot_bi_l: $ phi \/ bot <-> phi $ = '(ibii (eori id absurdum) orl); theorem or_bot_bi_r: $ bot \/ phi <-> phi $ = '(ibii (eori absurdum id) orr); -theorem or_or_not_an: $ a \/ b <-> a \/ (~a /\ b) $ = +theorem or_or_not_an: $ aa \/ bb <-> aa \/ (~aa /\ bb) $ = '(bitr (bitr (bicom an_top_bi_r) @ aneq1i @ ibii (a1i em) imp_top) @ bicom ordi); -theorem absurd_an: $~a /\ a <-> bot$ = '(ibii (impcom mpcom) absurdum); -theorem absurd_an_r: $a /\ ~a <-> bot$ = '(ibii (curry mpcom) absurdum); +theorem absurd_an: $~aa /\ aa <-> bot$ = '(ibii (impcom mpcom) absurdum); +theorem absurd_an_r: $aa /\ ~aa <-> bot$ = '(ibii (curry mpcom) absurdum); diff --git a/02-ml-normalization.mm1 b/02-ml-normalization.mm1 index d8d3f75..37436e1 100644 --- a/02-ml-normalization.mm1 +++ b/02-ml-normalization.mm1 @@ -269,8 +269,6 @@ do { [$epsilon$ 'eSubstitution_disjoint] [$top_letter$ 'eSubstitution_disjoint] - [$a$ 'eSubstitution_disjoint] - [$b$ 'eSubstitution_disjoint] [$top_word ,Y$ 'eSubstitution_disjoint] [$concat ,psi1 ,psi2$ '(_eSubst_concat ,(propag_e_subst_adv x psi1 wo_x) ,(propag_e_subst_adv x psi2 wo_x))] [$nnimp ,phi1 ,phi2$ '(_eSubst_nnimp ,(propag_e_subst_adv x phi1 wo_x) ,(propag_e_subst_adv x phi2 wo_x))] @@ -301,8 +299,6 @@ do { [$epsilon$ 'sSubstitution_disjoint] [$top_letter$ 'sSubstitution_disjoint] - [$a$ 'sSubstitution_disjoint] - [$b$ 'sSubstitution_disjoint] [$concat ,psi1 ,psi2$ '(sSubst_concat ,(propag_s_subst_adv X psi1 wo_X) ,(propag_s_subst_adv X psi2 wo_X))] [$top_word ,Y$ (if (== X Y) 'sSubstitution_in_same_mu 'sSubstitution_disjoint)] [$kleene ,Y ,psi$ (if (== X Y) diff --git a/10-theory-definedness.mm0 b/10-theory-definedness.mm0 index 5117835..3f958d8 100644 --- a/10-theory-definedness.mm0 +++ b/10-theory-definedness.mm0 @@ -20,6 +20,11 @@ infixl _in: $in$ prec 35; axiom definedness {x: EVar}: $ |^ eVar x ^| $; +--- Functional Patterns +----------------------- + +def functional {.x: EVar} (phi: Pattern): Pattern = $ exists x (eVar x == phi) $; + --- Contextual Implications --------------------------- diff --git a/12-proof-system-p.mm1 b/12-proof-system-p.mm1 index a66b8b5..853d01d 100644 --- a/12-proof-system-p.mm1 +++ b/12-proof-system-p.mm1 @@ -100,6 +100,12 @@ theorem propag_exists_def {x: EVar} (phi: Pattern x): $ |^ exists x phi ^| -> exists x (|^ phi ^|) $ = '(norm (norm_imp defNorm @ norm_exists defNorm) (! propag_exists_disjoint box)); +theorem commute_exists {x y: EVar} (phi: Pattern x y): $ exists x (exists y phi) -> exists y (exists x phi) $ = + '(exists_generalization (eFresh_exists eFresh_exists_same_var) @ exists_framing exists_intro_same_var); + +theorem commute_exists_bi {x y: EVar} (phi: Pattern x y): $ exists x (exists y phi) <-> exists y (exists x phi) $ = + '(ibii commute_exists commute_exists); + theorem prop_43_bot (rho: Pattern): $ bot -> rho $ = 'absurdum; theorem prop_43_or {box: SVar} (ctx: Pattern box) (phi1 phi2: Pattern): $ (app[ phi1 / box ] ctx \/ app[ phi2 / box ] ctx) -> app[ phi1 \/ phi2 / box ] ctx $ = @@ -253,8 +259,8 @@ theorem subset_to_eq: $ (phi C= psi) -> (psi C= phi) -> (phi == psi) $ = '(exp @ theorem eq_refl: $ phi == phi $ = '(equiv_to_eq biid); theorem functional_same_var: $ exists x (eVar x == eVar x) $ = '(exists_intro_same_var eq_refl); -theorem functional_var: $ exists x (eVar x == eVar y) $ = - '(exists_intro @ norm (norm_sym @ _eSubst_eq eSubstitution_in_same_eVar eSubstitution_disjoint) eq_refl); +theorem functional_var: $ functional (eVar x) $ = + (named '(exists_intro @ norm (norm_sym @ _eSubst_eq eSubstitution_in_same_eVar eSubstitution_disjoint) eq_refl)); theorem eq_sym: $ (phi1 == phi2) -> (phi2 == phi1) $ = '(con3 @ framing_def @ con3 bicom); @@ -764,6 +770,10 @@ theorem eq_to_forall_bi {x: EVar} (phi1 phi2: Pattern) (psi1 psi2: Pattern x) $ (phi1 == phi2) -> ((forall x psi1) <-> (forall x psi2)) $ = '(eq_to_not_bi @ eq_to_exists_bi @ eq_to_not_bi h); +theorem eq_to_func_bi + (h: $ (phi1 == phi2) -> (psi1 <-> psi2) $): + $ (phi1 == phi2) -> ((functional psi1) <-> (functional psi2)) $ = (named '(eq_to_exists_bi @ eq_to_eq_r_bi h)); + theorem eq_to_mem_bi {x: EVar} (phi1 phi2 psi1 psi2: Pattern x) (h: $ (phi1 == phi2) -> (psi1 <-> psi2) $): $ (phi1 == phi2) -> ((x in psi1) <-> (x in psi2)) $ = @@ -968,6 +978,7 @@ do { [$_subset ,phi1 ,phi2$ '(eq_to_subset_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))] [$equiv ,phi1 ,phi2$ '(eq_to_equiv_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))] [$_eq ,phi1 ,phi2$ '(eq_to_eq_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))] + [$functional ,psi$ '(eq_to_func_bi ,(func_subst_explicit_helper x psi))] [$nnimp ,phi1 ,phi2$ '(eq_to_nnimp_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper X phi2))] [$concat ,phi1 ,phi2$ '(eq_to_concat_bi ,(func_subst_explicit_helper x phi1) ,(func_subst_explicit_helper x phi2))] @@ -1003,31 +1014,31 @@ do { exists_generalization ,fre (mp (com12 @ syl anl ,(func_subst_explicit_helper x phi1)) ,phi1_pf) ,func_phi2 )) - (def (propag_mem x ctx) @ match ctx + (def (propag_mem_w_fun x ctx fun_patterns) @ if (not (== (lookup fun_patterns ctx) #undef)) (func_subst_thm (lookup fun_patterns ctx) 'y 'membership_var_bi) @ match ctx -- special case for top and bottom? [$eVar ,y$ (if (== x y) '(taut_equiv_top membership_same_var) 'membership_var_bi)] - [$exists ,y ,psi$ (if (== x y) 'biid '(bitr membership_exists_bi @ cong_of_equiv_exists ,(propag_mem x psi)))] - [$forall ,y ,psi$ (if (== x y) 'biid '(bitr membership_forall_bi @ cong_of_equiv_forall ,(propag_mem x psi)))] + [$exists ,y ,psi$ (if (== x y) 'biid '(bitr membership_exists_bi @ cong_of_equiv_exists ,(propag_mem_w_fun x psi fun_patterns)))] + [$forall ,y ,psi$ (if (== x y) 'biid '(bitr membership_forall_bi @ cong_of_equiv_forall ,(propag_mem_w_fun x psi fun_patterns)))] [$_in ,y ,psi$ (if (== x y) 'lemma_in_in_same_var 'lemma_in_in)] - [$not ,psi$ '(bitr membership_not_bi @ cong_of_equiv_not ,(propag_mem x psi))] - [$imp ,phi1 ,phi2$ '(bitr membership_imp_bi @ cong_of_equiv_imp ,(propag_mem x phi1) ,(propag_mem x phi2))] - [$or ,phi1 ,phi2$ '(bitr membership_or_bi @ cong_of_equiv_or ,(propag_mem x phi1) ,(propag_mem x phi2))] - [$and ,phi1 ,phi2$ '(bitr membership_and_bi @ cong_of_equiv_and ,(propag_mem x phi1) ,(propag_mem x phi2))] - [$equiv ,phi1 ,phi2$ '(bitr membership_equiv_bi @ cong_of_equiv_equiv ,(propag_mem x phi1) ,(propag_mem x phi2))] - [$app ,phi1 ,phi2$ '(bitr membership_app @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem #undef phi2))] + [$not ,psi$ '(bitr membership_not_bi @ cong_of_equiv_not ,(propag_mem_w_fun x psi fun_patterns))] + [$imp ,phi1 ,phi2$ '(bitr membership_imp_bi @ cong_of_equiv_imp ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))] + [$or ,phi1 ,phi2$ '(bitr membership_or_bi @ cong_of_equiv_or ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))] + [$and ,phi1 ,phi2$ '(bitr membership_and_bi @ cong_of_equiv_and ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))] + [$equiv ,phi1 ,phi2$ '(bitr membership_equiv_bi @ cong_of_equiv_equiv ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun x phi2 fun_patterns))] + [$app ,phi1 ,phi2$ '(bitr membership_app @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem_w_fun #undef phi2 fun_patterns))] [$_ceil ,psi$ 'mem_def] [$_floor ,psi$ 'mem_floor] [$_subset ,phi1 ,phi2$ 'mem_floor] [$_eq ,phi1 ,phi2$ 'mem_floor] - -- [$nnimp ,phi1 ,phi2$ '(membership_nnimp ,(propag_mem x phi1) ,(propag_mem X phi2))] - [$a$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_a)] - [$b$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_b)] - [$epsilon$ (func_subst 'y $(x in (eVar y)) <-> (eVar x == eVar y)$ 'membership_var_bi 'functional_epsilon)] - [$concat ,phi1 ,phi2$ '(bitr membership_app2 @ cong_of_equiv_exists @ cong_of_equiv_and ,(propag_mem #undef phi1) @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem #undef phi2))] + -- [$nnimp ,phi1 ,phi2$ '(membership_nnimp ,(propag_mem_w_fun x phi1 fun_patterns) ,(propag_mem_w_fun X phi2 fun_patterns))] + [$epsilon$ (func_subst_thm 'functional_epsilon 'y 'membership_var_bi)] + [$concat ,phi1 ,phi2$ '(bitr membership_app2 @ cong_of_equiv_exists @ cong_of_equiv_and ,(propag_mem_w_fun #undef phi1 fun_patterns) @ cong_of_equiv_exists @ cong_of_equiv_and_l ,(propag_mem_w_fun #undef phi2 fun_patterns))] [_ 'biid] ) + + (def (propag_mem x ctx) @ propag_mem_w_fun x ctx (atom-map!)) }; theorem func_subst_explicit_test_1 {x y: EVar} (phi: Pattern) diff --git a/20-theory-words.mm0 b/20-theory-words.mm0 index 5f227b3..8d71d44 100644 --- a/20-theory-words.mm0 +++ b/20-theory-words.mm0 @@ -1,10 +1,5 @@ import "10-theory-definedness.mm0"; -term a_symbol : Symbol ; -def a : Pattern = $sym a_symbol$ ; -term b_symbol : Symbol ; -def b : Pattern = $sym b_symbol$ ; - def emptyset : Pattern = $bot$ ; term epsilon_symbol : Symbol ; @@ -18,9 +13,8 @@ def kleene_l {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ sVar X . def kleene_r {X: SVar} (alpha: Pattern X) : Pattern = $mu X (epsilon \/ alpha . sVar X)$; def kleene {X: SVar} (alpha: Pattern X) : Pattern = $(kleene_r X alpha)$; ---- We assume that the alphabet has only two letters. ---- This, however, captures the full expressivity. -def top_letter : Pattern = $a \/ b$; +term top_letter_symbol: Symbol; +def top_letter: Pattern = $sym top_letter_symbol$; def top_word_l {X: SVar} : Pattern = $(kleene_l X top_letter )$ ; def top_word_r {X: SVar} : Pattern = $(kleene_r X top_letter )$ ; @@ -30,12 +24,9 @@ def top_word {X: SVar} : Pattern = $(kleene X top_letter )$ ; axiom domain_words {X: SVar} : $ top_word X $; -axiom functional_epsilon {x : EVar} : $exists x (eVar x == epsilon)$; -axiom functional_a {x : EVar} : $exists x (eVar x == a)$; -axiom functional_b {x : EVar} : $exists x (eVar x == b)$; -axiom functional_concat {w v x: EVar} : $exists x (eVar x == (eVar w . eVar v))$; +axiom functional_epsilon : $ functional epsilon $; +axiom functional_concat {w v: EVar} : $ functional (eVar w . eVar v)$; -axiom no_confusion_ab_e : $a != b$; axiom no_confusion_ae_e : $~(epsilon C= top_letter)$; axiom no_confusion_ec_e {u v: EVar} : $(epsilon == eVar u . eVar v) -> (epsilon == eVar u) /\ (epsilon == eVar v)$; axiom no_confusion_cc_e {u v x y: EVar} : $(x in top_letter) -> (y in top_letter) diff --git a/21-words-helpers.mm1 b/21-words-helpers.mm1 index 414cdf2..8d54ff0 100644 --- a/21-words-helpers.mm1 +++ b/21-words-helpers.mm1 @@ -132,20 +132,11 @@ theorem cong_of_equiv_kleene {X: SVar} (phi1 phi2: Pattern X) (cong_of_equiv_or_r @ cong_of_equiv_concat_l h)); ---- Helpers for top_letter -theorem positive_in_top_letter {X: SVar}: - $ _Positive X top_letter $ = - '(positive_in_or positive_disjoint positive_disjoint); -theorem sSubst_top_letter {X: SVar} (psi: Pattern X): - $ Norm (s[ psi / X ] (top_letter)) (top_letter) $ = 'sSubstitution_disjoint; -theorem eSubst_top_letter {X: EVar} (psi: Pattern X): - $ Norm (e[ psi / X ] (top_letter)) (top_letter) $ = 'eSubstitution_disjoint; - --- Helpers for top_word_l --- TODO: Define in terms of kleene_l theorem positive_in_top_word_l_body {X: SVar}: $_Positive X (epsilon \/ sVar X . top_letter)$ = '(positive_in_or positive_disjoint @ - positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_in_top_letter); + positive_in_app (positive_in_app positive_disjoint positive_in_same_sVar) positive_disjoint); theorem kt_top_word_l {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $psi . top_letter -> psi$): $top_word_l X -> psi$ = '(KT positive_in_top_word_l_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ sVar X . top_letter$) @ eori base rec); theorem unfold_r_top_word_l {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ top_word_l X . top_letter$) : $phi -> top_word_l X$ = @@ -155,7 +146,7 @@ theorem unfold_r_top_word_l {X : SVar} (phi: Pattern X) (h: $phi -> epsilon \/ t --- TODO: Define in terms of kleene_r theorem positive_in_top_word_r_body {X: SVar}: $_Positive X (epsilon \/ top_letter . sVar X)$ = '(positive_in_or positive_disjoint @ - positive_in_app (positive_in_app positive_disjoint positive_in_top_letter) positive_in_same_sVar); + positive_in_app (positive_in_app positive_disjoint positive_disjoint) positive_in_same_sVar); theorem kt_top_word_r {X: SVar} (psi: Pattern X) (base: $epsilon -> psi$) (rec: $top_letter . psi -> psi$): $top_word_r X -> psi$ = '(KT positive_in_top_word_r_body @ norm_lemma ,(propag_s_subst 'X $epsilon \/ top_letter . sVar X$) @ eori base rec); theorem lemma_83_top_word_r_forward diff --git a/23-words-theorems.mm1 b/23-words-theorems.mm1 index 7264c54..5e49bc6 100644 --- a/23-words-theorems.mm1 +++ b/23-words-theorems.mm1 @@ -4,45 +4,32 @@ import "21-words-helpers.mm1"; --- Lift axioms to higher level constructs ------------------------------------------ -theorem def_a: $|^ a ^|$ = - (named @ func_subst_thm 'functional_a 'x 'definedness); -theorem def_b: $|^ b ^|$ = - (named @ func_subst_thm 'functional_b 'x 'definedness); - -theorem a_in_top_letter: $|^ a /\ top_letter ^|$ = - '(framing_def (iand id orl) def_a); -theorem b_in_top_letter: $|^ b /\ top_letter ^|$ = - '(framing_def (iand id orr) def_b); - ---- Lift functional axioms to $ a . [] $ and $ b . [] $. -theorem functional_l_concat {.w x y v: EVar} (l: Pattern v) - (func_l: $ exists x (eVar x == l) $): - $ exists y (eVar y == l . eVar v) $ = - (func_subst_thm 'func_l 'w 'functional_concat); -theorem functional_a_concat {.w x v: EVar} : - $ exists x (eVar x == a . eVar v) $ = - (named '(functional_l_concat functional_a)); -theorem functional_b_concat {.w x v: EVar} : - $ exists x (eVar x == b . eVar v) $ = - (named '(functional_l_concat functional_b)); - -theorem regex_eq_ewp_ab +do { + (def (in_to_mem func_phi phi_in) '(mp ,(func_subst_thm func_phi 'x 'eVar_in_subset_reverse) @ imp_to_subset ,phi_in)) +}; + +theorem functional_l_concat {v: EVar} (l: Pattern v) + (func_l: $ functional l $): + $ functional (l . eVar v) $ = + (named (func_subst_thm 'func_l 'w 'functional_concat)); + +theorem regex_eq_ewp_l (h: $ letter -> top_letter $): $ epsilon /\ letter <-> bot $ - = '(ibii + = (named '(ibii (exists_generalization_disjoint (com12 (eq_to_imp (eq_to_def @ eq_to_and_l eq_to_intro) (eq_to_not @ eq_to_and_l eq_to_intro)) - (con2 (dne @ singleton_norm (! appCtxVar box1) (! defNorm box2))) -- |^ x /\ ~a ^| <-> ~(x /\ a) - ) (exists_framing eq_sym (! functional_epsilon x)) + (con2 (dne @ singleton_norm appCtxVar defNorm)) -- |^ x /\ ~l ^| <-> ~(x /\ l) + ) (exists_framing eq_sym functional_epsilon) (framing_def (con3 @ imim2i @ syl h dne) @ dne no_confusion_ae_e)) - absurdum); + absurdum)); theorem no_confusion_cc_e_epsilon {u x y: EVar} : $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ = - '(syl (imim2i @ imim1i @ com12 eq_trans @ eq_sym identity_right_e) - ,(func_subst 'v $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e '(! functional_epsilon w)) - ); + (named '(syl (imim2i @ imim1i @ com12 eq_trans @ eq_sym identity_right_e) + ,(func_subst 'v $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e 'functional_epsilon) + )); theorem assoc_concat (Alpha Beta Gamma: Pattern): $ ((Alpha . Beta) . Gamma) <-> (Alpha . (Beta . Gamma)) $ = (named '( @@ -154,10 +141,9 @@ theorem epsilon_implies_concat (phi psi : Pattern) id); theorem epsilon_implies_not_letter (letter : Pattern) - (h: $letter -> top_letter$) - : $epsilon -> ~ letter$ -= '(exp (bi1i @ regex_eq_ewp_ab h)) - ; + (h: $letter -> top_letter$): + $ epsilon -> ~ letter $ = + '(exp (bi1i @ regex_eq_ewp_l h)); theorem epsilon_implies_not_and_l (phi psi : Pattern) (h: $epsilon -> ~ phi$) @@ -179,10 +165,6 @@ theorem regex_eq_ewp_bot: $ (epsilon /\ bot) <-> bot $ = '(ibii anr absurdum); theorem regex_eq_ewp_epsilon: $ epsilon /\ epsilon <-> epsilon $ = 'anidm; -theorem regex_eq_ewp_a: - $ epsilon /\ a <-> bot $ = '(regex_eq_ewp_ab orl); -theorem regex_eq_ewp_b: - $ epsilon /\ b <-> bot $ = '(regex_eq_ewp_ab orr); theorem regex_eq_ewp_and: $ epsilon /\ (Alpha /\ Beta) <-> (epsilon /\ Alpha) /\ (epsilon /\ Beta) $ = 'anandi; theorem regex_eq_ewp_choice: @@ -196,10 +178,6 @@ theorem regex_eq_ewp_not_bot: $ (epsilon /\ ~bot) <-> epsilon $ = '(ibii anl @ syl ancom top_and); theorem regex_eq_ewp_not_eps: $ (epsilon /\ ~epsilon) <-> bot $ = '(ibii (notnot1 notnot1) absurdum); -theorem regex_eq_ewp_not_a: $ (epsilon /\ ~a) <-> epsilon $ = - '(ibii anl @ iand id @ dne @ anl regex_eq_ewp_a); -theorem regex_eq_ewp_not_b: $ (epsilon /\ ~b) <-> epsilon $ = - '(ibii anl @ iand id @ dne @ anl regex_eq_ewp_b); theorem regex_eq_ewp_not_and: $ (epsilon /\ ~(Alpha /\ Beta)) <-> ((epsilon /\ ~ Alpha) \/ (epsilon /\ ~ Beta)) $ = '(bitr (cong_of_equiv_and_r notan) andi); theorem regex_eq_ewp_not_choice: $ (epsilon /\ ~(Alpha \/ Beta)) <-> ((epsilon /\ ~ Alpha) /\ (epsilon /\ ~ Beta)) $ = @@ -262,8 +240,8 @@ theorem regex_eq_ewp_not_concat (Alpha Beta: Pattern): rsyl (anl ,(membership_var_func_subst 'functional_epsilon 'functional_concat)) no_confusion_ec_e) @ rsyl (exists_framing @ anr anass) @ rsyl (anl and_exists_disjoint_r) - @ rsyl (anim1 @ anr ,(func_subst_eps 'x 'membership_expand)) - @ anim id id))); + @ anim1 + @ anr ,(func_subst_eps 'x 'membership_expand)))); @@ -313,10 +291,10 @@ theorem regex_eq_bot_kleene: $ (kleene X bot) <-> epsilon $ = '(ibii (epsilon_implies_kleene positive_disjoint)); theorem regex_eq_eps_kleene {X: SVar}: $ (kleene X epsilon) <-> epsilon $ = - '(ibii - (KT (positive_in_kleene_r_body positive_disjoint) @ norm (norm_sym @ norm_imp_l ,(propag_s_subst 'Y $epsilon \/ (epsilon . sVar Y)$)) @ eori id @ eq_to_intro ,(func_subst 'u $(eVar u) . epsilon == (eVar u)$ 'identity_right_e '(! functional_epsilon w))) + (named '(ibii + (KT (positive_in_kleene_r_body positive_disjoint) @ norm (norm_sym @ norm_imp_l ,(propag_s_subst 'Y $epsilon \/ (epsilon . sVar Y)$)) @ eori id @ eq_to_intro ,(func_subst 'u $(eVar u) . epsilon == (eVar u)$ 'identity_right_e 'functional_epsilon)) (imim1i orl @ norm (norm_imp_l ,(propag_s_subst 'Y $epsilon \/ (epsilon . sVar Y)$)) @ pre_fixpoint (positive_in_kleene_r_body positive_disjoint)) - ); + )); theorem regex_eq_double_kleene_l_lemma {X: SVar} (Alpha: Pattern X) (h: $ _sFresh X Alpha $): $ (kleene_l X Alpha) . (kleene_l X Alpha) -> (kleene_l X Alpha) $ = @@ -377,6 +355,15 @@ theorem l_der_phi_imp_phi (l phi: Pattern): $ (l . derivative l phi) -> phi $ = (named '(unwrap_subst appctx_concat_r id)); +theorem der_ceil (h: $ functional phi $): $ (derivative phi (|^ psi ^|)) <-> |^ psi ^| $ = + (named '(bitr der_expand + @ bitr (cong_of_equiv_exists @ cong_of_equiv_and_r + ,(func_subst 'x $ (eVar x . eVar y C= (|^ psi ^|)) <-> |^ psi ^|$ + '(bitr ,(func_subst_thm 'functional_concat 'x 'eVar_in_subset_rev) + ,(func_subst_thm 'functional_concat 'x 'mem_def)) + 'h)) + @ bicom lemma_exists_and)); + theorem der_equality_forward_lemma {x: EVar} (phi psi: Pattern x) (l: Pattern) (h: $ exists x (eVar x == l) $): $(l . psi) /\ phi -> l . derivative l phi$ = (named '(syl ,(framing_subst '(anr der_expand) 'appctx_concat_r) @ syl (anr ,(ex_appCtx_subst 'appctx_concat_r)) @ rsyl (anim1 @ syl (anl ,(ex_appCtx_subst 'appctx_concat_r)) ,(framing_subst '(anl lemma_exists_and) 'appctx_concat_r)) @ @@ -413,18 +400,6 @@ theorem der_equality_bi: $phi <-> (epsilon /\ phi) \/ exists l ((eVar l . (deriv theorem der_equality: $phi == (epsilon /\ phi) \/ exists l ((eVar l . (derivative (eVar l) phi)) /\ l in top_letter)$ = '(equiv_to_eq der_equality_bi); -theorem der_equality_bi_concrete: $phi <-> (epsilon /\ phi) \/ ((a . (derivative a phi)) \/ (b . (derivative b phi)))$ = - (named - '(bitr der_equality_bi - @ oreq2i - -- @ exists_intro_l_bi_disjoint - @ bitr (cong_of_equiv_exists @ aneq2i ,(propag_mem 'x $a \/ b$)) - @ bitr (cong_of_equiv_exists @ bitr ancomb andir) - @ bitr or_exists_bi - @ oreqi - (mp ,(func_to_and_ctx_bi 'x $eVar x . derivative (eVar x) phi$) functional_a) - (mp ,(func_to_and_ctx_bi 'x $eVar x . derivative (eVar x) phi$) functional_b))); - --- Derivatives: Syntactic Simplifications ------------------------------------------ @@ -443,10 +418,10 @@ theorem cong_of_equiv_der_r '(cong_of_equiv_der biid h); theorem der_l1_l2_phi (l1 l2 phi: Pattern) - (l1_func: $ exists x (eVar x == l1) $) - (l2_func: $ exists y (eVar y == l2) $) - (h1: $ |^ l1 /\ top_letter ^| $) - (h2: $ |^ l2 /\ top_letter ^| $): + (l1_func: $ functional l1 $) + (l2_func: $ functional l2 $) + (h1: $ l1 -> top_letter $) + (h2: $ l2 -> top_letter $): $ (derivative l1 (l2 . phi)) <-> (l1 == l2) /\ phi $ = (named '(bitr der_expand @ bitr (cong_of_equiv_exists @ cong_of_equiv_and_r @ @@ -458,7 +433,7 @@ theorem der_l1_l2_phi (l1 l2 phi: Pattern) bitr (cong_of_equiv_and_r @ bitr (ibii ( mp (mp ,(func_subst 'x $(x in top_letter) -> |^ l2 /\ top_letter ^| -> (eVar x . eVar u == l2 . eVar v) -> (eVar x == l2) /\ (eVar u == eVar v)$ (func_subst 'y $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e 'l2_func) - 'l1_func) h1) h2 + 'l1_func) ,(in_to_mem 'l1_func 'h1)) ,(in_to_mem 'l2_func 'h2) ) (rsyl (anim ,(eq_imp_eq_framing_subst 'appctx_concat_l) ,(eq_imp_eq_framing_subst 'appctx_concat_r)) @ curry eq_trans)) (cong_of_equiv_and_r @ bicom membership_var_bi)) anlass) @ bitr and_exists_disjoint @ @@ -468,6 +443,35 @@ theorem der_l1_l2_phi (l1 l2 phi: Pattern) bitr and_exists_disjoint @ cong_of_equiv_and_r lemma_62_b)); +theorem der_l1_l2_phi_and (l1 l2 phi: Pattern) + (l1_func: $ functional l1 $) + (l2_func: $ functional l2 $) + (h1: $ l1 -> top_letter $): + $ (|^ l2 /\ top_letter ^| /\ derivative l1 (l2 . phi)) <-> (l1 == l2) /\ phi $ = + (named '(bitr (cong_of_equiv_and_r der_expand) @ + bitr (bicom and_exists_disjoint) @ + bitr (cong_of_equiv_exists @ bitr anlass @ cong_of_equiv_and_r @ + bitr + (cong_of_equiv_and_r ,(func_subst 'x $(eVar x C= (l2 . phi)) <-> exists z ((z in phi) /\ (eVar x == (l2 . eVar z)))$ '(bitr (bitr eVar_in_subset_rev membership_app) @ cong_of_equiv_exists @ cong_of_equiv_and_r + ,(func_subst 'y $(x in eVar y) <-> (eVar x == eVar y)$ 'membership_var_bi '(functional_l_concat l2_func))) + '(functional_l_concat l1_func))) @ + bitr (bicom and_exists_disjoint) @ + bitr (cong_of_equiv_exists @ + bitr anlass @ + bitr (cong_of_equiv_and_r @ bitr (ibii ( + curry (mp ,(func_subst 'x $(x in top_letter) -> |^ l2 /\ top_letter ^| -> (eVar x . eVar u == l2 . eVar v) -> (eVar x == l2) /\ (eVar u == eVar v)$ + (func_subst 'y $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y . eVar v) -> (eVar x == eVar y) /\ (eVar u == eVar v)$ 'no_confusion_cc_e 'l2_func) + 'l1_func) ,(in_to_mem 'l1_func 'h1)) + ) (iand (rsyl anl (com12 (syl anl ,(func_subst_explicit_helper 'x $x in top_letter$)) ,(in_to_mem 'l1_func 'h1))) (rsyl (anim ,(eq_imp_eq_framing_subst 'appctx_concat_l) ,(eq_imp_eq_framing_subst 'appctx_concat_r)) @ curry eq_trans))) (cong_of_equiv_and_r @ bicom membership_var_bi)) + anlass) @ + bitr and_exists_disjoint @ + bicom @ cong_of_equiv_and_r ,(membership_appCtx_subst 'appCtxVar) + ) @ + bitr (cong_of_equiv_exists anlass) @ + bitr and_exists_disjoint @ + cong_of_equiv_and_r lemma_62_b + )); + do { (def (der_transformer x y l phi) '(ibii (exists_generalization_disjoint @ curry @ syl anr ,(func_subst_explicit_helper 'y $(l . eVar y) C= phi$)) @@ -478,255 +482,144 @@ theorem der_transformer_test_1 {x y: EVar} (phi: Pattern): $ (exists x ((eVar y == eVar x) /\ ((a . eVar x) C= (~ phi)))) <-> ((a . eVar y) C= (~ phi)) $ = (der_transformer 'x 'y 'a $~ phi$); +theorem regex_eq_der_exists {x: EVar} (phi: Pattern) (psi: Pattern x) + (func_phi: $ functional phi $): + $ (derivative phi (exists x psi)) <-> exists x (derivative phi psi) $ = + (named '(bisquare der_expand (cong_of_equiv_exists der_expand) + @ bitr (cong_of_equiv_exists + @ bitr (cong_of_equiv_and_r ,(func_subst 'x $ (eVar x . eVar y C= exists z psi) <-> exists z (eVar x . eVar y C= psi)$ '(bisquare ,(func_subst_thm 'functional_concat 'x 'eVar_in_subset_rev) (cong_of_equiv_exists ,(func_subst_thm 'functional_concat 'x 'eVar_in_subset_rev)) ,(func_subst_thm 'functional_concat 'x 'membership_exists_bi)) 'func_phi)) + @ bicom and_exists_disjoint + ) + commute_exists_bi)); theorem regex_eq_der_bot - (h: $ exists x (eVar x == A) $): - $ (derivative A bot) -> bot $ - = '(exists_generalization_disjoint @ con3 anr @ notnot1 @ framing_def notnot1 @ + (h: $ functional phi $): + $ (derivative phi bot) -> bot $ + = (named '(exists_generalization_disjoint @ con3 anr @ notnot1 @ framing_def notnot1 @ exists_generalization_disjoint (com12 - (eq_to_def @ norm (norm_imp_r @ norm_imp_r @ norm_sym @ norm_trans appCtxR_disjoint @ norm_app norm_refl (! appCtxVar box)) @ eq_to_app_l @ eq_to_app_r eq_to_intro) + (eq_to_def @ norm (norm_imp_r @ norm_imp_r @ norm_sym @ norm_trans appCtxR_disjoint @ norm_app norm_refl appCtxVar) @ eq_to_app_l @ eq_to_app_r eq_to_intro) (exists_generalization_disjoint (com12 (eq_to_def eq_to_intro) definedness) - (! functional_concat x v1 x1)) + functional_concat) ) h - ); -theorem regex_eq_der_bot_wrt_a: - $ (derivative a bot) <-> bot $ = '(ibii (regex_eq_der_bot (! functional_a x)) absurdum); -theorem regex_eq_der_bot_wrt_b: - $ (derivative b bot) <-> bot $ = '(ibii (regex_eq_der_bot (! functional_b x)) absurdum); - -theorem regex_eq_der_epsilon_wrt_a: - $ (derivative a epsilon) <-> bot $ = - '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ - rsyl ,(func_subst 'x $((a . eVar d) C= eVar x) -> ((a . eVar d) == eVar x)$ ( - func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ ( - func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k) - ) '(! functional_a w1) - ) '(! functional_epsilon w2)) @ - rsyl eq_sym @ - rsyl ,(func_subst 'x $(epsilon == eVar x . eVar d) -> ((epsilon == eVar x) /\ (epsilon == eVar d))$ '(! no_confusion_ec_e _ d) '(! functional_a w3)) @ - con3 anl @ con3 (rsyl eq_imp_subset subset_imp_subset_or_l) no_confusion_ae_e - ) absurdum); -theorem regex_eq_der_epsilon_wrt_b: - $ (derivative b epsilon) <-> bot $ = - '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ - rsyl ,(func_subst 'x $((b . eVar d) C= eVar x) -> ((b . eVar d) == eVar x)$ ( + )); + +theorem regex_eq_der_epsilon (phi: Pattern) + (func_phi: $ functional phi $) + (phi_in_top_letter: $ phi -> top_letter $): + $ (derivative phi epsilon) <-> bot $ = + (named '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ + rsyl ,(func_subst 'x $((phi . eVar d) C= eVar x) -> ((phi . eVar d) == eVar x)$ ( func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ ( - func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k) - ) '(! functional_b w1) - ) '(! functional_epsilon w2)) @ + func_subst_thm 'functional_concat 'x 'eVars_subset_eq_forward + ) 'func_phi + ) 'functional_epsilon) @ rsyl eq_sym @ - rsyl ,(func_subst 'x $(epsilon == eVar x . eVar d) -> ((epsilon == eVar x) /\ (epsilon == eVar d))$ '(! no_confusion_ec_e _ d) '(! functional_b w3)) @ - con3 anl @ con3 (rsyl eq_imp_subset subset_imp_subset_or_r) no_confusion_ae_e - ) absurdum); -theorem regex_eq_der_diff_a_wrt_a: - $ (derivative a b) <-> bot $ = - '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ - rsyl ,(func_subst 'x $((a . eVar d) C= eVar x) -> ((a . eVar d) == eVar x)$ ( + rsyl ,(func_subst_thm 'func_phi 'u 'no_confusion_ec_e) @ + anwl @ con3 eq_imp_subset @ con3 (com12 subset_trans @ imp_to_subset phi_in_top_letter) no_confusion_ae_e + ) absurdum)); +theorem regex_eq_der_diff_l + (func_phi: $ functional phi $) + (func_psi: $ functional psi $) + (phi_in_top_letter: $ phi -> top_letter $) + (psi_in_top_letter: $ psi -> top_letter $) + (diff: $ phi != psi $): + $ (derivative phi psi) <-> bot $ = + (named '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ + rsyl ,(func_subst 'x $((phi . eVar d) C= eVar x) -> ((phi . eVar d) == eVar x)$ ( func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ ( - func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k) - ) '(! functional_a w1) - ) '(! functional_b w2)) @ - syl no_confusion_ab_e @ syl anl @ mp + func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) 'functional_concat + ) 'func_phi + ) 'func_psi) @ + syl diff @ syl anl @ mp ,(func_subst 'y $|^ a /\ top_letter ^| -> (y in top_letter) -> (a . eVar u == eVar y) -> (a == eVar y) /\ (eVar u == epsilon)$ - (func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ '(! no_confusion_cc_e_epsilon w3) '(! functional_a w5)) - '(! functional_b w4)) a_in_top_letter b_in_top_letter - ) absurdum); -theorem regex_eq_der_diff_a_wrt_b: - $ (derivative b a) <-> bot $ = - '(ibii (rsyl (anl der_expand) @ syl not_exists_bot @ exists_framing @ con3 anr @ - rsyl ,(func_subst 'x $((b . eVar d) C= eVar x) -> ((b . eVar d) == eVar x)$ ( - func_subst 'y $((eVar y . eVar d) C= eVar x) -> ((eVar y . eVar d) == eVar x)$ ( - func_subst 'z $(eVar z C= eVar x) -> (eVar z == eVar x)$ '(eVars_subset_eq_forward) '(! functional_concat _ _ k) - ) '(! functional_b w1) - ) '(! functional_a w2)) @ - syl no_confusion_ab_e @ syl eq_sym @ syl anl @ mp - ,(func_subst 'y $|^ b /\ top_letter ^| -> (y in top_letter) -> (b . eVar u == eVar y) -> (b == eVar y) /\ (eVar u == epsilon)$ - (func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ '(! no_confusion_cc_e_epsilon w3) '(! functional_b w5)) - '(! functional_a w4)) b_in_top_letter a_in_top_letter - ) absurdum); -theorem regex_eq_der_same_a_wrt_a: - $ (derivative a a) <-> epsilon $ = + (func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar u == eVar y) -> (eVar x == eVar y) /\ (eVar u == epsilon)$ 'no_confusion_cc_e_epsilon 'func_phi) + 'func_psi) ,(in_to_mem 'func_phi 'phi_in_top_letter) ,(in_to_mem 'func_psi 'psi_in_top_letter) + ) absurdum)); +theorem regex_eq_der_same_l (phi: Pattern) + (func_phi: $ functional phi $) + (phi_in_top_letter: $ phi -> top_letter $): + $ (derivative phi phi) <-> epsilon $ = (named '(ibii (rsyl (anl der_expand) @ exists_generalization_disjoint @ syl simple_eq_subst @ anim2 @ syl (syl anr @ mp ,(func_subst 'y $(y in top_letter) -> (a . eVar d == eVar y) -> (a == eVar y) /\ (eVar d == epsilon)$ '(mp - ,(func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar d == eVar y) -> (eVar x == eVar y) /\ (eVar d == epsilon)$ 'no_confusion_cc_e_epsilon 'functional_a) - a_in_top_letter) - 'functional_a) - a_in_top_letter) - ,(func_subst 'y $((a . eVar d) C= eVar y) -> ((a . eVar d) == eVar y)$ (func_subst 'v $((eVar v . eVar d) C= eVar y) -> ((eVar v . eVar d) == eVar y)$ (func_subst 'x $(eVar x C= eVar y) -> (eVar x == eVar y)$ 'eVars_subset_eq_forward 'functional_concat) 'functional_a) 'functional_a) + ,(func_subst_thm 'func_phi 'x 'no_confusion_cc_e_epsilon) + ,(in_to_mem 'func_phi 'phi_in_top_letter)) + 'func_phi) + ,(in_to_mem 'func_phi 'phi_in_top_letter)) + ,(func_subst 'y $((a . eVar d) C= eVar y) -> ((a . eVar d) == eVar y)$ (func_subst 'v $((eVar v . eVar d) C= eVar y) -> ((eVar v . eVar d) == eVar y)$ (func_subst 'x $(eVar x C= eVar y) -> (eVar x == eVar y)$ 'eVars_subset_eq_forward 'functional_concat) 'func_phi) 'func_phi) ) (syl (anr der_expand) @ syl ,(func_subst_fresh '(eFresh_imp eFresh_disjoint eFresh_exists_same_var) 'd $(eVar d /\ ((a . eVar d) C= a)) -> exists d (eVar d /\ ((a . eVar d) C= a))$ 'exists_intro_same_var 'functional_epsilon) @ iand id @ a1i @ imp_to_subset @ anl id_concat_r ) )); -theorem regex_eq_der_same_a_wrt_b: - $ (derivative b b) <-> epsilon $ = - (named '(ibii - (rsyl (anl der_expand) @ exists_generalization_disjoint @ syl simple_eq_subst @ anim2 @ syl - (syl anr @ mp - ,(func_subst 'y $(y in top_letter) -> (b . eVar d == eVar y) -> (b == eVar y) /\ (eVar d == epsilon)$ - '(mp - ,(func_subst 'x $(x in top_letter) -> (y in top_letter) -> (eVar x . eVar d == eVar y) -> (eVar x == eVar y) /\ (eVar d == epsilon)$ 'no_confusion_cc_e_epsilon 'functional_b) - b_in_top_letter) - 'functional_b) - b_in_top_letter) - ,(func_subst 'y $((b . eVar d) C= eVar y) -> ((b . eVar d) == eVar y)$ (func_subst 'v $((eVar v . eVar d) C= eVar y) -> ((eVar v . eVar d) == eVar y)$ (func_subst 'x $(eVar x C= eVar y) -> (eVar x == eVar y)$ 'eVars_subset_eq_forward 'functional_concat) 'functional_b) 'functional_b) - ) - (syl (anr der_expand) @ - syl ,(func_subst_fresh '(eFresh_imp eFresh_disjoint eFresh_exists_same_var) 'd $(eVar d /\ ((b . eVar d) C= b)) -> exists d (eVar d /\ ((b . eVar d) C= b))$ 'exists_intro_same_var 'functional_epsilon) @ - iand id @ a1i @ imp_to_subset @ anl id_concat_r - ) - )); -theorem regex_eq_der_choice_wrt_a: $ (derivative a (Alpha \/ Beta)) <-> (derivative a Alpha) \/ (derivative a Beta) $ = - '(bitr (! der_expand d1) @ +theorem regex_eq_der_choice (phi: Pattern) + (func_phi: $ functional phi $): + $ (derivative phi (Alpha \/ Beta)) <-> (derivative phi Alpha) \/ (derivative phi Beta) $ = + (named '(bitr (! der_expand d1) @ bitr ( membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= (Alpha \/ Beta)))) <-> ((exists x (eVar x /\ ((a . eVar x) C= Alpha))) \/ (exists x (eVar x /\ ((a . eVar x) C= Beta))))$) @ - bitr ,(der_transformer 'x 'y 'a $Alpha \/ Beta$) @ + ,(propag_mem_w_fun 'y $(exists x (eVar x /\ ((phi . eVar x) C= (Alpha \/ Beta)))) <-> ((exists x (eVar x /\ ((phi . eVar x) C= Alpha))) \/ (exists x (eVar x /\ ((phi . eVar x) C= Beta))))$ (atom-map! '[phi func_phi])) @ + bitr ,(der_transformer 'x 'y 'phi $Alpha \/ Beta$) @ bitr ,(func_subst 'x $(eVar x C= Alpha \/ Beta) <-> (eVar x C= Alpha) \/ (eVar x C= Beta)$ '( bitr eVar_in_subset_rev @ bitr membership_or_bi (cong_of_equiv_or eVar_in_subset eVar_in_subset) - ) '(! functional_a_concat d2 x)) @ + ) '(functional_l_concat func_phi)) @ bicom @ cong_of_equiv_or ,(der_transformer 'x 'y 'a $Alpha$) ,(der_transformer 'x 'y 'a $Beta$)) @ - bicom @ cong_of_equiv_or (! der_expand d1) (! der_expand d1)); -theorem regex_eq_der_choice_wrt_b: $ (derivative b (Alpha \/ Beta)) <-> (derivative b Alpha) \/ (derivative b Beta) $ = - '(bitr (! der_expand d1) @ + bicom @ cong_of_equiv_or (! der_expand d1) (! der_expand d1))); +theorem regex_eq_der_conj (phi: Pattern) + (func_phi: $ functional phi $): + $ (derivative phi (Alpha /\ Beta)) <-> (derivative phi Alpha) /\ (derivative phi Beta) $ = + (named '(bitr (! der_expand d1) @ bitr ( membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= (Alpha \/ Beta)))) <-> ((exists x (eVar x /\ ((b . eVar x) C= Alpha))) \/ (exists x (eVar x /\ ((b . eVar x) C= Beta))))$) @ - bitr ,(der_transformer 'x 'y 'b $Alpha \/ Beta$) @ - bitr ,(func_subst 'x $(eVar x C= Alpha \/ Beta) <-> (eVar x C= Alpha) \/ (eVar x C= Beta)$ '( - bitr eVar_in_subset_rev @ bitr membership_or_bi (cong_of_equiv_or eVar_in_subset eVar_in_subset) - ) '(! functional_b_concat d2 x)) @ - bicom @ cong_of_equiv_or ,(der_transformer 'x 'y 'b $Alpha$) ,(der_transformer 'x 'y 'b $Beta$)) @ - bicom @ cong_of_equiv_or (! der_expand d1) (! der_expand d1)); -theorem regex_eq_der_conj_wrt_a: $ (derivative a (Alpha /\ Beta)) <-> (derivative a Alpha) /\ (derivative a Beta) $ = - '(bitr (! der_expand d1) @ - bitr ( - membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= (Alpha /\ Beta)))) <-> ((exists x (eVar x /\ ((a . eVar x) C= Alpha))) /\ (exists x (eVar x /\ ((a . eVar x) C= Beta))))$) @ - bitr ,(der_transformer 'x 'y 'a $Alpha /\ Beta$) @ + ,(propag_mem_w_fun 'y $(exists x (eVar x /\ ((phi . eVar x) C= (Alpha /\ Beta)))) <-> ((exists x (eVar x /\ ((phi . eVar x) C= Alpha))) /\ (exists x (eVar x /\ ((phi . eVar x) C= Beta))))$ (atom-map! '[phi func_phi])) @ + bitr ,(der_transformer 'x 'y 'phi $Alpha /\ Beta$) @ bitr ,(func_subst 'x $(eVar x C= Alpha /\ Beta) <-> (eVar x C= Alpha) /\ (eVar x C= Beta)$ '( bitr eVar_in_subset_rev @ bitr membership_and_bi (cong_of_equiv_and eVar_in_subset eVar_in_subset) - ) '(! functional_a_concat d2 x)) @ + ) '(functional_l_concat func_phi)) @ bicom @ cong_of_equiv_and ,(der_transformer 'x 'y 'a $Alpha$) ,(der_transformer 'x 'y 'a $Beta$)) @ - bicom @ cong_of_equiv_and (! der_expand d1) (! der_expand d1)); -theorem regex_eq_der_conj_wrt_b: $ (derivative b (Alpha /\ Beta)) <-> (derivative b Alpha) /\ (derivative b Beta) $ = - '(bitr (! der_expand d1) @ + bicom @ cong_of_equiv_and (! der_expand d1) (! der_expand d1))); +theorem regex_eq_der_neg (phi: Pattern) + (func_phi: $ functional phi $): + $ (derivative phi (~ Alpha)) <-> ~ (derivative phi Alpha) $ = + (named '(bitr (! der_expand d1) @ bitr ( membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= (Alpha /\ Beta)))) <-> ((exists x (eVar x /\ ((b . eVar x) C= Alpha))) /\ (exists x (eVar x /\ ((b . eVar x) C= Beta))))$) @ - bitr ,(der_transformer 'x 'y 'b $Alpha /\ Beta$) @ - bitr ,(func_subst 'x $(eVar x C= Alpha /\ Beta) <-> (eVar x C= Alpha) /\ (eVar x C= Beta)$ '( - bitr eVar_in_subset_rev @ bitr membership_and_bi (cong_of_equiv_and eVar_in_subset eVar_in_subset) - ) '(! functional_b_concat d2 x)) @ - bicom @ cong_of_equiv_and ,(der_transformer 'x 'y 'b $Alpha$) ,(der_transformer 'x 'y 'b $Beta$)) @ - bicom @ cong_of_equiv_and (! der_expand d1) (! der_expand d1)); -theorem regex_eq_der_neg_wrt_a: $ (derivative a (~ Alpha)) <-> ~ (derivative a Alpha) $ = - '(bitr (! der_expand d1) @ - bitr ( - membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((a . eVar x) C= ~ Alpha))) <-> ~ (exists x (eVar x /\ ((a . eVar x) C= Alpha)))$) @ + ,(propag_mem_w_fun 'y $(exists x (eVar x /\ ((phi . eVar x) C= ~ Alpha))) <-> ~ (exists x (eVar x /\ ((phi . eVar x) C= Alpha)))$ (atom-map! '[phi func_phi])) @ bitr ,(der_transformer 'x 'y 'a $~ Alpha$) @ - bitr (cong_of_equiv_not ,(func_subst 'x $(x in Alpha) <-> (eVar x C= Alpha)$ 'eVar_in_subset '(! functional_a_concat d2 x))) @ - bicom @ cong_of_equiv_not ,(der_transformer 'x 'y 'b $Alpha$)) @ - bicom @ cong_of_equiv_not (! der_expand d1)); -theorem regex_eq_der_neg_wrt_b: $ (derivative b (~ Alpha)) <-> ~ (derivative b Alpha) $ = - '(bitr (! der_expand d1) @ - bitr ( - membership_elim_implicit @ anr - ,(propag_mem 'y $(exists x (eVar x /\ ((b . eVar x) C= ~ Alpha))) <-> ~ (exists x (eVar x /\ ((b . eVar x) C= Alpha)))$) @ - bitr ,(der_transformer 'x 'y 'b $~ Alpha$) @ - bitr (cong_of_equiv_not ,(func_subst 'x $(x in Alpha) <-> (eVar x C= Alpha)$ 'eVar_in_subset '(! functional_b_concat d2 x))) @ + bitr (cong_of_equiv_not ,(func_subst 'x $(x in Alpha) <-> (eVar x C= Alpha)$ 'eVar_in_subset '(functional_l_concat func_phi))) @ bicom @ cong_of_equiv_not ,(der_transformer 'x 'y 'b $Alpha$)) @ - bicom @ cong_of_equiv_not (! der_expand d1)); -theorem regex_eq_der_concat_wrt_a (Alpha Beta: Pattern) : - $ (derivative a (Alpha . Beta)) <-> ((derivative a Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative a Beta)) $ = - (named '(ibii - (rsyl (anl @ - bitr (cong_of_equiv_der_r @ cong_of_equiv_concat_l der_equality_bi_concrete) @ - bitr (cong_of_equiv_der_r ,(or_appCtx2_r_subst 'appctx_concat_l)) @ - bitr regex_eq_der_choice_wrt_a @ - bitr (cong_of_equiv_or_r regex_eq_der_choice_wrt_a) @ - bitr (cong_of_equiv_or - ( bitr (cong_of_equiv_der_r epsilon_and_concat) - der_expand) - @ cong_of_equiv_or - ( bitr (cong_of_equiv_der_r assoc_concat) @ - bitr (der_l1_l2_phi functional_a functional_a a_in_top_letter a_in_top_letter) @ - taut_and_equiv eq_refl) - ( bitr (cong_of_equiv_der_r assoc_concat) @ - bitr (der_l1_l2_phi functional_a functional_b a_in_top_letter b_in_top_letter) @ - absurd_and_equiv_bot no_confusion_ab_e) - ) @ - bitr (cong_of_equiv_or_r or_bot_bi_l) @ - orcomb) @ - orim2 @ syl (anr epsilon_and_concat) @ syl (anim2 @ anr der_expand) @ rsyl - (exists_framing @ syl (anr anlass) @ anim2 @ rsyl subset_and @ anim1 - ,(func_subst 'x $(eVar x C= |^ phi ^|) -> |^ phi ^|$ '(rsyl eVar_in_subset_reverse mem_def_forward) 'functional_a_concat)) - and_exists_disjoint_forwards - ) - (rsyl (anl @ cong_of_equiv_or (cong_of_equiv_concat_l der_expand) (cong_of_equiv_concat_r der_expand)) @ syl (anr der_expand) @ eori - (rsyl (norm (norm_imp appCtxLRVar @ norm_exists appCtxLRVar) propag_exists_disjoint) @ exists_generalization_disjoint @ - rsyl (anl ,(appCtx_pointwise_subst 'appCtxRVar)) @ exists_generalization_disjoint @ rsyl (anim1 - ,(func_subst 'x $((eVar d /\ (eVar x C= Alpha)) . eVar beta) -> (eVar d . eVar beta /\ (eVar x C= Alpha))$ '(anl ,(lemma_60_subset_subst 'appCtxLRVar)) 'functional_a_concat)) @ - rsyl (anl anass) @ rsyl (anim2 @ syl (framing_subset (anr assoc_concat) id) @ rsyl (anim - ,(subset_imp_subset_framing_subst 'appCtxLRVar) - (rsyl eVar_in_subset_forward ,(subset_imp_subset_framing_subst 'appCtxRVar))) @ - curry subset_trans) @ anr imp_exists_disjoint @ exists_framing ( - syl anr ,(func_subst_explicit_helper 'x $eVar x /\ ((a . eVar x) C= Alpha . Beta)$) - ) functional_concat) - (rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @ exists_framing @ iand - (rsyl ,(framing_subst 'anl 'appCtxLRVar) @ syl anl @ anl id_concat_l) - (rsyl (iand (norm (norm_imp_l appCtxLRVar) lemma_56) (syl anr @ syl (anl id_concat_l) ,(framing_subst 'anl 'appCtxLRVar))) @ - rsyl (anim1 ,(func_subst 'x $(x in Alpha) -> (eVar x C= Alpha)$ 'eVar_in_subset_forward 'functional_epsilon)) @ - rsyl (curry concat_subset) @ framing_subset (anr id_concat_l) id)) - ))); -theorem regex_eq_der_concat_wrt_b (Alpha Beta: Pattern) : - $ (derivative b (Alpha . Beta)) <-> ((derivative b Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative b Beta)) $ = - (named '(ibii - (rsyl (anl @ - bitr (cong_of_equiv_der_r @ cong_of_equiv_concat_l der_equality_bi_concrete) @ - bitr (cong_of_equiv_der_r ,(or_appCtx2_r_subst 'appctx_concat_l)) @ - bitr regex_eq_der_choice_wrt_b @ - bitr (cong_of_equiv_or_r regex_eq_der_choice_wrt_b) @ - bitr (cong_of_equiv_or - ( bitr (cong_of_equiv_der_r epsilon_and_concat) - der_expand) - @ cong_of_equiv_or - ( bitr (cong_of_equiv_der_r assoc_concat) @ - bitr (der_l1_l2_phi functional_b functional_a b_in_top_letter a_in_top_letter) @ - absurd_and_equiv_bot @ rsyl eq_sym no_confusion_ab_e) - ( bitr (cong_of_equiv_der_r assoc_concat) @ - bitr (der_l1_l2_phi functional_b functional_b b_in_top_letter b_in_top_letter) @ - taut_and_equiv eq_refl) - ) @ - bitr (cong_of_equiv_or_r or_bot_bi_r) @ - orcomb) @ - orim2 @ syl (anr epsilon_and_concat) @ syl (anim2 @ anr der_expand) @ rsyl - (exists_framing @ syl (anr anlass) @ anim2 @ rsyl subset_and @ anim1 - ,(func_subst 'x $(eVar x C= |^ phi ^|) -> |^ phi ^|$ '(rsyl eVar_in_subset_reverse mem_def_forward) 'functional_b_concat)) - and_exists_disjoint_forwards - ) - (rsyl (anl @ cong_of_equiv_or (cong_of_equiv_concat_l der_expand) (cong_of_equiv_concat_r der_expand)) @ syl (anr der_expand) @ eori - (rsyl (norm (norm_imp appCtxLRVar @ norm_exists appCtxLRVar) propag_exists_disjoint) @ exists_generalization_disjoint @ - rsyl (anl ,(appCtx_pointwise_subst 'appCtxRVar)) @ exists_generalization_disjoint @ rsyl (anim1 - ,(func_subst 'x $((eVar d /\ (eVar x C= Alpha)) . eVar beta) -> (eVar d . eVar beta /\ (eVar x C= Alpha))$ '(anl ,(lemma_60_subset_subst 'appCtxLRVar)) 'functional_b_concat)) @ - rsyl (anl anass) @ rsyl (anim2 @ syl (framing_subset (anr assoc_concat) id) @ rsyl (anim - ,(subset_imp_subset_framing_subst 'appCtxLRVar) - (rsyl eVar_in_subset_forward ,(subset_imp_subset_framing_subst 'appCtxRVar))) @ - curry subset_trans) @ anr imp_exists_disjoint @ exists_framing ( - syl anr ,(func_subst_explicit_helper 'x $eVar x /\ ((b . eVar x) C= Alpha . Beta)$) - ) functional_concat) - (rsyl (anl ,(ex_appCtx_subst 'appCtxRVar)) @ exists_framing @ iand - (rsyl ,(framing_subst 'anl 'appCtxLRVar) @ syl anl @ anl id_concat_l) - (rsyl (iand (norm (norm_imp_l appCtxLRVar) lemma_56) (syl anr @ syl (anl id_concat_l) ,(framing_subst 'anl 'appCtxLRVar))) @ - rsyl (anim1 ,(func_subst 'x $(x in Alpha) -> (eVar x C= Alpha)$ 'eVar_in_subset_forward 'functional_epsilon)) @ - rsyl (curry concat_subset) @ framing_subset (anr id_concat_l) id)) - ))); + bicom @ cong_of_equiv_not (! der_expand d1))); +theorem regex_eq_der_concat (phi: Pattern) + (func_phi: $ functional phi $) + (phi_in_top_letter: $ phi -> top_letter $): + $ (derivative phi (Alpha . Beta)) <-> ((derivative phi Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative phi Beta)) $ = + (named '( + bitr (cong_of_equiv_der_r @ cong_of_equiv_concat_l der_equality_bi) @ + bitr (cong_of_equiv_der_r ,(or_appCtx_subst 'appctx_concat_l)) @ + bitr (regex_eq_der_choice func_phi) @ + bitr orcomb @ + cong_of_equiv_or + ( bitr (cong_of_equiv_der_r ,(ex_appCtx_subst 'appctx_concat_l)) + @ bitr (regex_eq_der_exists func_phi) + @ bitr (cong_of_equiv_exists @ cong_of_equiv_der_r ,(lemma_60_subst 'appctx_concat_l)) + @ bitr (cong_of_equiv_exists @ cong_of_equiv_der_r @ cong_of_equiv_and_l assoc_concat) + @ bitr (cong_of_equiv_exists + ( bitr (regex_eq_der_conj func_phi) + @ bitr (cong_of_equiv_and_r @ der_ceil func_phi) + @ bitr ancomb + @ bitr (der_l1_l2_phi_and func_phi functional_var phi_in_top_letter) + @ cong_of_equiv_and_l @ ibii eq_sym eq_sym)) + @ mp ,(func_to_and_ctx_bi 'x $(derivative (eVar x) Alpha) . Beta$) func_phi + ) + ( bitr (cong_of_equiv_der_r epsilon_and_concat) + @ bitr (regex_eq_der_conj func_phi) + @ bitr (cong_of_equiv_and_l @ der_ceil func_phi) + @ bicom epsilon_and_concat) + )); theorem regex_eq_der_kleene_lemma {X: SVar} (Alpha: Pattern X) @@ -770,31 +663,19 @@ theorem regex_eq_der_kleene_lemma {X: SVar} (Alpha: Pattern X) @ rsyl and_exists_disjoint_forwards anl)) @ framing_concat_l anr)); -theorem regex_eq_der_kleene_wrt_a {X: SVar} (Alpha: Pattern X) - (X_fresh: $ _sFresh X Alpha $): - $ (derivative a (kleene X Alpha)) <-> ((derivative a Alpha) . (kleene X Alpha)) $ = - (named '(bitr (cong_of_equiv_der_r @ bitr (unfold_kleene X_fresh) or_or_not_an) @ - bitr regex_eq_der_choice_wrt_a @ - bitr (cong_of_equiv_or_l regex_eq_der_epsilon_wrt_a) @ - bitr or_bot_bi_r @ - bitr (cong_of_equiv_der_r @ regex_eq_der_kleene_lemma X_fresh) @ - bitr regex_eq_der_concat_wrt_a @ - bitr (cong_of_equiv_or - (cong_of_equiv_concat_l (bitr regex_eq_der_conj_wrt_a @ bitr (cong_of_equiv_and_l @ bitr regex_eq_der_neg_wrt_a @ cong_of_equiv_not regex_eq_der_epsilon_wrt_a) an_top_bi_r)) - (bitr (cong_of_equiv_concat_l @ bitr (bicom anass) @ bitr (cong_of_equiv_and_l absurd_an_r) an_bot_bi_r) (ibii (norm (norm_imp_l appctx_concat_l) propag_bot) absurdum))) @ - or_bot_bi_l)); - -theorem regex_eq_der_kleene_wrt_b {X: SVar} (Alpha: Pattern X) - (X_fresh: $ _sFresh X Alpha $): - $ (derivative b (kleene X Alpha)) <-> ((derivative b Alpha) . (kleene X Alpha)) $ = +theorem regex_eq_der_kleene {X: SVar} (Alpha: Pattern X) (phi: Pattern) + (X_fresh: $ _sFresh X Alpha $) + (func_phi: $ functional phi $) + (phi_in_top_letter: $ phi -> top_letter $): + $ (derivative phi (kleene X Alpha)) <-> ((derivative phi Alpha) . (kleene X Alpha)) $ = (named '(bitr (cong_of_equiv_der_r @ bitr (unfold_kleene X_fresh) or_or_not_an) @ - bitr regex_eq_der_choice_wrt_b @ - bitr (cong_of_equiv_or_l regex_eq_der_epsilon_wrt_b) @ + bitr (regex_eq_der_choice func_phi) @ + bitr (cong_of_equiv_or_l @ regex_eq_der_epsilon func_phi phi_in_top_letter) @ bitr or_bot_bi_r @ bitr (cong_of_equiv_der_r @ regex_eq_der_kleene_lemma X_fresh) @ - bitr regex_eq_der_concat_wrt_b @ + bitr (regex_eq_der_concat func_phi phi_in_top_letter) @ bitr (cong_of_equiv_or - (cong_of_equiv_concat_l (bitr regex_eq_der_conj_wrt_b @ bitr (cong_of_equiv_and_l @ bitr regex_eq_der_neg_wrt_b @ cong_of_equiv_not regex_eq_der_epsilon_wrt_b) an_top_bi_r)) + (cong_of_equiv_concat_l (bitr (regex_eq_der_conj func_phi) @ bitr (cong_of_equiv_and_l @ bitr (regex_eq_der_neg func_phi) @ cong_of_equiv_not (regex_eq_der_epsilon func_phi phi_in_top_letter)) an_top_bi_r)) (bitr (cong_of_equiv_concat_l @ bitr (bicom anass) @ bitr (cong_of_equiv_and_l absurd_an_r) an_bot_bi_r) (ibii (norm (norm_imp_l appctx_concat_l) propag_bot) absurdum))) @ or_bot_bi_l)); @@ -856,59 +737,6 @@ theorem top_implies_fp_leaf {box: SVar} (phi : Pattern box) : $( ctximp_app box (sVar box . top_letter) phi) . top_letter -> phi $ = '(norm (norm_imp appctx_concat_l norm_refl) ctximp_in_ctx_forward); ---- fp-implies-alpha --------------------- - -theorem positive_in_fp_interior (phi_a phi_b: Pattern X) - (p_a: $ _Positive X phi_a $) - (p_b: $ _Positive X phi_b $): - $ _Positive X (epsilon \/ (a . phi_a \/ b . phi_b )) $ - = '(positive_in_or positive_disjoint (positive_in_or (positive_in_concat positive_disjoint p_a) - (positive_in_concat positive_disjoint p_b))); - --- TODO(MirceaS): Can't this be relaxed to allow eBox to show up in some or all of the patterns? -theorem top_implies_fp_interior {X: SVar} {box: SVar} (fp_unf_a fp_unf_b fp_ctximp_a fp_ctximp_b: Pattern X box) - (p_fp_unf_a: $ _Positive X fp_unf_a $) - (p_fp_unf_b: $ _Positive X fp_unf_b $) - (p_fp_ctximp_a: $ _Positive X fp_ctximp_a $) - (p_fp_ctximp_b: $ _Positive X fp_ctximp_b $) - - (he_a: $epsilon -> s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_a$) - (he_b: $epsilon -> s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_b$) - (ha: $((s[ (ctximp_app box (sVar box . top_letter) (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))) / X ] fp_ctximp_a) . top_letter) - -> (s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_a)$) - (hb: $((s[ (ctximp_app box (sVar box . top_letter) (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))) / X ] fp_ctximp_b) . top_letter) - -> (s[ (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b)))) / X ] fp_unf_b)$) - : ------------------------ - $(mu X (epsilon \/ ((a . fp_ctximp_a) \/ (b . fp_ctximp_b)))) . top_letter -> (mu X (epsilon \/ ((a . fp_unf_a) \/ (b . fp_unf_b))))$ - = (id - '(unwrap_subst appctx_concat_l - @ KT_subst (positive_in_fp_interior p_fp_ctximp_a p_fp_ctximp_b) ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$) - @ eori - ( wrap_subst appctx_concat_l - @ rsyl (anl regex_eq_eps_concat_l) - @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b) - @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$)) - @ orrd - @ orim - (rsyl (anr regex_eq_eps_concat_r) @ framing_concat_r he_a) - (rsyl (anr regex_eq_eps_concat_r) @ framing_concat_r he_b)) - @ eori - ( wrap_subst appctx_concat_l - @ rsyl (bi1i @ assoc_concat) - @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b) - @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$)) - @ orrd @ orld - @ framing_concat_r ha) - ( wrap_subst appctx_concat_l - @ rsyl (bi1i @ assoc_concat) - @ unfold_r (positive_in_fp_interior p_fp_unf_a p_fp_unf_b) - @ norm (norm_sym @ norm_imp_r ,(propag_s_subst 'X $epsilon \/ (a . _ \/ b . _)$)) - @ orrd @ orrd - @ framing_concat_r hb) - )); - - --- Apply equivalence left to right theorem apply_equiv (eq: $phi <-> psi$) (cont: $rho -> psi$): $rho -> phi$ @@ -916,18 +744,3 @@ theorem apply_equiv (eq: $phi <-> psi$) (cont: $rho -> psi$): $rho -> phi$ theorem fp_implies_regex_leaf : $rho -> rho$ = 'id; - -theorem fp_implies_regex_interior {X: SVar} (phi_a phi_b: Pattern X) - (posa: $ _Positive X phi_a $) - (posb: $ _Positive X phi_b $) - (he: $epsilon -> rho$) - (ha: $s[ rho / X ] phi_a -> (derivative a rho)$) - (hb: $s[ rho / X ] phi_b -> (derivative b rho)$): - ---------------------------------------------- - $(mu X (epsilon \/ ((a . phi_a) \/ (b . phi_b)))) -> rho$ = - '(KT - (positive_in_or positive_disjoint @ positive_in_or (positive_in_concat positive_disjoint posa) (positive_in_concat positive_disjoint posb)) @ - apply_equiv der_equality_bi_concrete (norm - (norm_imp_l @ norm_sym @ _sSubst_or sSubstitution_disjoint @ _sSubst_or (sSubst_concat_r norm_refl) (sSubst_concat_r norm_refl)) - (orim (iand id he) @ orim (framing_concat_r ha) (framing_concat_r hb)) - )); diff --git a/proof-gen.py b/proof-gen.py index 5d5bf0d..8cca629 100755 --- a/proof-gen.py +++ b/proof-gen.py @@ -21,12 +21,12 @@ def cleanup_maude_output(s: str) -> str: (mm01, theorem, regex) = sys.argv[1:] if mm01 == 'mm0': - print('import "../20-theory-words.mm0";') + print('import "../24-ab-alphabet.mm0";') print(cleanup_maude_output( reduce_in_module('regexp-proof-gen.maude', 'PROOF-GEN', 'MM0Decl', 'theorem-{0}-mm0({1})'.format(theorem, regex)))) elif mm01 == 'mm1': - print('import "../23-words-theorems.mm1";') + print('import "../24-ab-alphabet.mm1";') print(cleanup_maude_output( reduce_in_module('regexp-proof-gen.maude', 'PROOF-GEN', 'MM0Decl', 'theorem-{0}({1})'.format(theorem, regex)))) diff --git a/regexp-proof-gen.maude b/regexp-proof-gen.maude index 80a8055..97bfb0a 100644 --- a/regexp-proof-gen.maude +++ b/regexp-proof-gen.maude @@ -261,10 +261,11 @@ mod ERE-THEOREMS is vars A B A1 A2 : Letter . vars X Y : Qid . - rl [regex_eq_der_bot] : (derivative A bot) => bot . - rl [regex_eq_der_epsilon] : (derivative A epsilon) => bot . - rl [regex_eq_der_same_a] : (derivative A A) => epsilon . - crl [regex_eq_der_diff_a] : (derivative A B) => bot if A =/= B . + rl [regex_eq_der_bot] : (derivative A bot) => bot . + rl [regex_eq_der_epsilon] : (derivative A epsilon) => bot . + rl [regex_eq_der_same_l] : (derivative A A) => epsilon . + crl [regex_eq_der_diff_l_a] : (derivative A a) => bot if A =/= a . + crl [regex_eq_der_diff_l_b] : (derivative A b) => bot if A =/= b . rl [regex_eq_der_kleene] : (derivative A [[kleene X Alpha]]) => (derivative A Alpha) . [[kleene X Alpha]] . @@ -418,8 +419,9 @@ mod PROOF-GEN is eq applyAnyEquation(S, SL, NAT) = applyEq(S, SL, NAT, 'regex_eq_der_bot) or-else applyEq(S, SL, NAT, 'regex_eq_der_epsilon) or-else - applyEq(S, SL, NAT, 'regex_eq_der_same_a) or-else - applyEq(S, SL, NAT, 'regex_eq_der_diff_a) or-else + applyEq(S, SL, NAT, 'regex_eq_der_same_l) or-else + applyEq(S, SL, NAT, 'regex_eq_der_diff_l_a) or-else + applyEq(S, SL, NAT, 'regex_eq_der_diff_l_b) or-else applyEq(S, SL, NAT, 'regex_eq_der_kleene) or-else applyEq(S, SL, NAT, 'regex_eq_der_concat) or-else applyEq(S, SL, NAT, 'regex_eq_der_choice) or-else @@ -681,8 +683,8 @@ mod PROOF-GEN is *** is-letter ************************************************************* op is-letter : Letter -> MM0SExpr . - eq is-letter(a) = 'orl . - eq is-letter(b) = 'orr . + eq is-letter(a) = 'a-in-top-letter . + eq is-letter(b) = 'b-in-top-letter . *** epsilon-implies-ewp *************************************************** --- MetaTheorem: diff --git a/test b/test index 366c473..4b2f204 100755 --- a/test +++ b/test @@ -2,6 +2,8 @@ set -euo pipefail export PYTHONPYCACHEPREFIX='.build/' +./words-theory-gen.py 24-ab-alphabet a b + poetry install poetry run mypy *.py poetry run pytest ./test.py "$@" diff --git a/words-theory-gen.py b/words-theory-gen.py new file mode 100755 index 0000000..d7b05f2 --- /dev/null +++ b/words-theory-gen.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 + +import os, string, itertools, functools, sys +from textwrap import dedent + +def gen_mm0(letters, f, longest): + f.write('import "20-theory-words.mm0";\n') + for lname in letters: + space = ' '*(longest-len(lname)) + symbol_def = dedent(''' + term {0}_symbol{1}: Symbol; + def {0}{1}: Pattern = $ sym {0}_symbol {1}$;'''.format(lname, space)) + f.write(symbol_def) + f.write('\n') + for lname in letters: + space = ' '*(longest-len(lname)) + functional_let = dedent(''' + axiom functional_{0} {1}: $ functional {0}{1} $;'''.format(lname, space)) + f.write(functional_let) + f.write('\n') + for (lname1, lname2) in itertools.combinations(letters, 2): + space1 = ' '*(longest-len(lname1)) + space2 = ' '*(longest-len(lname2)) + no_confusion = dedent(''' + axiom no_confusion_{0}_{1}{2}{3}: $ {0} {2}!= {1} {3}$;'''.format(lname1, lname2, space1, space2)) + f.write(no_confusion) + f.write('\n') + top_letter = 'axiom all_letters: $ top_letter == {} $;'.format(' \/ '.join(letters)) + f.write('\n{}\n'.format(top_letter)) + +def gen_thms(letters, f, longest, str_base): + for lname in letters: + thm = dedent(str_base.format(lname)) + f.write(thm) + f.write('\n') + +def build_str(letters, delim, part_format): + return delim.join(map(part_format.format, letters)) + +def bin_tree_list(n): + if n == 1: + return ['id'] + return [((('orld @ '*(n-2)) + 'orld') if i == 0 else (('orld @ '*(n-i-1)) + 'orrd')) for i in range(n)] + +def gen_mm1(letters, f, longest): + n = len(letters) + f.write('import "{}.mm0";\n'.format(filename)) + f.write('import "23-words-theorems.mm1";\n') + for (lname1, lname2) in itertools.combinations(letters, 2): + no_confusion = dedent(''' + theorem no_confusion_{1}_{0}: $ {1} != {0} $ = '(con3 eq_sym no_confusion_{0}_{1});'''.format(lname1, lname2)) + f.write(no_confusion) + f.write('\n') + for i, lname in enumerate(letters): + if n == 1: + proof = 'eq_to_intro_rev all_letters' + else: + if i == 0: + proof = ('@ syl orl '*(n-2)) + 'orl' + else: + proof = ('@ syl orl '*(n-i-1)) + 'orr' + proof = 'syl (eq_to_intro_rev all_letters) {}'.format(proof) + in_top_letter = dedent(''' + theorem {0}_in_top_letter: $ {0} -> top_letter $ = + \'({1});'''.format(lname, proof)) + f.write(in_top_letter) + f.write('\n') + gen_thms(letters, f, longest, ''' + theorem functional_{0}_concat {{x v: EVar}}: $ exists x (eVar x == {0} . eVar v) $ = + '(functional_l_concat functional_{0});''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_ewp_{0}: $ epsilon /\ {0} <-> bot $ = + '(regex_eq_ewp_l {0}_in_top_letter);''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_ewp_not_{0}: $ (epsilon /\ ~{0}) <-> epsilon $ = + '(ibii anl @ iand id @ dne @ anl regex_eq_ewp_{0});''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_bot_wrt_{0}: $ (derivative {0} bot) <-> bot $ = + '(ibii (regex_eq_der_bot functional_{0}) absurdum);''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_epsilon_wrt_{0}: $ (derivative {0} epsilon) <-> bot $ = + '(regex_eq_der_epsilon functional_{0} {0}_in_top_letter);''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_choice_wrt_{0}: $ (derivative {0} (Alpha \/ Beta)) <-> (derivative {0} Alpha) \/ (derivative {0} Beta) $ = + '(regex_eq_der_choice functional_{0});''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_conj_wrt_{0}: $ (derivative {0} (Alpha /\ Beta)) <-> (derivative {0} Alpha) /\ (derivative {0} Beta) $ = + '(regex_eq_der_conj functional_{0});''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_neg_wrt_{0}: $ (derivative {0} (~ Alpha)) <-> ~ (derivative {0} Alpha) $ = + '(regex_eq_der_neg functional_{0});''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_same_l_wrt_{0}: $ (derivative {0} {0}) <-> epsilon $ = + '(regex_eq_der_same_l functional_{0} {0}_in_top_letter);''') + + for (lname1, lname2) in itertools.permutations(letters, 2): + der_diff_letters = dedent(''' + theorem regex_eq_der_diff_l_{1}_wrt_{0}: $ (derivative {0} {1}) <-> bot $ = + '(regex_eq_der_diff_l functional_{0} functional_{1} {0}_in_top_letter {1}_in_top_letter no_confusion_{0}_{1});'''.format(lname1, lname2)) + f.write(der_diff_letters) + f.write('\n') + + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_concat_wrt_{0}: $ (derivative {0} (Alpha . Beta)) <-> ((derivative {0} Alpha) . Beta) \/ ((epsilon /\ Alpha) . (derivative {0} Beta)) $ = + '(regex_eq_der_concat functional_{0} {0}_in_top_letter);''') + gen_thms(letters, f, longest, ''' + theorem regex_eq_der_kleene_wrt_{0} {{X: SVar}} (Alpha: Pattern X) (X_fresh: $ _sFresh X Alpha $): $ (derivative {0} (kleene X Alpha)) <-> ((derivative {0} Alpha) . (kleene X Alpha)) $ = + '(regex_eq_der_kleene X_fresh functional_{0} {0}_in_top_letter);''') + + der_equality_bi_concrete = dedent(''' + theorem der_equality_bi_concrete: $phi <-> (epsilon /\ phi) \/ ({0})$ = + (named + \'(bitr der_equality_bi + @ oreq2i + @ bitr ( cong_of_equiv_exists + @ bitr (aneq2i (bitr (cong_of_equiv_mem @ eq_to_intro_bi all_letters) + ,(propag_mem_w_fun \'x ${1}$ (atom-map! {2})))) + ancomb) + {3} + )); + '''.format(build_str(letters, ' \/ ', '({0} . (derivative {0} phi))'), + ' \/ '.join(letters), + build_str(letters, ' ', '\'[{0} functional_{0}]'), + functools.reduce('(bitr (cong_of_equiv_exists andir) @ bitr or_exists_bi @ oreqi {0} {1})'.format, + map("(mp ,(func_to_and_ctx_bi 'x $eVar x . derivative (eVar x) phi$) functional_{})".format, + letters)))) + f.write(der_equality_bi_concrete) + + positive_in_fp_interior = dedent(''' + theorem positive_in_fp_interior {{X: SVar}} ({0}: Pattern X) + {1}: + $ _Positive X (epsilon \/ ({2})) $ + = '(positive_in_or positive_disjoint {3}); + '''.format(build_str(letters, ' ', 'phi_{0}'), + build_str(letters, '\n ', '(pos_{0}: $ _Positive X phi_{0} $)'), + build_str(letters, ' \/ ', '{0} . phi_{0}'), + functools.reduce('(positive_in_or {0} {1})'.format, map('(positive_in_concat positive_disjoint pos_{0})'.format, letters)), + )) + f.write(positive_in_fp_interior) + + fp_implies_regex_interior = dedent(''' + theorem fp_implies_regex_interior {{X: SVar}} ({0} rho: Pattern X) + {1} + (he: $ epsilon -> rho $) + {2}: + ---------------------------------------------- + $(mu X (epsilon \/ ({3}))) -> rho$ = + '(KT (positive_in_fp_interior {4}) @ + apply_equiv der_equality_bi_concrete (norm + (norm_imp_l @ norm_sym @ _sSubst_or sSubstitution_disjoint {5}) + (orim (iand id he) {6}) + )); + '''.format(build_str(letters, ' ', 'phi_{0}'), + build_str(letters, '\n ', '(pos_{0}: $ _Positive X phi_{0} $)'), + build_str(letters, '\n ', '(h_{0}: $ s[ rho / X ] phi_{0} -> (derivative {0} rho) $)'), + build_str(letters, ' \/ ', '({0} . phi_{0})'), + build_str(letters, ' ', 'pos_{0}'), + functools.reduce('(_sSubst_or {0} {1})'.format, ['(sSubst_concat_r norm_refl)']*n), + functools.reduce('(orim {0} {1})'.format, map('(framing_concat_r h_{0})'.format, letters)), + )) + f.write(fp_implies_regex_interior) + + top_implies_fp_interior = dedent(''' + theorem top_implies_fp_interior {{X box: SVar}} ({0} {1}: Pattern X box) + {2} + {3} + + {4} + {5} + : ------------------------ + $(mu X (epsilon \/ ({6}))) . top_letter -> (mu X (epsilon \/ ({7})))$ + = '(unwrap_subst appctx_concat_l + @ KT_subst (positive_in_fp_interior {8}) ,(propag_s_subst_adv 'X $epsilon \/ ({9})$ (atom-map! {10})) + @ eori + ( wrap_subst appctx_concat_l + @ rsyl (anl regex_eq_eps_concat_l) + @ unfold_r (positive_in_fp_interior {11}) + @ norm (norm_sym @ norm_imp_r ,(propag_s_subst_adv 'X $epsilon \/ ({9})$ (atom-map! {10}))) + @ orrd + @ rsyl (eq_to_intro all_letters) + {12}) + {13} + ); + '''.format(build_str(letters, ' ', 'fp_unf_{0}'), + build_str(letters, ' ', 'fp_ctximp_{0}'), + build_str(letters, '\n ', '(p_fp_unf_{0}: $ _Positive X fp_unf_{0} $)'), + build_str(letters, '\n ', '(p_fp_ctximp_{0}: $ _Positive X fp_ctximp_{0} $)'), + build_str(letters, '\n ', '(he_{{0}}: $ epsilon -> s[ (mu X (epsilon \/ ({0}))) / X ] fp_unf_{{0}} $)' + .format(build_str(letters, ' \/ ', '{0} . fp_unf_{0}'))), + build_str(letters, '\n ', '(h{{0}}: $ ((s[ (ctximp_app box (sVar box . top_letter) (mu X (epsilon \/ ({0})))) / X ] fp_ctximp_{{0}}) . top_letter)\n -> (s[ (mu X (epsilon \/ ({0}))) / X ] fp_unf_{{0}}) $)' + .format(build_str(letters, ' \/ ', '{0} . fp_unf_{0}'))), + build_str(letters, ' \/ ', '{0} . fp_ctximp_{0}'), + build_str(letters, ' \/ ', '{0} . fp_unf_{0}'), + build_str(letters, ' ', 'p_fp_ctximp_{0}'), + build_str(letters, ' \/ ', '{0} . _'), + build_str(letters, ' ', '\'[{0} #t]'), + build_str(letters, ' ', 'p_fp_unf_{0}'), + functools.reduce('(orim {0} {1})'.format, map('(rsyl (anr regex_eq_eps_concat_r) @ framing_concat_r he_{0})'.format, letters)), + functools.reduce('(eori {0} {1})'.format, map(''' + ( wrap_subst appctx_concat_l + @ rsyl (bi1i @ assoc_concat) + @ unfold_r (positive_in_fp_interior {0}) + @ norm (norm_sym @ norm_imp_r ,(propag_s_subst_adv 'X $epsilon \/ ({1})$ (atom-map! {2}))) + @ orrd + @ {{1}} + @ framing_concat_r h{{0}})'''.format(build_str(letters, ' ', 'p_fp_unf_{0}'), + build_str(letters, ' \/ ', '{0} . _'), + build_str(letters, ' ', '\'[{0} #t]'), + ).format, letters, bin_tree_list(n))), + )) + f.write(top_implies_fp_interior) + + + +assert len(sys.argv) >= 3, "Usage: words-theory-gen *" +filename = sys.argv[1] +letters = sys.argv[2:] + +assert len(set(letters)) == len(letters), "List of letters may not contain duplicates" + +ascii = set(string.ascii_uppercase + string.ascii_lowercase) +assert all(ascii.issuperset(lname) for lname in letters), "Letter names may only be of the form 'a-Z'*" + +longest = max(map(len, letters)) + +f = open("{}.mm0".format(filename), "w") +gen_mm0(letters, f, longest) +f.close() + +f = open("{}.mm1".format(filename), "w") +gen_mm1(letters, f, longest) +f.close()