From bf6d8233aaeb8996c725dee5cfab1e60c22f3423 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 18:33:34 +0200 Subject: [PATCH 1/6] fixed parsing errors --- dtt.mm | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/dtt.mm b/dtt.mm index 46b6456..0214369 100644 --- a/dtt.mm +++ b/dtt.mm @@ -1288,7 +1288,7 @@ $( The conditional (bool recursor). (Contributed by Mario Carneiro, 14-Mar-2016.) $) - kcd $a |- cond i : \ x : Type i , ( two -> ( x -> ( x -> x ) ) ) $. + kcl $a |- cond i : \ x : Type i , ( bool -> ( x -> ( x -> x ) ) ) $. ${ dett.1 $e |- ( ph |= OA : Type i ) $. @@ -1315,6 +1315,8 @@ $c sigma1 $. $c sigma2 $. $c pair $. + $c 1st $. + $c 2nd $. $( The sigma type, the equivalent of an indexed disjoint union in ZFC. (Contributed by Mario Carneiro, 26-Feb-2016.) $) From bde659c5e6c45f61ecffc1a82d49539d1dc50bfd Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 18:34:10 +0200 Subject: [PATCH 2/6] fixed $d conditions --- dtt.mm | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/dtt.mm b/dtt.mm index 0214369..2865afb 100644 --- a/dtt.mm +++ b/dtt.mm @@ -967,7 +967,7 @@ $} ${ - $d x OA $. $d x OB $. + $d x OA $. $d x OB $. $d x OC $. $d x ph $. $( The type of a constant function. (Contributed by Mario Carneiro, 26-Feb-2016.) $) imval $p |- ( A : OA |= ( OA -> OB ) A := OB ) $= @@ -986,6 +986,7 @@ $} ${ + $d x OA $. $d x OB $. kcim.1 $e |- ( ph |= MA : ( OA -> OB ) ) $. kcim.2 $e |- ( ph |= B : OA ) $. $( The type of a combination. @@ -1141,6 +1142,7 @@ OB : Type imax i j ) $. ${ + $d x OA $. $d x ph $. $d x j $. tyld.1 $e |- ( ph |= OA : Type i ) $. tyld.2 $e |- ( ( ph , x : OA ) |= OB : Type j ) $. $( A lambda abstraction representing a pi type is a member of the imax of the @@ -1153,6 +1155,7 @@ $} ${ + $d x OA $. $d x ph $. tylpp.1 $e |- ( ph |= OA : Type i ) $. tylpp.2 $e |- ( ( ph , x : OA ) |= OB : Prop ) $. $( The type of a forall statement. From 33743a6153e6ab4395e5f035e5c9724a6f9ec0c9 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 19:08:54 +0200 Subject: [PATCH 3/6] fixed latex --- dtt.mm | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/dtt.mm b/dtt.mm index 2865afb..83dbc35 100644 --- a/dtt.mm +++ b/dtt.mm @@ -1426,16 +1426,16 @@ htmldef "wff" as 'wff '; althtmldef "wff" as 'wff '; - latexdef "wff" as "{\rm wff}"; + latexdef "wff" as "\mathrm{wff}"; htmldef "var" as 'var '; althtmldef "var" as 'var '; - latexdef "var" as "{\rm var}"; + latexdef "var" as "\mathrm{var}"; htmldef "type" as 'type '; althtmldef "type" as 'type '; - latexdef "type" as "{\rm type}"; + latexdef "type" as "\mathrm{type}"; htmldef "term" as 'term '; althtmldef "term" as 'term '; - latexdef "term" as "{\rm term}"; + latexdef "term" as "\mathrm{term}"; htmldef "|-" as "|- "; althtmldef "|-" as @@ -1580,13 +1580,13 @@ latexdef "?!" as "\exists{!}"; htmldef "typedef" as "typedef "; althtmldef "typedef" as 'typedef '; - latexdef "typedef" as "\mbox{typedef }"; + latexdef "typedef" as "\text{ typedef }"; htmldef "1-1" as "1-1 "; althtmldef "1-1" as '1-1 '; - latexdef "1-1" as "\mbox{1-1 }"; + latexdef "1-1" as "\mathrm{1-1}"; htmldef "onto" as "onto "; althtmldef "onto" as 'onto '; - latexdef "onto" as "\mbox{onto }"; + latexdef "onto" as "\mathrm{onto}"; htmldef "@" as "@"; althtmldef "@" as 'ε'; @@ -1596,5 +1596,3 @@ $) $( 456789012345 (79-character line to adjust text window width) 567890123456 $) - - From 73efadedc15cf00b1d2f1b36067dd180f8114c75 Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 19:23:10 +0200 Subject: [PATCH 4/6] fixed parenthesis --- dtt.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dtt.mm b/dtt.mm index 83dbc35..466f7a2 100644 --- a/dtt.mm +++ b/dtt.mm @@ -1340,7 +1340,7 @@ $( Type of the sigma type. (Contributed by Mario Carneiro, 26-Feb-2016.) $) ksig $a |- sigma i j : \ x : Type i , \ y : ( x -> Type j ) , - Type max suc u0 max i j ) $. + ( Type max suc u0 max i j ) $. $( Type of the first component function. (Contributed by Mario Carneiro, 26-Feb-2016.) $) From 36cda4f77b5811f4a85374cb908e4a0794b125cf Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 20:34:09 +0200 Subject: [PATCH 5/6] removed dates below proofs --- dtt.mm | 94 ++++------------------------------------------------------ 1 file changed, 6 insertions(+), 88 deletions(-) diff --git a/dtt.mm b/dtt.mm index 466f7a2..b949805 100644 --- a/dtt.mm +++ b/dtt.mm @@ -138,7 +138,6 @@ (Contributed by Mario Carneiro, 25-Feb-2016.) $) idi $p |- ph $= ( ) B $. - $( [25-Feb-2016] $) $} $( Axiom _Simp_. @@ -165,7 +164,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) a1i $p |- ( ps |= ph ) $= ( wi ax-1 ax-mp ) ABADCABEF $. - $( [26-Feb-2016] $) $} ${ @@ -175,7 +173,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) mpd $p |- ( ph |= ch ) $= ( wi ax-2 ax-mp ) ABFZACFZDABCFFIJFEABCGHH $. - $( [26-Feb-2016] $) $} ${ @@ -185,14 +182,12 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) syl $p |- ( ph |= ch ) $= ( wi a1i mpd ) ABCDBCFAEGH $. - $( [26-Feb-2016] $) $} $( The identity inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) id $p |- ( ph |= ph ) $= ( wi ax-1 mpd ) AAABZAAACAECD $. - $( [26-Feb-2016] $) ${ ax-imp.1 $e |- ( ph |= ( ps |= ch ) ) $. @@ -204,7 +199,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) imp $p |- ( ( ph , ps ) |= ch ) $= ( ax-imp ) ABCDE $. - $( [26-Feb-2016] $) $} ${ @@ -217,7 +211,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) ex $p |- ( ph |= ( ps |= ch ) ) $= ( ax-ex ) ABCDE $. - $( [26-Feb-2016] $) $} ${ @@ -227,7 +220,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) jca $p |- ( ph |= ( ps , ch ) ) $= ( wa wi id ex syl mpd ) ACBCFZEABCLGDBCLLHIJK $. - $( [26-Feb-2016] $) $} ${ @@ -238,7 +230,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) syl2anc $p |- ( ph |= th ) $= ( wa jca syl ) ABCHDABCEFIGJ $. - $( [26-Feb-2016] $) $} ${ @@ -249,20 +240,17 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) mp2an $p |- ch $= ( a1i syl2anc ax-mp ) ACDAABCAADGBAEGFHI $. - $( [26-Feb-2016] $) $} $( Extract an assumption from the context. (Contributed by Mario Carneiro, 26-Feb-2016.) $) simpl $p |- ( ( ph , ps ) |= ph ) $= ( ax-1 imp ) ABAABCD $. - $( [26-Feb-2016] $) $( Extract an assumption from the context. (Contributed by Mario Carneiro, 26-Feb-2016.) $) simpr $p |- ( ( ph , ps ) |= ps ) $= ( wi id a1i imp ) ABBBBCABDEF $. - $( [26-Feb-2016] $) $( "Definition" of tautology. (Contributed by Mario Carneiro, 25-Feb-2016.) $) @@ -272,7 +260,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) tru $p |- T. $= ( ax-tru ) A $. - $( [26-Feb-2016] $) ${ trud.1 $e |- ( T. |= ph ) $. @@ -280,7 +267,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) trud $p |- ph $= ( wtru tru ax-mp ) CADBE $. - $( [26-Feb-2016] $) $} ${ @@ -290,7 +276,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) mpdan $p |- ( ph |= ch ) $= ( ex mpd ) ABCDABCEFG $. - $( [26-Feb-2016] $) $} ${ @@ -299,13 +284,11 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) simpld $p |- ( ph |= ps ) $= ( wa simpl syl ) ABCEBDBCFG $. - $( [26-Feb-2016] $) $( Extract an assumption from the context. (Contributed by Mario Carneiro, 26-Feb-2016.) $) simprd $p |- ( ph |= ch ) $= ( wa simpr syl ) ABCECDBCFG $. - $( [26-Feb-2016] $) $} ${ @@ -314,7 +297,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) ancoms $p |- ( ( ps , ph ) |= ch ) $= ( wa simpr simpl syl2anc ) BAEABCBAFBAGDH $. - $( [26-Feb-2016] $) $} ${ @@ -323,13 +305,11 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) adantr $p |- ( ( ph , ps ) |= ch ) $= ( wa simpl syl ) ABEACABFDG $. - $( [26-Feb-2016] $) $( Extract an assumption from the context. (Contributed by Mario Carneiro, 26-Feb-2016.) $) adantl $p |- ( ( ps , ph ) |= ch ) $= ( adantr ancoms ) ABCABCDEF $. - $( [26-Feb-2016] $) $} ${ @@ -338,13 +318,11 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) anim1i $p |- ( ( ph , ch ) |= ( ps , ch ) ) $= ( wa adantr simpr jca ) ACEBCACBDFACGH $. - $( [26-Feb-2016] $) $( Introduce a left conjunct. (Contributed by Mario Carneiro, 26-Feb-2016.) $) anim2i $p |- ( ( ch , ph ) |= ( ch , ps ) ) $= ( wa simpl adantl jca ) CAECBCAFACBDGH $. - $( [26-Feb-2016] $) $} ${ @@ -354,7 +332,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) syldan $p |- ( ( ph , ps ) |= th ) $= ( wa simpl syl2anc ) ABGACDABHEFI $. - $( [26-Feb-2016] $) $} ${ @@ -364,7 +341,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) sylan $p |- ( ( ph , ch ) |= th ) $= ( wa anim1i syl ) ACGBCGDABCEHFI $. - $( [26-Feb-2016] $) $} ${ @@ -373,13 +349,11 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) an32s $p |- ( ( ( ph , ch ) , ps ) |= th ) $= ( wa simpl anim1i simpr adantr syl2anc ) ACFZBFABFCDLABACGHLBCACIJEK $. - $( [26-Feb-2016] $) $( Associativity for context. (Contributed by Mario Carneiro, 26-Feb-2016.) $) anasss $p |- ( ( ph , ( ps , ch ) ) |= th ) $= ( wa id ancoms sylan an32s ) BCFADBACDBAFABFZCDABKKGHEIJH $. - $( [26-Feb-2016] $) $} ${ @@ -388,7 +362,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) anassrs $p |- ( ( ( ph , ps ) , ch ) |= th ) $= ( wa simpl adantr simpr anim1i syl2anc ) ABFZCFABCFDLCAABGHLBCABIJEK $. - $( [26-Feb-2016] $) $} $( Reflexivity of equality. @@ -399,13 +372,11 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) deid $p |- OA := OA $= ( ax-deid ) AB $. - $( [26-Feb-2016] $) $( Reflexivity of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) deidd $p |- ( ph |= OA := OA ) $= ( wde deid a1i ) BBCABDE $. - $( [26-Feb-2016] $) $( Transitivity of equality. (Contributed by Mario Carneiro, 25-Feb-2016.) $) @@ -416,7 +387,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) desym $p |- ( OA := OB |= OB := OA ) $= ( wde deidd id ax-detr syl2anc ) ABCZBBCHBACHBDHEBBAFG $. - $( [26-Feb-2016] $) $} ${ @@ -425,7 +395,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) desymi $p |- OB := OA $= ( wde desym ax-mp ) ABDBADCABEF $. - $( [26-Feb-2016] $) ${ desymi.2 $e |- OC := OB $. @@ -433,7 +402,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) detr4i $p |- OA := OC $= ( wde ax-detr mp2an ) ABFCBFACFDEABCGH $. - $( [26-Feb-2016] $) $} detri.2 $e |- OB := OC $. @@ -441,7 +409,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) detri $p |- OA := OC $= ( desymi detr4i ) ABCDBCEFG $. - $( [26-Feb-2016] $) $} ${ @@ -450,7 +417,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) desymd $p |- ( ph |= OB := OA ) $= ( wde desym syl ) ABCECBEDBCFG $. - $( [26-Feb-2016] $) ${ desymd.2 $e |- ( ph |= OC := OB ) $. @@ -458,7 +424,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) detr4d $p |- ( ph |= OA := OC ) $= ( wde ax-detr syl2anc ) ABCGDCGBDGEFBCDHI $. - $( [26-Feb-2016] $) $} detrd.2 $e |- ( ph |= OB := OC ) $. @@ -466,7 +431,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) detrd $p |- ( ph |= OA := OC ) $= ( desymd detr4d ) ABCDEACDFGH $. - $( [26-Feb-2016] $) $} ${ @@ -478,7 +442,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) 3detr4d $p |- ( ph |= OC := OD ) $= ( detr4d ) ADBEGAECBHFII $. - $( [26-Feb-2016] $) $} ${ @@ -488,7 +451,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) 3detr3d $p |- ( ph |= OC := OD ) $= ( desymd detrd ) ADCEADBCABDGIFJHJ $. - $( [26-Feb-2016] $) $} ${ @@ -498,7 +460,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) 3detr4g $p |- ( ph |= OC := OD ) $= ( wde a1i 3detr4d ) ABCDEFDBIAGJECIAHJK $. - $( [26-Feb-2016] $) $} ${ @@ -508,7 +469,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) 3detr3g $p |- ( ph |= OC := OD ) $= ( wde a1i 3detr3d ) ABCDEFBDIAGJCEIAHJK $. - $( [26-Feb-2016] $) $} $} @@ -524,7 +484,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) bd $p |- ( ph |= ( OA ) := OA ) $= ( to mt om wde df-b a1i ) BCDEBFABGH $. - $( [26-Feb-2016] $) ${ bded.1 $e |- ( ph |= OA := OB ) $. @@ -532,7 +491,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) bded $p |- ( ph |= ( OA ) := ( OB ) ) $= ( to mt om df-b 3detr4g ) ABCBEFGCEFGDBHCHI $. - $( [26-Feb-2016] $) $} ${ @@ -543,7 +501,6 @@ dektri $p |- OA : OC $= ( wk wde wi desymi ax-deid ax-dek mp2an ax-mp ) BCFZACFZEBAGCCGNOHABDICJB ACCKLM $. - $( [26-Feb-2016] $) $} ${ @@ -553,7 +510,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) kdetri $p |- OA : OC $= ( wk wde wi deid ax-dek mp2an ax-mp ) ABFZACFZDAAGBCGMNHAIEAABCJKL $. - $( [26-Feb-2016] $) $} ${ @@ -564,7 +520,6 @@ dektrd $p |- ( ph |= OA : OC ) $= ( wk wde wi desymd deidd ax-dek syl2anc mpd ) ACDGZBDGZFACBHDDHOPIABCEJAD KCBDDLMN $. - $( [26-Feb-2016] $) $} ${ @@ -574,7 +529,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) kdetrd $p |- ( ph |= OA : OC ) $= ( wk wde wi deidd ax-dek syl2anc mpd ) ABCGZBDGZEABBHCDHNOIABJFBBCDKLM $. - $( [26-Feb-2016] $) $} $( The type of a combination. @@ -592,7 +546,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) kcd $p |- ( ph |= MA B : MB B ) $= ( om mt ol wk mc ax-kc syl2anc ) AEJBKJZDGLMCKJQMCENJCFNJMHIBCDEFGOP $. - $( [26-Feb-2016] $) $} ${ @@ -603,14 +556,12 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) cde12d $p |- ( ph |= MA A := MB B ) $= ( om wde mt mc ax-cde syl2anc ) ADHEHIBJHCJHIBDKHCEKHIFGBCDELM $. - $( [26-Feb-2016] $) $} $( Equality theorem for combination. (Contributed by Mario Carneiro, 26-Feb-2016.) $) cde1d $p |- ( ph |= MA A := MB A ) $= ( mt om deidd cde12d ) ABBCDEABFGHI $. - $( [26-Feb-2016] $) $} ${ @@ -619,7 +570,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) cde2d $p |- ( ph |= MA A := MA B ) $= ( om deidd cde12d ) ABCDDADFGEH $. - $( [26-Feb-2016] $) $} $( Equality theorem for a lambda abstraction. @@ -632,7 +582,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) lde1d $p |- ( ph |= \ x : OA , OC := \ x : OB , OC ) $= ( wde ol ax-lde1 syl ) ABCGBDEHCDEHGFBCDEIJ $. - $( [26-Feb-2016] $) $} ${ @@ -658,7 +607,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) lded $p |- ( ph |= \ x : OA , OB := \ x : OA , OC ) $= ( tv mt om wk wde adantr ax-lde ) ABCDEAEGHIBJCDKFLM $. - $( [26-Feb-2016] $) $} $} @@ -689,20 +637,19 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) hbl1 $p |- ( ph |= ( \ x : OA , \ x : OB , OC ) A := \ x : OB , OC ) $= ( mt om wk ol to mc wde ax-hbl1 syl ) ABHICJBCDEFKZFKLHMIQNGBCDEFOP $. - $( [26-Feb-2016] $) $} ${ $d x OB $. $( If ` x ` does not appear in ` OB ` , then any substitution to ` OB ` - yields ` OB ` again, i.e. ` \ x OB ` is a constant function. $) + yields ` OB ` again, i.e. ` \ x OB ` is a constant function. + (Contributed by Mario Carneiro, 26-Feb-2016.) $) ax-17 $a |- ( A : OA |= ( \ x : OA , OB ) A := OB ) $. a17d.1 $e |- ( ph |= A : OA ) $. $( Deduction form of ~ ax-17 . $) a17d $p |- ( ph |= ( \ x : OA , OB ) A := OB ) $= ( mt om wk ol to mc wde ax-17 syl ) ABGHCIBCDEJKGLHDMFBCDENO $. - $( [26-Feb-2016] $) $} ${ @@ -714,7 +661,6 @@ hbxfrf $p |- ( ( ps , ph ) |= ( \ x : OA , OC ) A := OC ) $= ( wa ol to mt mc om wde lded adantl bded cde1d 3detr4d ) BAJZCDEGKZLMZNOE CDFGKZLMZNOFIUBCUFUDUBUEUCABUEUCPADFEGHQRSTABFEPHRUA $. - $( [26-Feb-2016] $) $} ${ @@ -725,7 +671,6 @@ hbxfr $p |- ( ph |= ( \ x : OA , OC ) A := OC ) $= ( ol to mt mc om wde wi wtru a1i adantr hbxfrf ancoms ex trud ) ABCEFIJKL MENZOPAUCAPUCPABCDEFEDNPGQAPBCDFIJKLMDNHRSTUAUB $. - $( [26-Feb-2016] $) $} ${ @@ -736,18 +681,17 @@ hbc $p |- ( ph |= ( \ x : OA , MA B ) A := MA B ) $= ( mc om ol to mt wde ax-distrc a1i bd detrd cde12d ) ABDCEIJZFKLMIJZBDCMJ ZFKLMIJZLZBDEJFKLMIZIJZTUAUFNABCDEFOPAUDCUEEGAUDMJUCUBAUCQHRSR $. - $( [26-Feb-2016] $) $} ${ $d x y $. $d y A $. $d y ph $. hbl.1 $e |- ( ph |= ( \ x : OA , OB ) A := OB ) $. hbl.2 $e |- ( ph |= ( \ x : OA , OC ) A := OC ) $. - $( Hypothesis builder for lambda abstraction. $) + $( Hypothesis builder for lambda abstraction. + (Contributed by Mario Carneiro, 8-Oct-2014.) $) hbl $p |- ( ph |= ( \ x : OA , \ y : OB , OC ) A := \ y : OB , OC ) $= ( ol to mt mc om wde ax-distrl a1i lde1d lded detrd ) ABCDEGJZFJKLMNZBCDF JKLMNZBCEFJKLMNZGJZUAUBUEOABCDEFGPQAUEDUDGJUAAUCDUDGHRADUDEGISTT $. - $( [8-Oct-2014] $) $} $( Beta-reduce a term. @@ -767,17 +711,16 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) clf $p |- ( ph |= ( \ x : OA , OB ) A := OC ) $= ( ol to mt mc om ax-cl detrd ) ABCDFJKLMNBCEFJKLMNEABCDEFGHOIP $. - $( [26-Feb-2016] $) $} ${ $d x A $. $d x OA $. $d x OC $. cl.1 $e |- ( x := A |= OB := OC ) $. - $( Evaluate a lambda expression. $) + $( Evaluate a lambda expression. + (Contributed by Mario Carneiro, 8-Oct-2014.) $) cl $p |- ( A : OA |= ( \ x : OA , OB ) A := OC ) $= ( mt om wk id tv wde adantl ax-17 clf ) AGHZBIZABCDEQJEKGHPLQCDLFMABDENO $. - $( [8-Oct-2014] $) $} ${ @@ -795,7 +738,6 @@ syl sylan adantl clf ax-lde 3detr3d ) ABCGNZOPZQZBHRZUQSQZHNZUPBDHNAVAU RAURBFGNZUAVAURTAURUPVBAUPUBZABCFEGIJUCUDBFUQHGUEUJUFVCABUTDHAUSPQZBUAZ UGZUSBCDGAVEUHVFAGRPQVDTCDTAVEUIKUKVEAUSBDGNOPSQDTMULUMUNUO $. - $( [26-Feb-2016] $) $} $d x OC $. $d y OB $. @@ -803,7 +745,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) cbv $p |- ( ph |= \ x : OA , OB := \ y : OA , OC ) $= ( tv ax-17 cbvf ) ABCDEFGHIJKGLBCHMHLBDGMN $. - $( [26-Feb-2016] $) $} $( @@ -833,7 +774,6 @@ oveq123d $p |- ( ph |= [ A F B ] := [ C S T ] ) $= ( mt mc om tov cde12d df-ov 3detr4g ) ACBEKZLZLMGDFKZLZLMBCENKMDGFNKMACGS UAABDRTHIOJOBCEPDGFPQ $. - $( [26-Feb-2016] $) $} ${ @@ -842,14 +782,12 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) oveq1d $p |- ( ph |= [ A F B ] := [ C F B ] ) $= ( mt om deidd oveq123d ) ABCDEECAEGHIFACGHIJ $. - $( [26-Feb-2016] $) oveq12d.5 $e |- ( ph |= B := T ) $. $( Equality theorem for binary operation. (Contributed by Mario Carneiro, 26-Feb-2016.) $) oveq12d $p |- ( ph |= [ A F B ] := [ C F T ] ) $= ( mt om deidd oveq123d ) ABCDEEFAEIJKGHL $. - $( [26-Feb-2016] $) $} ${ @@ -858,7 +796,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) oveq2d $p |- ( ph |= [ A F B ] := [ A F T ] ) $= ( mt om deidd oveq12d ) ABCBDEABGHIFJ $. - $( [26-Feb-2016] $) $} ${ @@ -867,7 +804,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) oveqd $p |- ( ph |= [ A F B ] := [ A S B ] ) $= ( mt om deidd oveq123d ) ABCBDECFABGHIACGHIJ $. - $( [26-Feb-2016] $) $} ${ @@ -879,7 +815,6 @@ hbov $p |- ( ph |= ( \ x : OA , [ B F C ] ) A := [ B F C ] ) $= ( mt mc om tov df-ov hbc hbxfr ) ABFDCEKZLZLMCDENKMGCDEOABDFSGABCFRGHIPJP Q $. - $( [26-Feb-2016] $) $} ${ @@ -897,7 +832,6 @@ IUJWCVTAVOWEUKSULVHACDVPGHVHACDGVSTVHAACVOGVHACVNVOKGVNUMVHACCEGVSUNUOVHA CVDGVSTUPUQURVHVQUSVAUTVHBDVPFHVEVGRZVHHUEJKVFQZMZACEFGVHWGVEVSUFZWHWGWBE FQZVHWGRWBWGWJIVBVCWHACFGWITURVHBDFHWFTURSS $. - $( [26-Feb-2016] $) $} $( @@ -923,7 +857,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) kim2 $p |- ( ph |= OC : \ x : OA , OB ) $= ( tim mt om ol wde df-im a1i kdetrd ) ADBCGHIZBCEJZFOPKABCELMN $. - $( [26-Feb-2016] $) $} ${ @@ -934,7 +867,6 @@ imde1d $p |- ( ph |= ( OA -> OC ) := ( OB -> OC ) ) $= ( vx ol tim mt om lde1d df-im 3detr4g ) ABDFGCDFGBDHIJCDHIJABCDFEKBDFLCDF LM $. - $( [26-Feb-2016] $) imde12d.1 $e |- ( ph |= OC := OD ) $. $( Equality theorem for a constant function. @@ -942,7 +874,6 @@ imde12d $p |- ( ph |= ( OA -> OC ) := ( OB -> OD ) ) $= ( vx tim mt om imde1d ol lded df-im 3detr4g detrd ) ABDIJKCDIJKZCEIJKZABC DFLACDHMCEHMRSACDEHGNCDHOCEHOPQ $. - $( [26-Feb-2016] $) $} ${ @@ -951,7 +882,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) imde2d $p |- ( ph |= ( OA -> OB ) := ( OA -> OC ) ) $= ( deidd imde12d ) ABBCDABFEG $. - $( [26-Feb-2016] $) $} ${ @@ -963,7 +893,6 @@ kim1 $p |- ( ph |= \ x : OA , OB : ( OA -> OC ) ) $= ( ol tim mt om ax-kl wde df-im desymi a1i kdetrd ) ABCFIBDFIZBDJKLZABCDEF GHMSTNATSBDFOPQR $. - $( [26-Feb-2016] $) $} ${ @@ -973,7 +902,6 @@ imval $p |- ( A : OA |= ( OA -> OB ) A := OB ) $= ( vx mt om wk tim mc ol to wde df-im df-b detr4i a1i cde1d ax-17 detrd ) AEFBGZABCHEZIFABCDJZKEZIFCTAUAUCUAFZUCFZLTUDUBUEBCDMUBNOPQABCDRS $. - $( [26-Feb-2016] $) kim.1 $e |- ( ph |= OA : OD ) $. kim.2 $e |- ( ph |= OB : OC ) $. @@ -982,7 +910,6 @@ kim $p |- ( ph |= ( OA -> OB ) : ( OA -> OC ) ) $= ( vx tim mt om ol wde df-im a1i tv wk adantr kim1 dektrd ) ABCIJKZBCHLZBD IJKUAUBMABCHNOABCDEHFAHPJKBQCDQGRST $. - $( [26-Feb-2016] $) $} ${ @@ -995,7 +922,6 @@ ( vx mc om tim mt to ol wde df-im a1i bd desymd kdetrd lde1d detrd kcd wk imval syl ) ABEIJBCDKLZIJZDACMZBDEUGHAEJUGJZUILJZDHNZFAUJCDHNZULUJUMOACDH PQACUKDHAUKCACRSZUAUBTABLJZCUKGUNTUCAUOCUDUHDOGBCDUEUFT $. - $( [26-Feb-2016] $) $} ${ @@ -1006,7 +932,6 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) hbim $p |- ( ph |= ( \ x : OA , ( OB -> OC ) ) A := ( OB -> OC ) ) $= ( vy ol tim mt om df-im hbl hbxfr ) ABCDEIJDEKLMFDEINABCDEFIGHOP $. - $( [26-Feb-2016] $) $} $( @@ -1151,7 +1076,6 @@ tyld $p |- ( ph |= \ x : OA , OB : Type imax i j ) $= ( tty mt om wk ol tim uimax kim1 tyim syl2anc ) ABEIJKZLBCDMZBFIJKZNJKLTE FOIJKLGABCUASDGHPBTEFQR $. - $( [26-Feb-2016] $) $} ${ @@ -1164,7 +1088,6 @@ ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( [26-Feb-2016] $) $} $( If ` OB ` contains an element, then it is a type, so it resides in some @@ -1212,7 +1135,6 @@ ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( [26-Feb-2016] $) $( The one type, a type with one element. (Contributed by Mario Carneiro, 14-Mar-2016.) $) @@ -1246,7 +1168,6 @@ ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( [14-Mar-2016] $) $( Type of the one recursor. (Contributed by Mario Carneiro, 14-Mar-2016.) $) @@ -1262,7 +1183,6 @@ ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( [14-Mar-2016] $) $} $( The boolean type, a type with two elements. @@ -1300,12 +1220,10 @@ $( The equality rule for the conditional, true case. (Contributed by Mario Carneiro, 14-Mar-2016.) $) dett $a |- ( ph |= cond i tt A B := A ) $. - $( [26-Feb-2016] $) $( The equality rule for the conditional, false case. (Contributed by Mario Carneiro, 14-Mar-2016.) $) deff $a |- ( ph |= cond i ff A B := B ) $. - $( [26-Feb-2016] $) $} $( From 56a15c9390495859a4b93fcbf55934eedcb1615f Mon Sep 17 00:00:00 2001 From: GinoGiotto <73717712+GinoGiotto@users.noreply.github.com> Date: Fri, 14 Jul 2023 20:37:01 +0200 Subject: [PATCH 6/6] rewrap --- dtt.mm | 664 +++++++++++++++++++++++++++------------------------------ 1 file changed, 312 insertions(+), 352 deletions(-) diff --git a/dtt.mm b/dtt.mm index b949805..330ac68 100644 --- a/dtt.mm +++ b/dtt.mm @@ -94,58 +94,48 @@ $( Let variable ` q ` be a set variable. $) vq $f set q $. - $( A set is a term. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( A set is a term. (Contributed by Mario Carneiro, 25-Feb-2016.) $) tv $a term x $. - $( A term is a middle term. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( A term is a middle term. (Contributed by Mario Carneiro, 25-Feb-2016.) $) mt $a mterm A $. - $( A middle term is an open term. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( A middle term is an open term. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) om $a oterm MA $. - $( An open term with parentheses is a term. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( An open term with parentheses is a term. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) to $a term ( OA ) $. - $( A combination (function application). Middle terms are used for ensuring + $( A combination (function application). Middle terms are used for ensuring left-associativity of combination, with higher precedence than lambda - abstraction. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + abstraction. (Contributed by Mario Carneiro, 25-Feb-2016.) $) mc $a mterm MA B $. - $( A lambda abstraction is a term. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( A lambda abstraction is a term. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) ol $a oterm \ x : OA , OB $. - $( Typehood assertion. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Typehood assertion. (Contributed by Mario Carneiro, 25-Feb-2016.) $) wk $a wff OA : OB $. - $( Definitional equality. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Definitional equality. (Contributed by Mario Carneiro, 25-Feb-2016.) $) wde $a wff OA := OB $. - $( Context operator. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Context operator. (Contributed by Mario Carneiro, 25-Feb-2016.) $) wa $a wff ( ph , ps ) $. - $( A deduction is a wff. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( A deduction is a wff. (Contributed by Mario Carneiro, 25-Feb-2016.) $) wi $a wff ( ph |= ps ) $. - $( Tautology is a wff. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Tautology is a wff. (Contributed by Mario Carneiro, 25-Feb-2016.) $) wtru $a wff T. $. ${ idi.1 $e |- ph $. - $( The identity inference. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( The identity inference. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) idi $p |- ph $= ( ) B $. $} - $( Axiom _Simp_. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Axiom _Simp_. (Contributed by Mario Carneiro, 25-Feb-2016.) $) ax-1 $a |- ( ph |= ( ps |= ph ) ) $. - $( Axiom _Frege_. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Axiom _Frege_. (Contributed by Mario Carneiro, 25-Feb-2016.) $) ax-2 $a |- ( ( ph |= ( ps |= ch ) ) |= ( ( ph |= ps ) |= ( ph |= ch ) ) ) $. ${ @@ -153,15 +143,14 @@ min $e |- ph $. $( Major premise for modus ponens. $) maj $e |- ( ph |= ps ) $. - $( Rule of Modus Ponens. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Rule of Modus Ponens. (Contributed by Mario Carneiro, 25-Feb-2016.) $) ax-mp $a |- ps $. $} ${ a1i.1 $e |- ph $. - $( Change an empty context into any context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Change an empty context into any context. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) a1i $p |- ( ps |= ph ) $= ( wi ax-1 ax-mp ) ABADCABEF $. $} @@ -169,8 +158,8 @@ ${ mpd.1 $e |- ( ph |= ps ) $. mpd.2 $e |- ( ph |= ( ps |= ch ) ) $. - $( Modus ponens deduction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Modus ponens deduction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) mpd $p |- ( ph |= ch ) $= ( wi ax-2 ax-mp ) ABFZACFZDABCFFIJFEABCGHH $. $} @@ -178,37 +167,35 @@ ${ syl.1 $e |- ( ph |= ps ) $. syl.2 $e |- ( ps |= ch ) $. - $( Syllogism inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Syllogism inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) syl $p |- ( ph |= ch ) $= ( wi a1i mpd ) ABCDBCFAEGH $. $} - $( The identity inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The identity inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) id $p |- ( ph |= ph ) $= ( wi ax-1 mpd ) AAABZAAACAECD $. ${ ax-imp.1 $e |- ( ph |= ( ps |= ch ) ) $. - $( Importation for context conjunction. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Importation for context conjunction. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) ax-imp $a |- ( ( ph , ps ) |= ch ) $. - $( Importation for context conjunction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Importation for context conjunction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) imp $p |- ( ( ph , ps ) |= ch ) $= ( ax-imp ) ABCDE $. $} ${ ax-ex.1 $e |- ( ( ph , ps ) |= ch ) $. - $( Exportation for context conjunction. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Exportation for context conjunction. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) ax-ex $a |- ( ph |= ( ps |= ch ) ) $. - $( Exportation for context conjunction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Exportation for context conjunction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ex $p |- ( ph |= ( ps |= ch ) ) $= ( ax-ex ) ABCDE $. $} @@ -216,8 +203,7 @@ ${ jca.1 $e |- ( ph |= ps ) $. jca.2 $e |- ( ph |= ch ) $. - $( Syllogism inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Syllogism inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) jca $p |- ( ph |= ( ps , ch ) ) $= ( wa wi id ex syl mpd ) ACBCFZEABCLGDBCLLHIJK $. $} @@ -226,8 +212,7 @@ syl2anc.1 $e |- ( ph |= ps ) $. syl2anc.2 $e |- ( ph |= ch ) $. syl2anc.3 $e |- ( ( ps , ch ) |= th ) $. - $( Syllogism inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Syllogism inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) syl2anc $p |- ( ph |= th ) $= ( wa jca syl ) ABCHDABCEFIGJ $. $} @@ -236,35 +221,34 @@ mp2an.1 $e |- ph $. mp2an.2 $e |- ps $. mp2an.3 $e |- ( ( ph , ps ) |= ch ) $. - $( An inference based on modus ponens. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( An inference based on modus ponens. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) mp2an $p |- ch $= ( a1i syl2anc ax-mp ) ACDAABCAADGBAEGFHI $. $} - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) simpl $p |- ( ( ph , ps ) |= ph ) $= ( ax-1 imp ) ABAABCD $. - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) simpr $p |- ( ( ph , ps ) |= ps ) $= ( wi id a1i imp ) ABBBBCABDEF $. - $( "Definition" of tautology. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( "Definition" of tautology. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) ax-tru $a |- T. $. - $( Tautology is provable. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Tautology is provable. (Contributed by Mario Carneiro, 26-Feb-2016.) $) tru $p |- T. $= ( ax-tru ) A $. ${ trud.1 $e |- ( T. |= ph ) $. - $( Eliminate ` T. ` as an antecedent. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Eliminate ` T. ` as an antecedent. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) trud $p |- ph $= ( wtru tru ax-mp ) CADBE $. $} @@ -272,55 +256,55 @@ ${ mpdan.1 $e |- ( ph |= ps ) $. mpdan.2 $e |- ( ( ph , ps ) |= ch ) $. - $( Modus ponens deduction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Modus ponens deduction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) mpdan $p |- ( ph |= ch ) $= ( ex mpd ) ABCDABCEFG $. $} ${ simpld.1 $e |- ( ph |= ( ps , ch ) ) $. - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) simpld $p |- ( ph |= ps ) $= ( wa simpl syl ) ABCEBDBCFG $. - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) simprd $p |- ( ph |= ch ) $= ( wa simpr syl ) ABCECDBCFG $. $} ${ ancoms.1 $e |- ( ( ph , ps ) |= ch ) $. - $( Swap the two elements of a context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Swap the two elements of a context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ancoms $p |- ( ( ps , ph ) |= ch ) $= ( wa simpr simpl syl2anc ) BAEABCBAFBAGDH $. $} ${ adantr.1 $e |- ( ph |= ch ) $. - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) adantr $p |- ( ( ph , ps ) |= ch ) $= ( wa simpl syl ) ABEACABFDG $. - $( Extract an assumption from the context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Extract an assumption from the context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) adantl $p |- ( ( ps , ph ) |= ch ) $= ( adantr ancoms ) ABCABCDEF $. $} ${ anim2i.1 $e |- ( ph |= ps ) $. - $( Introduce a right conjunct. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Introduce a right conjunct. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) anim1i $p |- ( ( ph , ch ) |= ( ps , ch ) ) $= ( wa adantr simpr jca ) ACEBCACBDFACGH $. - $( Introduce a left conjunct. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Introduce a left conjunct. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) anim2i $p |- ( ( ch , ph ) |= ( ch , ps ) ) $= ( wa simpl adantl jca ) CAECBCAFACBDGH $. $} @@ -328,8 +312,7 @@ ${ syldan.1 $e |- ( ( ph , ps ) |= ch ) $. syldan.2 $e |- ( ( ph , ch ) |= th ) $. - $( Syllogism inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Syllogism inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) syldan $p |- ( ( ph , ps ) |= th ) $= ( wa simpl syl2anc ) ABGACDABHEFI $. $} @@ -337,98 +320,91 @@ ${ sylan.1 $e |- ( ph |= ps ) $. sylan.2 $e |- ( ( ps , ch ) |= th ) $. - $( Syllogism inference. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Syllogism inference. (Contributed by Mario Carneiro, 26-Feb-2016.) $) sylan $p |- ( ( ph , ch ) |= th ) $= ( wa anim1i syl ) ACGBCGDABCEHFI $. $} ${ an32s.1 $e |- ( ( ( ph , ps ) , ch ) |= th ) $. - $( Commutation identity for context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Commutation identity for context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) an32s $p |- ( ( ( ph , ch ) , ps ) |= th ) $= ( wa simpl anim1i simpr adantr syl2anc ) ACFZBFABFCDLABACGHLBCACIJEK $. - $( Associativity for context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Associativity for context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) anasss $p |- ( ( ph , ( ps , ch ) ) |= th ) $= ( wa id ancoms sylan an32s ) BCFADBACDBAFABFZCDABKKGHEIJH $. $} ${ anassrs.1 $e |- ( ( ph , ( ps , ch ) ) |= th ) $. - $( Associativity for context. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Associativity for context. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) anassrs $p |- ( ( ( ph , ps ) , ch ) |= th ) $= ( wa simpl adantr simpr anim1i syl2anc ) ABFZCFABCFDLCAABGHLBCABIJEK $. $} - $( Reflexivity of equality. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Reflexivity of equality. (Contributed by Mario Carneiro, 25-Feb-2016.) $) ax-deid $a |- OA := OA $. - $( Reflexivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Reflexivity of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) deid $p |- OA := OA $= ( ax-deid ) AB $. - $( Reflexivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Reflexivity of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) deidd $p |- ( ph |= OA := OA ) $= ( wde deid a1i ) BBCABDE $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) ax-detr $a |- ( ( OA := OB , OC := OB ) |= OA := OC ) $. ${ - $( Symmetry of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Symmetry of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) desym $p |- ( OA := OB |= OB := OA ) $= ( wde deidd id ax-detr syl2anc ) ABCZBBCHBACHBDHEBBAFG $. $} ${ desymi.1 $e |- OA := OB $. - $( Symmetry of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Symmetry of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) desymi $p |- OB := OA $= ( wde desym ax-mp ) ABDBADCABEF $. ${ desymi.2 $e |- OC := OB $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) detr4i $p |- OA := OC $= ( wde ax-detr mp2an ) ABFCBFACFDEABCGH $. $} detri.2 $e |- OB := OC $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) detri $p |- OA := OC $= ( desymi detr4i ) ABCDBCEFG $. $} ${ desymd.1 $e |- ( ph |= OA := OB ) $. - $( Symmetry of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Symmetry of equality. (Contributed by Mario Carneiro, 26-Feb-2016.) $) desymd $p |- ( ph |= OB := OA ) $= ( wde desym syl ) ABCECBEDBCFG $. ${ desymd.2 $e |- ( ph |= OC := OB ) $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) detr4d $p |- ( ph |= OA := OC ) $= ( wde ax-detr syl2anc ) ABCGDCGBDGEFBCDHI $. $} detrd.2 $e |- ( ph |= OB := OC ) $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) detrd $p |- ( ph |= OA := OC ) $= ( desymd detr4d ) ABCDEACDFGH $. $} @@ -438,8 +414,8 @@ ${ 3detr4d.2 $e |- ( ph |= OC := OA ) $. 3detr4d.3 $e |- ( ph |= OD := OB ) $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) 3detr4d $p |- ( ph |= OC := OD ) $= ( detr4d ) ADBEGAECBHFII $. $} @@ -447,8 +423,8 @@ ${ 3detr3d.2 $e |- ( ph |= OA := OC ) $. 3detr3d.3 $e |- ( ph |= OB := OD ) $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) 3detr3d $p |- ( ph |= OC := OD ) $= ( desymd detrd ) ADCEADBCABDGIFJHJ $. $} @@ -456,8 +432,8 @@ ${ 3detr4g.2 $e |- OC := OA $. 3detr4g.3 $e |- OD := OB $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) 3detr4g $p |- ( ph |= OC := OD ) $= ( wde a1i 3detr4d ) ABCDEFDBIAGJECIAHJK $. $} @@ -465,30 +441,30 @@ ${ 3detr3g.2 $e |- OA := OC $. 3detr3g.3 $e |- OB := OD $. - $( Transitivity of equality. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transitivity of equality. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) 3detr3g $p |- ( ph |= OC := OD ) $= ( wde a1i 3detr3d ) ABCDEFBDIAGJCEIAHJK $. $} $} - $( Definitional equality applied to a typehood assertion. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Definitional equality applied to a typehood assertion. (Contributed by + Mario Carneiro, 25-Feb-2016.) $) ax-dek $a |- ( ( OA := OB , OC := OD ) |= ( OA : OC |= OB : OD ) ) $. - $( Reduction of parentheses. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Reduction of parentheses. (Contributed by Mario Carneiro, + 25-Feb-2016.) $) df-b $a |- ( OA ) := OA $. - $( Equality theorem for parentheses. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for parentheses. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) bd $p |- ( ph |= ( OA ) := OA ) $= ( to mt om wde df-b a1i ) BCDEBFABGH $. ${ bded.1 $e |- ( ph |= OA := OB ) $. - $( Equality theorem for parentheses. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for parentheses. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) bded $p |- ( ph |= ( OA ) := ( OB ) ) $= ( to mt om df-b 3detr4g ) ABCBEFGCEFGDBHCHI $. $} @@ -496,8 +472,8 @@ ${ dektri.1 $e |- OA := OB $. dektri.2 $e |- OB : OC $. - $( Substitution of equal classes into membership relation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Substitution of equal classes into membership relation. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) dektri $p |- OA : OC $= ( wk wde wi desymi ax-deid ax-dek mp2an ax-mp ) BCFZACFZEBAGCCGNOHABDICJB ACCKLM $. @@ -506,8 +482,8 @@ ${ kdetri.1 $e |- OA : OB $. kdetri.2 $e |- OB := OC $. - $( Substitution of equal classes into membership relation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Substitution of equal classes into membership relation. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) kdetri $p |- OA : OC $= ( wk wde wi deid ax-dek mp2an ax-mp ) ABFZACFZDAAGBCGMNHAIEAABCJKL $. $} @@ -515,8 +491,8 @@ ${ dektrd.1 $e |- ( ph |= OA := OB ) $. dektrd.2 $e |- ( ph |= OB : OC ) $. - $( Substitution of equal classes into membership relation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Substitution of equal classes into membership relation. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) dektrd $p |- ( ph |= OA : OC ) $= ( wk wde wi desymd deidd ax-dek syl2anc mpd ) ACDGZBDGZFACBHDDHOPIABCEJAD KCBDDLMN $. @@ -525,25 +501,25 @@ ${ kdetrd.1 $e |- ( ph |= OA : OB ) $. kdetrd.2 $e |- ( ph |= OB := OC ) $. - $( Substitution of equal classes into membership relation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Substitution of equal classes into membership relation. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) kdetrd $p |- ( ph |= OA : OC ) $= ( wk wde wi deidd ax-dek syl2anc mpd ) ABCGZBDGZEABBHCDHNOIABJFBBCDKLM $. $} - $( The type of a combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-kc $a |- ( ( MA : \ x : A , OB , B : A ) |= MA B : MB B ) $. - $( Equality theorem for a combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-cde $a |- ( ( MA := MB , A := B ) |= MA A := MB B ) $. ${ kcd.1 $e |- ( ph |= MA : \ x : A , OB ) $. kcd.2 $e |- ( ph |= B : A ) $. - $( The type of a combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kcd $p |- ( ph |= MA B : MB B ) $= ( om mt ol wk mc ax-kc syl2anc ) AEJBKJZDGLMCKJQMCENJCFNJMHIBCDEFGOP $. $} @@ -552,34 +528,34 @@ cde12d.1 $e |- ( ph |= MA := MB ) $. ${ cde12d.2 $e |- ( ph |= A := B ) $. - $( Equality theorem for combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) cde12d $p |- ( ph |= MA A := MB B ) $= ( om wde mt mc ax-cde syl2anc ) ADHEHIBJHCJHIBDKHCEKHIFGBCDELM $. $} - $( Equality theorem for combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) cde1d $p |- ( ph |= MA A := MB A ) $= ( mt om deidd cde12d ) ABBCDEABFGHI $. $} ${ cde2d.1 $e |- ( ph |= A := B ) $. - $( Equality theorem for combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) cde2d $p |- ( ph |= MA A := MA B ) $= ( om deidd cde12d ) ABCDDADFGEH $. $} - $( Equality theorem for a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-lde1 $a |- ( OA := OB |= \ x : OA , OC := \ x : OB , OC ) $. ${ lde1d.1 $e |- ( ph |= OA := OB ) $. - $( Equality theorem for a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) lde1d $p |- ( ph |= \ x : OA , OC := \ x : OB , OC ) $= ( wde ol ax-lde1 syl ) ABCGBDEHCDEHGFBCDEIJ $. $} @@ -589,40 +565,39 @@ ${ ax-kl.1 $e |- ( ph |= OA : OD ) $. ax-kl.2 $e |- ( ( ph , x : OA ) |= OB : OC ) $. - $( The type of a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a lambda abstraction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-kl $a |- ( ph |= \ x : OA , OB : \ x : OA , OC ) $. $} ${ ax-lde.2 $e |- ( ( ph , x : OA ) |= OB := OC ) $. - $( Equality theorem for a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-lde $a |- ( ph |= \ x : OA , OB := \ x : OA , OC ) $. $} ${ lded.1 $e |- ( ph |= OB := OC ) $. - $( Equality theorem for a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) lded $p |- ( ph |= \ x : OA , OB := \ x : OA , OC ) $= ( tv mt om wk wde adantr ax-lde ) ABCDEAEGHIBJCDKFLM $. $} $} - $( Axiom of eta reduction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Axiom of eta reduction. (Contributed by Mario Carneiro, 26-Feb-2016.) $) ax-eta $a |- ( MB : \ y : OA , OC |= \ x : OA , MB x := MB ) $. - $( Distribution of combination over substitution. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Distribution of combination over substitution. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-distrc $a |- ( \ x : OA , MA B ) A := ( \ x : OA , MA ) A ( ( \ x : OA , B ) A ) $. ${ $d x y $. $d y A $. - $( Distribution of lambda abstraction over substitution. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Distribution of lambda abstraction over substitution. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) ax-distrl $a |- ( \ x : OA , \ y : OB , OC ) A := \ y : ( \ x : OA , OB ) A , ( \ x : OA , OC ) A $. $} @@ -633,8 +608,8 @@ ${ hbl1.1 $e |- ( ph |= A : OA ) $. - $( Deduction form of ~ ax-hbl1 . - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Deduction form of ~ ax-hbl1 . (Contributed by Mario Carneiro, + 26-Feb-2016.) $) hbl1 $p |- ( ph |= ( \ x : OA , \ x : OB , OC ) A := \ x : OB , OC ) $= ( mt om wk ol to mc wde ax-hbl1 syl ) ABHICJBCDEFKZFKLHMIQNGBCDEFOP $. $} @@ -656,8 +631,8 @@ $d x ph $. hbxfrf.1 $e |- ( ph |= OC := OB ) $. hbxfrf.2 $e |- ( ( ps , ph ) |= ( \ x : OA , OB ) A := OB ) $. - $( Transfer a hypothesis builder to an equivalent expression. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transfer a hypothesis builder to an equivalent expression. (Contributed + by Mario Carneiro, 26-Feb-2016.) $) hbxfrf $p |- ( ( ps , ph ) |= ( \ x : OA , OC ) A := OC ) $= ( wa ol to mt mc om wde lded adantl bded cde1d 3detr4d ) BAJZCDEGKZLMZNOE CDFGKZLMZNOFIUBCUFUDUBUEUCABUEUCPADFEGHQRSTABFEPHRUA $. @@ -666,8 +641,8 @@ ${ hbxfr.1 $e |- OC := OB $. hbxfr.2 $e |- ( ph |= ( \ x : OA , OB ) A := OB ) $. - $( Transfer a hypothesis builder to an equivalent expression. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Transfer a hypothesis builder to an equivalent expression. (Contributed + by Mario Carneiro, 26-Feb-2016.) $) hbxfr $p |- ( ph |= ( \ x : OA , OC ) A := OC ) $= ( ol to mt mc om wde wi wtru a1i adantr hbxfrf ancoms ex trud ) ABCEFIJKL MENZOPAUCAPUCPABCDEFEDNPGQAPBCDFIJKLMDNHRSTUAUB $. @@ -676,8 +651,8 @@ ${ hbc.1 $e |- ( ph |= ( \ x : OA , MA ) A := MA ) $. hbc.2 $e |- ( ph |= ( \ x : OA , B ) A := B ) $. - $( Hypothesis builder for combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Hypothesis builder for combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) hbc $p |- ( ph |= ( \ x : OA , MA B ) A := MA B ) $= ( mc om ol to mt wde ax-distrc a1i bd detrd cde12d ) ABDCEIJZFKLMIJZBDCMJ ZFKLMIJZLZBDEJFKLMIZIJZTUAUFNABCDEFOPAUDCUEEGAUDMJUCUBAUCQHRSR $. @@ -687,28 +662,27 @@ $d x y $. $d y A $. $d y ph $. hbl.1 $e |- ( ph |= ( \ x : OA , OB ) A := OB ) $. hbl.2 $e |- ( ph |= ( \ x : OA , OC ) A := OC ) $. - $( Hypothesis builder for lambda abstraction. - (Contributed by Mario Carneiro, 8-Oct-2014.) $) + $( Hypothesis builder for lambda abstraction. (Contributed by Mario + Carneiro, 8-Oct-2014.) $) hbl $p |- ( ph |= ( \ x : OA , \ y : OB , OC ) A := \ y : OB , OC ) $= ( ol to mt mc om wde ax-distrl a1i lde1d lded detrd ) ABCDEGJZFJKLMNZBCDF JKLMNZBCEFJKLMNZGJZUAUBUEOABCDEFGPQAUEDUDGJUAAUCDUDGHRADUDEGISTT $. $} - $( Beta-reduce a term. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Beta-reduce a term. (Contributed by Mario Carneiro, 26-Feb-2016.) $) ax-beta $a |- ( x : OA |= ( \ x : OA , OB ) x := OB ) $. ${ $d x ph $. ax-cl.1 $e |- ( ph |= A : OA ) $. ax-cl.2 $e |- ( ( ph , x := A ) |= OB := OC ) $. - $( Apply a variable substitution. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Apply a variable substitution. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-cl $a |- ( ph |= ( \ x : OA , OB ) A := ( \ x : OA , OC ) A ) $. clf.3 $e |- ( ph |= ( \ x : OA , OC ) A := OC ) $. - $( Evaluate a lambda expression. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Evaluate a lambda expression. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) clf $p |- ( ph |= ( \ x : OA , OB ) A := OC ) $= ( ol to mt mc om ax-cl detrd ) ABCDFJKLMNBCEFJKLMNEABCDEFGHOIP $. $} @@ -716,8 +690,8 @@ ${ $d x A $. $d x OA $. $d x OC $. cl.1 $e |- ( x := A |= OB := OC ) $. - $( Evaluate a lambda expression. - (Contributed by Mario Carneiro, 8-Oct-2014.) $) + $( Evaluate a lambda expression. (Contributed by Mario Carneiro, + 8-Oct-2014.) $) cl $p |- ( A : OA |= ( \ x : OA , OB ) A := OC ) $= ( mt om wk id tv wde adantl ax-17 clf ) AGHZBIZABCDEQJEKGHPLQCDLFMABDENO $. @@ -731,8 +705,8 @@ ${ cbvf.4 $e |- ( x : OA |= ( \ y : OA , OB ) x := OB ) $. cbvf.5 $e |- ( y : OA |= ( \ x : OA , OC ) y := OC ) $. - $( Change bound variables in a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Change bound variables in a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) cbvf $p |- ( ph |= \ x : OA , OB := \ y : OA , OC ) $= ( ol to mt om tv mc wde wk bd ax-kl dektrd ax-eta desymd wa simpr simpl syl sylan adantl clf ax-lde 3detr3d ) ABCGNZOPZQZBHRZUQSQZHNZUPBDHNAVAU @@ -741,8 +715,8 @@ $} $d x OC $. $d y OB $. - $( Change bound variables in a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Change bound variables in a lambda abstraction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) cbv $p |- ( ph |= \ x : OA , OB := \ y : OA , OC ) $= ( tv ax-17 cbvf ) ABCDEFGHIJKGLBCHMHLBDGMN $. $} @@ -755,22 +729,20 @@ $c [ ] $. - $( Infix operator. - (Contributed by Mario Carneiro, 25-Feb-2016.) $) + $( Infix operator. (Contributed by Mario Carneiro, 25-Feb-2016.) $) tov $a term [ A F B ] $. - $( Infix operator. This is a simple metamath way of cleaning up the syntax + $( Infix operator. This is a simple metamath way of cleaning up the syntax of all these infix operators to make them a bit more readable than the - curried representation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + curried representation. (Contributed by Mario Carneiro, 26-Feb-2016.) $) df-ov $a |- [ A F B ] := F A B $. ${ oveq123d.4 $e |- ( ph |= F := S ) $. oveq123d.5 $e |- ( ph |= A := C ) $. oveq123d.6 $e |- ( ph |= B := T ) $. - $( Equality theorem for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for binary operation. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) oveq123d $p |- ( ph |= [ A F B ] := [ C S T ] ) $= ( mt mc om tov cde12d df-ov 3detr4g ) ACBEKZLZLMGDFKZLZLMBCENKMDGFNKMACGS UAABDRTHIOJOBCEPDGFPQ $. @@ -778,30 +750,30 @@ ${ oveq1d.4 $e |- ( ph |= A := C ) $. - $( Equality theorem for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for binary operation. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) oveq1d $p |- ( ph |= [ A F B ] := [ C F B ] ) $= ( mt om deidd oveq123d ) ABCDEECAEGHIFACGHIJ $. oveq12d.5 $e |- ( ph |= B := T ) $. - $( Equality theorem for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for binary operation. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) oveq12d $p |- ( ph |= [ A F B ] := [ C F T ] ) $= ( mt om deidd oveq123d ) ABCDEEFAEIJKGHL $. $} ${ oveq2d.4 $e |- ( ph |= B := T ) $. - $( Equality theorem for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for binary operation. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) oveq2d $p |- ( ph |= [ A F B ] := [ A F T ] ) $= ( mt om deidd oveq12d ) ABCBDEABGHIFJ $. $} ${ oveqd.4 $e |- ( ph |= F := S ) $. - $( Equality theorem for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for binary operation. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) oveqd $p |- ( ph |= [ A F B ] := [ A S B ] ) $= ( mt om deidd oveq123d ) ABCBDECFABGHIACGHIJ $. $} @@ -810,8 +782,8 @@ hbov.1 $e |- ( ph |= ( \ x : OA , F ) A := F ) $. hbov.2 $e |- ( ph |= ( \ x : OA , B ) A := B ) $. hbov.3 $e |- ( ph |= ( \ x : OA , C ) A := C ) $. - $( Hypothesis builder for binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Hypothesis builder for binary operation. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) hbov $p |- ( ph |= ( \ x : OA , [ B F C ] ) A := [ B F C ] ) $= ( mt mc om tov df-ov hbc hbxfr ) ABFDCEKZLZLMCDENKMGCDEOABDFSGABCFRGHIPJP Q $. @@ -820,8 +792,8 @@ ${ $d x y A $. $d x y B $. $d x y OA $. $d x y OB $. $d x y OD $. ovl.1 $e |- ( ( x := A , y := B ) |= OC := OD ) $. - $( Evaluate a lambda expression in a binary operation. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Evaluate a lambda expression in a binary operation. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) ovl $p |- ( ( A : OA , B : OB ) |= [ A ( \ x : OA , \ y : OB , OC ) B ] := OD ) $= ( mt om wk wa ol to mc wde simpr detrd a17d tov df-ov a1i simpl tv adantr @@ -842,19 +814,18 @@ $c -> $. - $( The function type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The function type. (Contributed by Mario Carneiro, 26-Feb-2016.) $) tim $a term ( OA -> OB ) $. ${ $d x OA $. $d x OB $. $( Definition of the function type, which is just a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + (Contributed by Mario Carneiro, 26-Feb-2016.) $) df-im $a |- ( OA -> OB ) := \ x : OA , OB $. kim2.1 $e |- ( ph |= OC : ( OA -> OB ) ) $. - $( The type of a combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kim2 $p |- ( ph |= OC : \ x : OA , OB ) $= ( tim mt om ol wde df-im a1i kdetrd ) ADBCGHIZBCEJZFOPKABCELMN $. $} @@ -862,15 +833,15 @@ ${ $d x ph $. $d x OA $. $d x OB $. $d x OC $. $d x OD $. imde1d.1 $e |- ( ph |= OA := OB ) $. - $( Equality theorem for a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a constant function. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) imde1d $p |- ( ph |= ( OA -> OC ) := ( OB -> OC ) ) $= ( vx ol tim mt om lde1d df-im 3detr4g ) ABDFGCDFGBDHIJCDHIJABCDFEKBDFLCDF LM $. imde12d.1 $e |- ( ph |= OC := OD ) $. - $( Equality theorem for a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a constant function. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) imde12d $p |- ( ph |= ( OA -> OC ) := ( OB -> OD ) ) $= ( vx tim mt om imde1d ol lded df-im 3detr4g detrd ) ABDIJKCDIJKZCEIJKZABC DFLACDHMCEHMRSACDEHGNCDHOCEHOPQ $. @@ -878,8 +849,8 @@ ${ imde2d.1 $e |- ( ph |= OB := OC ) $. - $( Equality theorem for a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for a constant function. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) imde2d $p |- ( ph |= ( OA -> OB ) := ( OA -> OC ) ) $= ( deidd imde12d ) ABBCDABFEG $. $} @@ -888,8 +859,8 @@ $d x ph $. $d x OA $. $d x OC $. kim1.1 $e |- ( ph |= OA : OD ) $. kim1.2 $e |- ( ( ph , x : OA ) |= OB : OC ) $. - $( The type of a lambda abstraction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a lambda abstraction. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kim1 $p |- ( ph |= \ x : OA , OB : ( OA -> OC ) ) $= ( ol tim mt om ax-kl wde df-im desymi a1i kdetrd ) ABCFIBDFIZBDJKLZABCDEF GHMSTNATSBDFOPQR $. @@ -897,16 +868,16 @@ ${ $d x OA $. $d x OB $. $d x OC $. $d x ph $. - $( The type of a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a constant function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) imval $p |- ( A : OA |= ( OA -> OB ) A := OB ) $= ( vx mt om wk tim mc ol to wde df-im df-b detr4i a1i cde1d ax-17 detrd ) AEFBGZABCHEZIFABCDJZKEZIFCTAUAUCUAFZUCFZLTUDUBUEBCDMUBNOPQABCDRS $. kim.1 $e |- ( ph |= OA : OD ) $. kim.2 $e |- ( ph |= OB : OC ) $. - $( The type of a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a constant function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kim $p |- ( ph |= ( OA -> OB ) : ( OA -> OC ) ) $= ( vx tim mt om ol wde df-im a1i tv wk adantr kim1 dektrd ) ABCIJKZBCHLZBD IJKUAUBMABCHNOABCDEHFAHPJKBQCDQGRST $. @@ -916,8 +887,8 @@ $d x OA $. $d x OB $. kcim.1 $e |- ( ph |= MA : ( OA -> OB ) ) $. kcim.2 $e |- ( ph |= B : OA ) $. - $( The type of a combination. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a combination. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kcim $p |- ( ph |= MA B : OB ) $= ( vx mc om tim mt to ol wde df-im a1i bd desymd kdetrd lde1d detrd kcd wk imval syl ) ABEIJBCDKLZIJZDACMZBDEUGHAEJUGJZUILJZDHNZFAUJCDHNZULUJUMOACDH @@ -928,8 +899,8 @@ $d x y $. $d y ph $. $d y A $. $d y OB $. $d y OC $. hbim.1 $e |- ( ph |= ( \ x : OA , OB ) A := OB ) $. hbim.2 $e |- ( ph |= ( \ x : OA , OC ) A := OC ) $. - $( The type of a constant function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a constant function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) hbim $p |- ( ph |= ( \ x : OA , ( OB -> OC ) ) A := ( OB -> OC ) ) $= ( vy ol tim mt om df-im hbl hbxfr ) ABCDEIJDEKLMFDEINABCDEFIGHOP $. $} @@ -949,7 +920,7 @@ $c Type $. $( Type of types $) $c Prop $. $( Type of propositions $) $c typeof $. $( Typeof operator $) - + $v i j k $. $( Universe variables $) @@ -960,109 +931,104 @@ $( Let variable ` k ` be a universe variable. $) uk $f univ k $. - $( The universe zero. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The universe zero. (Contributed by Mario Carneiro, 26-Feb-2016.) $) uu0 $a univ u0 $. - $( The successor function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The successor function. (Contributed by Mario Carneiro, 26-Feb-2016.) $) usuc $a univ suc i $. - $( The max function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The max function. (Contributed by Mario Carneiro, 26-Feb-2016.) $) umax $a univ max i j $. $( The imax function, which is equal to ` u0 ` if ` j = u0 ` , otherwise - ` imax i j = max i j ` . - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + ` imax i j = max i j ` . (Contributed by Mario Carneiro, 26-Feb-2016.) $) uimax $a univ imax i j $. $( Comparison of universe levels is a deduction. The collection of universe levels, modeled by the natural numbers, is a join-semilattice with a - bottom element and a successor function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + bottom element and a successor function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) wule $a wff i u<_ j $. - $( Ordering of universes is reflexive. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Ordering of universes is reflexive. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-leid $a |- i u<_ i $. - $( Ordering of universes is transitive. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Ordering of universes is transitive. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-letr $a |- ( ( i u<_ j , j u<_ k ) |= i u<_ k ) $. - $( Zero is the bottom element of the universe order. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Zero is the bottom element of the universe order. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-0le $a |- u0 u<_ i $. - $( Comparison of universe levels is a deduction. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Comparison of universe levels is a deduction. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-lesuc $a |- i u<_ suc i $. - $( The successor function is monotonic. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The successor function is monotonic. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-sucle $a |- ( i u<_ j |= suc i u<_ suc j ) $. - $( The maximum function is greater than the first argument. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The maximum function is greater than the first argument. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) ax-max1 $a |- i u<_ max i j $. - $( The maximum function is greater than the second argument. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The maximum function is greater than the second argument. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) ax-max2 $a |- j u<_ max i j $. - $( If both arguments are below a bound, so is the maximum. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( If both arguments are below a bound, so is the maximum. (Contributed by + Mario Carneiro, 26-Feb-2016.) $) ax-lemax $a |- ( ( i u<_ k , j u<_ k ) |= max i j u<_ k ) $. - $( The imax function is less than the max function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The imax function is less than the max function. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-imaxle $a |- imax i j u<_ max i j $. - $( The imax function with zero right argument is zero. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The imax function with zero right argument is zero. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-imax0 $a |- imax i u0 u<_ u0 $. $( The imax function with nonzero right argument is equivalent to the max - function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + function. (Contributed by Mario Carneiro, 26-Feb-2016.) $) ax-imaxsuc $a |- max i suc j u<_ imax i suc j $. - $( The imax function of equal arguments equals the common value. This is + $( The imax function of equal arguments equals the common value. This is provable for the natural numbers but must be assumed here since we only - have the first order theory. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + have the first order theory. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-imaxid $a |- i u<_ imax i i $. $( The type " ` Type i ` " is the set of all types at universe level ` i ` . - The lowest one is ` Prop ` , and each Type is in the next higher one. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + The lowest one is ` Prop ` , and each Type is in the next higher one. + (Contributed by Mario Carneiro, 26-Feb-2016.) $) tty $a term Type i $. - $( The type of propositions. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of propositions. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) tpp $a term Prop $. - $( The type of propositions. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of propositions. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) df-pp $a |- Prop := Type u0 $. $( The typeof operator returns the universe level in which a type resides. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + (Contributed by Mario Carneiro, 26-Feb-2016.) $) uto $a univ typeof OA $. - $( Each type is in the next higher type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Each type is in the next higher type. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kty $a |- Type i : Type suc i $. $( The set of universes is a partial order, so two universe levels that are - less than each other produce definitionally equal type universes. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + less than each other produce definitionally equal type universes. + (Contributed by Mario Carneiro, 26-Feb-2016.) $) tyde $a |- ( ( i u<_ j , j u<_ i ) |= Type i := Type j ) $. $( A lambda abstraction representing a pi type is a member of the imax of the - index type and the type of the target types. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + index type and the type of the target types. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) tyim $a |- ( ( OA : Type i , OB : ( OA -> Type j ) ) |= OB : Type imax i j ) $. @@ -1070,9 +1036,9 @@ $d x OA $. $d x ph $. $d x j $. tyld.1 $e |- ( ph |= OA : Type i ) $. tyld.2 $e |- ( ( ph , x : OA ) |= OB : Type j ) $. - $( A lambda abstraction representing a pi type is a member of the imax of the - index type and the type of the target types. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( A lambda abstraction representing a pi type is a member of the imax of + the index type and the type of the target types. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) tyld $p |- ( ph |= \ x : OA , OB : Type imax i j ) $= ( tty mt om wk ol tim uimax kim1 tyim syl2anc ) ABEIJKZLBCDMZBFIJKZNJKLTE FOIJKLGABCUASDGHPBTEFQR $. @@ -1082,8 +1048,8 @@ $d x OA $. $d x ph $. tylpp.1 $e |- ( ph |= OA : Type i ) $. tylpp.2 $e |- ( ( ph , x : OA ) |= OB : Prop ) $. - $( The type of a forall statement. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The type of a forall statement. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) tylpp $p |- ( ph |= \ x : OA , OB : Prop ) $= ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM @@ -1091,17 +1057,17 @@ $} $( If ` OB ` contains an element, then it is a type, so it resides in some - type universe, labeled by the typeof operator. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + type universe, labeled by the typeof operator. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) ax-to $a |- ( OA : OB |= OB : Type typeof OB ) $. $( If ` OA ` is in the universe level ` i ` , then ` i ` is at least as large - as the universe of ` OA ` . - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + as the universe of ` OA ` . (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-tole $a |- ( OA : Type i |= typeof OA u<_ i ) $. - $( Proof irrelevance for propositions. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Proof irrelevance for propositions. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) ax-irrel $a |- ( OA : Prop |= ( ( OB : OA , OC : OA ) |= OB := OC ) ) $. $( @@ -1113,116 +1079,111 @@ $c one one.* one.rec $. $c bool tt ff cond $. - $( The zero type, a type with no elements. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The zero type, a type with no elements. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) t0 $a term zero $. - $( The zero recursor. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The zero recursor. (Contributed by Mario Carneiro, 14-Mar-2016.) $) t0r $a term zero.rec $. - $( The universe of the zero type. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The universe of the zero type. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) k0 $a |- zero : Type suc u0 $. - $( Definition of the zero recursor, a function to any type. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( Definition of the zero recursor, a function to any type. (Contributed by + Mario Carneiro, 14-Mar-2016.) $) k0r $a |- zero.rec i : \ x : Type i , ( zero -> x ) $. - $( The type of the zero recursor. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The type of the zero recursor. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) 0val $p |- ( A : Type i |= zero.rec i A : ( zero -> A ) ) $= ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( The one type, a type with one element. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The one type, a type with one element. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) t1 $a term one $. - $( The sole element of the one type. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The sole element of the one type. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) t1s $a term one.* $. - $( The one recursor. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The one recursor. (Contributed by Mario Carneiro, 14-Mar-2016.) $) t1r $a term one.rec $. $( Definition of the one type, as the set of all functions from zero to - itself. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + itself. (Contributed by Mario Carneiro, 14-Mar-2016.) $) df-1 $a |- one := ( zero -> zero ) $. $( Definition of the unique element of the one type, the identity function on - zero. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + zero. (Contributed by Mario Carneiro, 14-Mar-2016.) $) df-1s $a |- one.* := \ x : zero , x $. - $( Definition of the one recursor. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( Definition of the one recursor. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) df-1r $a |- one.rec i := \ x : Type i , \ y : x , \ z : one , y $. - $( The star is a member of its type. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The star is a member of its type. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) k1s $p |- one.* : one $= ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. - $( Type of the one recursor. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( Type of the one recursor. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) k1r $p |- one.rec i : \ x : Type i , ( x -> ( one -> x ) ) $= ? $. ${ de1s.1 $e |- ( ph |= OA : Type i ) $. de1s.2 $e |- ( ph |= A : OA ) $. - $( The equality rule for the star. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The equality rule for the star. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) de1s $p |- ( ph |= one.rec i A one.* := A ) $= ( ol uu0 uimax tty mt om tpp tv wde df-pp a1i kdetrd wule ax-imax0 ax-0le wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $. $} - $( The boolean type, a type with two elements. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The boolean type, a type with two elements. (Contributed by Mario + Carneiro, 14-Mar-2016.) $) t2 $a term bool $. - $( The first element of the boolean type, "true". - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The first element of the boolean type, "true". (Contributed by Mario + Carneiro, 14-Mar-2016.) $) ttt $a term tt $. - $( The second element of the boolean type, "false". - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The second element of the boolean type, "false". (Contributed by Mario + Carneiro, 14-Mar-2016.) $) tff $a term ff $. - $( The universe of the zero type. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The universe of the zero type. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) k2 $a |- bool : Type suc u0 $. - $( True is a boolean value. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( True is a boolean value. (Contributed by Mario Carneiro, 14-Mar-2016.) $) ktt $a |- tt : bool $. - $( False is a boolean value. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( False is a boolean value. (Contributed by Mario Carneiro, + 14-Mar-2016.) $) kff $a |- ff : bool $. - $( The conditional (bool recursor). - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The conditional (bool recursor). (Contributed by Mario Carneiro, + 14-Mar-2016.) $) kcl $a |- cond i : \ x : Type i , ( bool -> ( x -> ( x -> x ) ) ) $. ${ dett.1 $e |- ( ph |= OA : Type i ) $. dett.2 $e |- ( ph |= A : OA ) $. - dett.3 $e |- ( ph |= B : OA ) $. - $( The equality rule for the conditional, true case. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + dett.3 $e |- ( ph |= B : OA ) $. + $( The equality rule for the conditional, true case. (Contributed by Mario + Carneiro, 14-Mar-2016.) $) dett $a |- ( ph |= cond i tt A B := A ) $. - $( The equality rule for the conditional, false case. - (Contributed by Mario Carneiro, 14-Mar-2016.) $) + $( The equality rule for the conditional, false case. (Contributed by + Mario Carneiro, 14-Mar-2016.) $) deff $a |- ( ph |= cond i ff A B := B ) $. $} @@ -1243,35 +1204,34 @@ (Contributed by Mario Carneiro, 26-Feb-2016.) $) tsig $a term sigma i j $. - $( The first component function for a sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The first component function for a sigma type. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) t1st $a term 1st i j $. - $( The second component function for a sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The second component function for a sigma type. (Contributed by Mario + Carneiro, 26-Feb-2016.) $) t2nd $a term 2nd i j $. - $( The pair function for a sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( The pair function for a sigma type. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) tpair $a term pair i j $. - $( Type of the sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Type of the sigma type. (Contributed by Mario Carneiro, 26-Feb-2016.) $) ksig $a |- sigma i j : \ x : Type i , \ y : ( x -> Type j ) , ( Type max suc u0 max i j ) $. - $( Type of the first component function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Type of the first component function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) k1st $a |- 1st i j : \ x : Type i , \ y : ( x -> Type j ) , ( sigma i j x y -> x ) $. - $( Type of the second component function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Type of the second component function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) k2nd $a |- 2nd i j : \ x : Type i , \ y : ( x -> Type j ) , \ p : sigma i j x y , y ( sigma1 i j x y p ) $. - $( Type of the pair function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Type of the pair function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kpair $a |- pair i j : \ x : Type i , \ y : ( x -> Type j ) , \ p : x , ( y p -> sigma i j x y ) $. @@ -1280,17 +1240,17 @@ kpair1.2 $e |- ( ph |= B : ( A -> Type j ) ) $. kpair1.3 $e |- ( ph |= C : A ) $. kpair1.4 $e |- ( ph |= D : B C ) $. - $( Type of the pair function. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Type of the pair function. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) kpaird $p |- ( ph |= pair i j A B C D : sigma i j A B ) $= ? $. - $( Equality theorem for the sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for the sigma type. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) desig1 $a |- ( ph |= sigma1 i j A B pair i j A B C D := C ) $. - $( Equality theorem for the sigma type. - (Contributed by Mario Carneiro, 26-Feb-2016.) $) + $( Equality theorem for the sigma type. (Contributed by Mario Carneiro, + 26-Feb-2016.) $) desig2 $a |- ( ph |= sigma2 i j A B pair i j A B C D := D ) $. $}