Logiweb(TM)

Logiweb extract of Peano

Up Help

Table of contents

Date of publication
Bibliography
Definitions
Charges

Date of publication

GRD-2009-11-28.UTC:11:17:40.281380 (Gregorian Date / Universal Coordinated Time)
MJD-55163.TAI:11:18:14.281380 (Modified Julian Day / International Atomic Time)
LGT-4766123894281380e-6 (Logiweb Time)

Bibliography

[0] Peano (0176CD88B275E1404092783C6E442E09C246B342FAA4A9B28DBBD8BB0806)
[1] check (014E93CEDBCA44EB611BC0974861950432277A602795E9B4F2BAD8BB0806)
[2] base (01AB1F51C8C17606A5C0331B5689B4858C796547B9A0A4AEF0BCB2BB0806)

Definitions

Peano

Index 0 of page Peano

lgcdef lgcname of Peano as "Peano" enddef

define claim of Peano as [test1 &c defcheck] &c proofcheck end define

lgcdef lgccharge of Peano as "0" enddef

expand-all ( " )

Index 1 of page Peano

lgcdef lgcname of expand-all ( lgcvar ) as "expand-all ( ""! )" enddef

define value of expand-all ( x ) as norm [x is val : LET x BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [u IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [v IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET stateexpand ( u , s , c ) BE [asterisk IN LET asterisk BE [u IN LET stateexpand ( v , s , c ) BE [asterisk IN LET asterisk BE [v IN expand-all1 ( t , u , v )]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of expand-all ( lgcvar ) as "0" enddef

expand-all1 ( " , " , " )

Index 2 of page Peano

lgcdef lgcname of expand-all1 ( lgcvar , lgcvar , lgcvar ) as "expand-all1 ( ""! , ""! , ""! )" enddef

define value of expand-all1 ( t , u , v ) as norm [t is val : [u is val : [v is val : if .not. [u r= quote x ,, y end quote] then make-root ( t , quote f.allfunc \ u unquote . [v unquote] end quote ) :: [[make-root ( t , quote \ u unquote . [v unquote] end quote ) :: [u :: [v :: true]]] :: true] else expand-all1 ( t , u first , expand-all1 ( t , u second , v ) )]]] end define

lgcdef lgccharge of expand-all1 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

is-meta-term ( " , " )

Index 3 of page Peano

lgcdef lgcname of is-meta-term ( lgcvar , lgcvar ) as "is-meta-term ( ""! , ""! )" enddef

define value of is-meta-term ( t , c ) as norm [t is val : [c is val : LET t metadef ( c ) BE [asterisk IN LET asterisk BE [d IN if [d != true] .and. [d != "var"] then true else .not. [t stmt-rhs ( c )]]]]] end define

lgcdef lgccharge of is-meta-term ( lgcvar , lgcvar ) as "0" enddef

unitac-hyp

Index 4 of page Peano

lgcdef lgcname of unitac-hyp as "unitac-hyp" enddef

define value of unitac-hyp as norm [true [[ hook-lemma -> quote \ u . unitac-lemma-hyp ( u ) end quote ]] [[ hook-rule -> quote \ u . unitac-rule-hyp ( u ) end quote ]] [[ hook-conclude -> quote \ u . unitac-conclude-hyp ( u ) end quote ]]] end define

lgcdef lgccharge of unitac-hyp as "0" enddef

unitac-lemma-hyp ( " )

Index 5 of page Peano

lgcdef lgcname of unitac-lemma-hyp ( lgcvar ) as "unitac-lemma-hyp ( ""! )" enddef

define value of unitac-lemma-hyp ( x ) as norm [x is val : LET x BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t stmt-rhs ( c ) BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [T IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [r IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN if is-meta-term ( r , c ) then unitac-lemma-std ( x ) else LET s [[ hook-hyp ]] BE [asterisk IN LET asterisk BE [h IN LET unitac-theo ( T , s , c ) BE [asterisk IN LET asterisk BE [a prime IN LET make-root ( t , quote a prime unquote ;; [t unquote Init Deref Ponens] end quote ) :: [a prime :: [[make-root ( t , quote t unquote Init Deref Ponens end quote ) :: [[make-root ( t , quote t unquote Init Deref end quote ) :: [[make-root ( t , quote t unquote Init end quote ) :: [t :: true]] :: true]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( a , quote a unquote ;; [[[A1' Init Deref Ponens at [h unquote]] at [r unquote]] Ponens] end quote ) :: [a :: [[make-root ( a , quote [[A1' Init Deref Ponens at [h unquote]] at [r unquote]] Ponens end quote ) :: [[make-root ( a , quote [A1' Init Deref Ponens at [h unquote]] at [r unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens end quote ) :: [[make-root ( a , quote A1' Init Deref end quote ) :: [[make-root ( a , quote A1' Init end quote ) :: [[make-root ( a , quote A1' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [r :: true]]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote h unquote imply [r unquote] end quote ) :: [h :: [r :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of unitac-lemma-hyp ( lgcvar ) as "0" enddef

unitac-rule-hyp ( " )

Index 6 of page Peano

lgcdef lgcname of unitac-rule-hyp ( lgcvar ) as "unitac-rule-hyp ( ""! )" enddef

define value of unitac-rule-hyp ( x ) as norm [x is val : LET x BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t stmt-rhs ( c ) BE [asterisk IN LET asterisk BE [r IN if is-meta-term ( r , c ) then unitac-rule-std ( x ) else LET s [[ hook-hyp ]] BE [asterisk IN LET asterisk BE [h IN LET unitac-theo ( t , s , c ) BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote a unquote Deref end quote ) :: [a :: true] BE [asterisk IN LET asterisk BE [a IN LET make-root ( a , quote a unquote ;; [[[A1' Init Deref Ponens at [h unquote]] at [r unquote]] Ponens] end quote ) :: [a :: [[make-root ( a , quote [[A1' Init Deref Ponens at [h unquote]] at [r unquote]] Ponens end quote ) :: [[make-root ( a , quote [A1' Init Deref Ponens at [h unquote]] at [r unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens end quote ) :: [[make-root ( a , quote A1' Init Deref end quote ) :: [[make-root ( a , quote A1' Init end quote ) :: [[make-root ( a , quote A1' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [r :: true]]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote h unquote imply [r unquote] end quote ) :: [h :: [r :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of unitac-rule-hyp ( lgcvar ) as "0" enddef

unitac-conclude-hyp ( " )

Index 7 of page Peano

lgcdef lgcname of unitac-conclude-hyp ( lgcvar ) as "unitac-conclude-hyp ( ""! )" enddef

define value of unitac-conclude-hyp ( x ) as norm [x is val : LET x BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [q IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [r IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN if is-meta-term ( r , c ) then unitac-conclude-std ( x ) else LET s [[ hook-hyp ]] BE [asterisk IN LET asterisk BE [h IN LET unieval ( q , s , c ) BE [asterisk IN LET asterisk BE [s IN LET f.unitac-adapt ( r mathdef ( c ) , s , c ) BE [asterisk IN LET asterisk BE [s IN LET make-root ( r , quote h unquote imply [r unquote] end quote ) :: [h :: [r :: true]] BE [asterisk IN LET asterisk BE [r IN LET unify ( s [[ hook-res ]] , r , s [[ hook-uni ]] ) BE [asterisk IN LET asterisk BE [u IN [s [[ hook-uni -> u ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of unitac-conclude-hyp ( lgcvar ) as "0" enddef

tactic-hyp ( " )

Index 8 of page Peano

lgcdef lgcname of tactic-hyp ( lgcvar ) as "tactic-hyp ( ""! )" enddef

define value of tactic-hyp ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET s [[ hook-hyp ]] BE [asterisk IN LET asterisk BE [h IN if h then tactic-first-hyp ( t , s , c ) else tactic-next-hyp ( h , t , s , c )]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-hyp ( lgcvar ) as "0" enddef

tactic-dummyhyp ( " )

Index 9 of page Peano

lgcdef lgcname of tactic-dummyhyp ( lgcvar ) as "tactic-dummyhyp ( ""! )" enddef

define value of tactic-dummyhyp ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [n IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET s [[ hook-hyp ]] BE [asterisk IN LET asterisk BE [h IN if .not. h then taceval ( n , s , c ) else LET tactic-first-hyp ( true :: [true :: [quote tt end quote :: [n :: <<>>]]] , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-res ]] second BE [asterisk IN LET asterisk BE [r IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( a , quote a unquote ;; [[LElimHyp Init Deref Ponens at [r unquote]] Ponens] end quote ) :: [a :: [[make-root ( a , quote [LElimHyp Init Deref Ponens at [r unquote]] Ponens end quote ) :: [[make-root ( a , quote LElimHyp Init Deref Ponens at [r unquote] end quote ) :: [[make-root ( a , quote LElimHyp Init Deref Ponens end quote ) :: [[make-root ( a , quote LElimHyp Init Deref end quote ) :: [[make-root ( a , quote LElimHyp Init end quote ) :: [[make-root ( a , quote LElimHyp end quote ) :: true] :: true]] :: true]] :: true]] :: [r :: true]]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN [s [[ hook-arg -> a ]] [[ hook-res -> r second ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-dummyhyp ( lgcvar ) as "0" enddef

tactic-ded ( " , " )

Index 10 of page Peano

lgcdef lgcname of tactic-ded ( lgcvar , lgcvar ) as "tactic-ded ( ""! , ""! )" enddef

lgcdef lgccharge of tactic-ded ( lgcvar , lgcvar ) as "0" enddef

define tactic of tactic-ded ( l , n ) as \ u . tactic-dummyhyp ( u ) end define

define locate of tactic-ded ( l , n ) as "line" :: 2 end define

tactic-first-hyp ( " , " , " )

Index 11 of page Peano

lgcdef lgcname of tactic-first-hyp ( lgcvar , lgcvar , lgcvar ) as "tactic-first-hyp ( ""! , ""! , ""! )" enddef

define value of tactic-first-hyp ( t , s , c ) as norm [t is val : [s is val : [c is val : LET quote x conclude y end quote BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [r IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [i IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [l IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [x IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE [asterisk IN LET asterisk prime prime prime prime tail BE [asterisk prime prime prime prime IN LET asterisk BE [n IN LET asterisk prime prime prime prime head BE [asterisk IN LET asterisk prime prime prime prime tail BE [asterisk prime prime prime prime IN LET s [[ hook-hyp -> x ]] BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-unitac -> unitac-hyp ]] BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-pre -> add-first-hyp* ( x , s [[ hook-pre ]] , c ) ]] BE [asterisk IN LET asterisk BE [s IN LET make-root ( t , quote x unquote imply [x unquote] end quote ) :: [x :: [x :: true]] BE [asterisk IN LET asterisk BE [x prime IN LET tactic-push ( hook-pre , l :: [x prime :: [[make-root ( x prime , quote x prime unquote Init end quote ) :: [x prime :: true]] :: <<>>]] , s ) BE [asterisk IN LET asterisk BE [s IN LET taceval ( n , s , c ) BE [asterisk IN LET asterisk BE [s IN [s [[ hook-arg -> make-root ( t , quote [Mend1.8 Init Deref Ponens at [x unquote]] ;; [s [[ hook-arg ]] unquote] end quote ) :: [[make-root ( t , quote Mend1.8 Init Deref Ponens at [x unquote] end quote ) :: [[make-root ( t , quote Mend1.8 Init Deref Ponens end quote ) :: [[make-root ( t , quote Mend1.8 Init Deref end quote ) :: [[make-root ( t , quote Mend1.8 Init end quote ) :: [[make-root ( t , quote Mend1.8 end quote ) :: true] :: true]] :: true]] :: true]] :: [x :: true]]] :: [s [[ hook-arg ]] :: true]] ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-first-hyp ( lgcvar , lgcvar , lgcvar ) as "0" enddef

add-first-hyp* ( " , " , " )

Index 12 of page Peano

lgcdef lgcname of add-first-hyp* ( lgcvar , lgcvar , lgcvar ) as "add-first-hyp* ( ""! , ""! , ""! )" enddef

define value of add-first-hyp* ( h , p , c ) as norm [h is val : [p is val : [c is val : if p then true else [add-first-hyp ( h , p head , c ) :: add-first-hyp* ( h , p tail , c )]]]] end define

lgcdef lgccharge of add-first-hyp* ( lgcvar , lgcvar , lgcvar ) as "0" enddef

add-first-hyp ( " , " , " )

Index 13 of page Peano

lgcdef lgcname of add-first-hyp ( lgcvar , lgcvar , lgcvar ) as "add-first-hyp ( ""! , ""! , ""! )" enddef

define value of add-first-hyp ( h , p , c ) as norm [h is val : [p is val : [c is val : LET p BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [l IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [r IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [a IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN if is-meta-term ( r , c ) then p else LET make-root ( a , quote [[A1' Init Deref Ponens at [h unquote]] at [r unquote]] ;; [a unquote] end quote ) :: [[make-root ( a , quote [A1' Init Deref Ponens at [h unquote]] at [r unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( a , quote A1' Init Deref Ponens end quote ) :: [[make-root ( a , quote A1' Init Deref end quote ) :: [[make-root ( a , quote A1' Init end quote ) :: [[make-root ( a , quote A1' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [r :: true]]] :: [a :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote h unquote imply [r unquote] end quote ) :: [h :: [r :: true]] BE [asterisk IN LET asterisk BE [r IN [l :: [r :: [a :: <<>>]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of add-first-hyp ( lgcvar , lgcvar , lgcvar ) as "0" enddef

tactic-next-hyp ( " , " , " , " )

Index 14 of page Peano

lgcdef lgcname of tactic-next-hyp ( lgcvar , lgcvar , lgcvar , lgcvar ) as "tactic-next-hyp ( ""! , ""! , ""! , ""! )" enddef

define value of tactic-next-hyp ( h , t , s , c ) as norm [h is val : [t is val : [s is val : [c is val : LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [l IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [x IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime prime IN LET asterisk prime prime prime prime head BE [asterisk IN LET asterisk prime prime prime prime tail BE [asterisk prime prime prime prime IN LET asterisk BE [n IN LET asterisk prime prime prime prime head BE [asterisk IN LET asterisk prime prime prime prime tail BE [asterisk prime prime prime prime IN LET make-root ( t , quote h unquote and [x unquote] end quote ) :: [h :: [x :: true]] BE [asterisk IN LET asterisk BE [h prime IN LET s [[ hook-hyp -> h prime ]] BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-pre -> add-next-hyp* ( x , s [[ hook-pre ]] , c ) ]] BE [asterisk IN LET asterisk BE [s IN LET make-root ( t , quote h prime unquote imply [x unquote] end quote ) :: [h prime :: [x :: true]] BE [asterisk IN LET asterisk BE [x prime IN LET tactic-push ( hook-pre , l :: [x prime :: [[make-root ( x prime , quote x prime unquote Init end quote ) :: [x prime :: true]] :: <<>>]] , s ) BE [asterisk IN LET asterisk BE [s IN LET taceval ( n , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN if [.not. [r r= quote x imply y end quote]] .or. .not. [r first r= quote x and y end quote] then error ( x , LocateProofLine ( x , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET make-root ( t , quote [Mend1.48e Init Deref Ponens at [h unquote]] at [x unquote] end quote ) :: [[make-root ( t , quote Mend1.48e Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote Mend1.48e Init Deref Ponens end quote ) :: [[make-root ( t , quote Mend1.48e Init Deref end quote ) :: [[make-root ( t , quote Mend1.48e Init end quote ) :: [[make-root ( t , quote Mend1.48e end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [x :: true]] BE [asterisk IN LET asterisk BE [a prime IN LET make-root ( t , quote [[[Lcurry Init Deref Ponens at [r first first unquote]] at [r first second unquote]] at [r second unquote]] Ponens end quote ) :: [[make-root ( t , quote [[Lcurry Init Deref Ponens at [r first first unquote]] at [r first second unquote]] at [r second unquote] end quote ) :: [[make-root ( t , quote [Lcurry Init Deref Ponens at [r first first unquote]] at [r first second unquote] end quote ) :: [[make-root ( t , quote Lcurry Init Deref Ponens at [r first first unquote] end quote ) :: [[make-root ( t , quote Lcurry Init Deref Ponens end quote ) :: [[make-root ( t , quote Lcurry Init Deref end quote ) :: [[make-root ( t , quote Lcurry Init end quote ) :: [[make-root ( t , quote Lcurry end quote ) :: true] :: true]] :: true]] :: true]] :: [r first first :: true]]] :: [r first second :: true]]] :: [r second :: true]]] :: true] BE [asterisk IN LET asterisk BE [a prime prime IN LET make-root ( t , quote r first first unquote imply [r first second unquote imply [r second unquote]] end quote ) :: [r first first :: [[make-root ( t , quote r first second unquote imply [r second unquote] end quote ) :: [r first second :: [r second :: true]]] :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> make-root ( t , quote a prime unquote ;; [s [[ hook-arg ]] unquote ;; [a prime prime unquote]] end quote ) :: [a prime :: [[make-root ( t , quote s [[ hook-arg ]] unquote ;; [a prime prime unquote] end quote ) :: [s [[ hook-arg ]] :: [a prime prime :: true]]] :: true]] ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-next-hyp ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

add-next-hyp* ( " , " , " )

Index 15 of page Peano

lgcdef lgcname of add-next-hyp* ( lgcvar , lgcvar , lgcvar ) as "add-next-hyp* ( ""! , ""! , ""! )" enddef

define value of add-next-hyp* ( x , p , c ) as norm [x is val : [p is val : [c is val : if p then true else [add-next-hyp ( x , p head , c ) :: add-next-hyp* ( x , p tail , c )]]]] end define

lgcdef lgccharge of add-next-hyp* ( lgcvar , lgcvar , lgcvar ) as "0" enddef

add-next-hyp ( " , " , " )

Index 16 of page Peano

lgcdef lgcname of add-next-hyp ( lgcvar , lgcvar , lgcvar ) as "add-next-hyp ( ""! , ""! , ""! )" enddef

define value of add-next-hyp ( x , p , c ) as norm [x is val : [p is val : [c is val : LET p BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [l IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [t IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [a IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN if is-meta-term ( t , c ) then p else LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [h IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [r IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET make-root ( a , quote a unquote ;; [[[[Lnexthyp Init Deref Ponens at [h unquote]] at [x unquote]] at [r unquote]] Ponens] end quote ) :: [a :: [[make-root ( a , quote [[[Lnexthyp Init Deref Ponens at [h unquote]] at [x unquote]] at [r unquote]] Ponens end quote ) :: [[make-root ( a , quote [[Lnexthyp Init Deref Ponens at [h unquote]] at [x unquote]] at [r unquote] end quote ) :: [[make-root ( a , quote [Lnexthyp Init Deref Ponens at [h unquote]] at [x unquote] end quote ) :: [[make-root ( a , quote Lnexthyp Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( a , quote Lnexthyp Init Deref Ponens end quote ) :: [[make-root ( a , quote Lnexthyp Init Deref end quote ) :: [[make-root ( a , quote Lnexthyp Init end quote ) :: [[make-root ( a , quote Lnexthyp end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [x :: true]]] :: [r :: true]]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote [h unquote and [x unquote]] imply [r unquote] end quote ) :: [[make-root ( r , quote h unquote and [x unquote] end quote ) :: [h :: [x :: true]]] :: [r :: true]] BE [asterisk IN LET asterisk BE [r IN [l :: [r :: [a :: <<>>]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of add-next-hyp ( lgcvar , lgcvar , lgcvar ) as "0" enddef

f.unitac-adapt ( " , " , " )

Index 17 of page Peano

lgcdef lgcname of f.unitac-adapt ( lgcvar , lgcvar , lgcvar ) as "f.unitac-adapt ( ""! , ""! , ""! )" enddef

define value of f.unitac-adapt ( t , s , c ) as norm [t is val : [s is val : [c is val : if t = "var" then s else LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN LET r metadef ( c ) BE [asterisk IN LET asterisk BE [d IN if .not. d then s else if .not. [r r= quote x imply y end quote] then error ( r , LocateProofLine ( r , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE [asterisk IN LET asterisk BE [h IN LET r second BE [asterisk IN LET asterisk BE [r IN if .not. [r metadef ( c )] then s else LET r mathdef ( c ) BE [asterisk IN LET asterisk BE [d IN if d = t then s else LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN if d = "all" then f.unitac-adapt-all ( t , h , a , r , r , s [[ hook-idx ]] , true , s , c ) else if d = "imply" then LET r first BE [asterisk IN LET asterisk BE [x IN LET r second BE [asterisk IN LET asterisk BE [y IN LET make-root ( t , quote a unquote ;; [[h unquote imply [x unquote]] Init ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens]] end quote ) :: [a :: [[make-root ( t , quote [h unquote imply [x unquote]] Init ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens] end quote ) :: [[make-root ( t , quote [h unquote imply [x unquote]] Init end quote ) :: [[make-root ( t , quote h unquote imply [x unquote] end quote ) :: [h :: [x :: true]]] :: true]] :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens end quote ) :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens end quote ) :: [[make-root ( t , quote [[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote] end quote ) :: [[make-root ( t , quote [MP' Init Deref Ponens at [h unquote]] at [x unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens end quote ) :: [[make-root ( t , quote MP' Init Deref end quote ) :: [[make-root ( t , quote MP' Init end quote ) :: [[make-root ( t , quote MP' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [x :: true]]] :: [y :: true]]] :: true]] :: true]] :: true]]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( t , quote h unquote imply [y unquote] end quote ) :: [h :: [y :: true]] BE [asterisk IN LET asterisk BE [r IN f.unitac-adapt ( t , s [[ hook-arg -> a ]] [[ hook-res -> r ]] , c )]]]]]]]] else if t then s else error ( a , diag ( "Cannot convert" ) disp ( r ) diag ( "to type ``" ) diag ( t ) diag ( "''" ) end diagnose )]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-adapt ( lgcvar , lgcvar , lgcvar ) as "0" enddef

f.unitac-adapt-all ( " , " , " , " , " , " , " , " , " )

Index 18 of page Peano

lgcdef lgcname of f.unitac-adapt-all ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "f.unitac-adapt-all ( ""! , ""! , ""! , ""! , ""! , ""! , ""! , ""! , ""! )" enddef

define value of f.unitac-adapt-all ( t , h , a , R , r , i , b , s , c ) as norm [t is val : [h is val : [a is val : [R is val : [r is val : [i is val : [b is val : [s is val : [c is val : if r mathdef ( c ) = "all" then LET r First BE [asterisk IN LET asterisk BE [u IN LET r Second BE [asterisk IN LET asterisk BE [r IN LET univar ( a , u , i ) BE [asterisk IN LET asterisk BE [v IN LET [u :: v] :: b BE [asterisk IN LET asterisk BE [b IN f.unitac-adapt-all ( t , h , a , R , r , i + 1 , b , s , c )]]]]]]]] else LET s [[ hook-idx -> i ]] BE [asterisk IN LET asterisk BE [s IN LET f.subst ( r , b , c ) BE [asterisk IN LET asterisk BE [r prime IN LET make-root ( a , quote a unquote ;; [[[[LAP4' Init Deref Ponens at [h unquote]] at [R unquote]] at [r prime unquote]] Verify Ponens] end quote ) :: [a :: [[make-root ( a , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [R unquote]] at [r prime unquote]] Verify Ponens end quote ) :: [[make-root ( a , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [R unquote]] at [r prime unquote]] Verify end quote ) :: [[make-root ( a , quote [[LAP4' Init Deref Ponens at [h unquote]] at [R unquote]] at [r prime unquote] end quote ) :: [[make-root ( a , quote [LAP4' Init Deref Ponens at [h unquote]] at [R unquote] end quote ) :: [[make-root ( a , quote LAP4' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( a , quote LAP4' Init Deref Ponens end quote ) :: [[make-root ( a , quote LAP4' Init Deref end quote ) :: [[make-root ( a , quote LAP4' Init end quote ) :: [[make-root ( a , quote LAP4' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [R :: true]]] :: [r prime :: true]]] :: true]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r prime , quote h unquote imply [r prime unquote] end quote ) :: [h :: [r prime :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-adapt-all ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

f.tacfresh ( " )

Index 19 of page Peano

lgcdef lgcname of f.tacfresh ( lgcvar ) as "f.tacfresh ( ""! )" enddef

lgcdef lgccharge of f.tacfresh ( lgcvar ) as "0" enddef

f.unitac-ponens ( " )

Index 20 of page Peano

lgcdef lgcname of f.unitac-ponens ( lgcvar ) as "f.unitac-ponens ( ""! )" enddef

define value of f.unitac-ponens ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET unieval ( t first , s , c ) BE [asterisk IN LET asterisk BE [s IN LET f.unitac-adapt ( "imply" , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN if .not. [r r= quote x imply y end quote] then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE [asterisk IN LET asterisk BE [h IN LET r second BE [asterisk IN LET asterisk BE [r IN LET r first BE [asterisk IN LET asterisk BE [x IN LET r second BE [asterisk IN LET asterisk BE [y IN LET unieval ( t second , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a prime IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r prime IN if .not. [r prime r= quote x imply y end quote] then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r prime ) end diagnose ) else LET r prime second BE [asterisk IN LET asterisk BE [r prime IN LET s [[ hook-uni ]] BE [asterisk IN LET asterisk BE [u IN LET unify ( x , r prime , u ) BE [asterisk IN LET asterisk BE [u IN LET s [[ hook-uni -> u ]] BE [asterisk IN LET asterisk BE [s IN LET make-root ( t , quote a unquote ;; [a prime unquote ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens]] end quote ) :: [a :: [[make-root ( t , quote a prime unquote ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens] end quote ) :: [a prime :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens end quote ) :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens end quote ) :: [[make-root ( t , quote [[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote] end quote ) :: [[make-root ( t , quote [MP' Init Deref Ponens at [h unquote]] at [x unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens end quote ) :: [[make-root ( t , quote MP' Init Deref end quote ) :: [[make-root ( t , quote MP' Init end quote ) :: [[make-root ( t , quote MP' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [x :: true]]] :: [y :: true]]] :: true]] :: true]] :: true]]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( t , quote h unquote imply [y unquote] end quote ) :: [h :: [y :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-ponens ( lgcvar ) as "0" enddef

f.unitac-Ponens ( " )

Index 21 of page Peano

lgcdef lgcname of f.unitac-Ponens ( lgcvar ) as "f.unitac-Ponens ( ""! )" enddef

define value of f.unitac-Ponens ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET unieval ( t first , s , c ) BE [asterisk IN LET asterisk BE [s IN LET f.unitac-adapt ( "imply" , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN if .not. [r r= quote x imply y end quote] then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE [asterisk IN LET asterisk BE [h IN LET r second BE [asterisk IN LET asterisk BE [r IN LET r first BE [asterisk IN LET asterisk BE [x IN LET r second BE [asterisk IN LET asterisk BE [y IN LET make-root ( t , quote a unquote ;; [[h unquote imply [x unquote]] Init ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens]] end quote ) :: [a :: [[make-root ( t , quote [h unquote imply [x unquote]] Init ;; [[[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens] end quote ) :: [[make-root ( t , quote [h unquote imply [x unquote]] Init end quote ) :: [[make-root ( t , quote h unquote imply [x unquote] end quote ) :: [h :: [x :: true]]] :: true]] :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens Ponens end quote ) :: [[make-root ( t , quote [[[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote]] Ponens end quote ) :: [[make-root ( t , quote [[MP' Init Deref Ponens at [h unquote]] at [x unquote]] at [y unquote] end quote ) :: [[make-root ( t , quote [MP' Init Deref Ponens at [h unquote]] at [x unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote MP' Init Deref Ponens end quote ) :: [[make-root ( t , quote MP' Init Deref end quote ) :: [[make-root ( t , quote MP' Init end quote ) :: [[make-root ( t , quote MP' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [x :: true]]] :: [y :: true]]] :: true]] :: true]] :: true]]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( t , quote h unquote imply [y unquote] end quote ) :: [h :: [y :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-Ponens ( lgcvar ) as "0" enddef

f.unitac-at ( " )

Index 22 of page Peano

lgcdef lgcname of f.unitac-at ( lgcvar ) as "f.unitac-at ( ""! )" enddef

define value of f.unitac-at ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET unieval ( t first , s , c ) BE [asterisk IN LET asterisk BE [s IN LET f.unitac-adapt ( "all" , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN if .not. [r r= quote x imply y end quote] then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE [asterisk IN LET asterisk BE [h IN LET r second BE [asterisk IN LET asterisk BE [r IN LET r First BE [asterisk IN LET asterisk BE [x IN LET r Second BE [asterisk IN LET asterisk BE [y IN LET s [[ hook-idx ]] BE [asterisk IN LET asterisk BE [i IN LET s [[ hook-idx -> i + 1 ]] BE [asterisk IN LET asterisk BE [s IN LET univar ( a , x , i ) BE [asterisk IN LET asterisk BE [v IN LET f.subst ( y , [x :: v] :: <<>> , c ) BE [asterisk IN LET asterisk BE [r prime IN LET make-root ( t , quote a unquote ;; [[[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify Ponens] end quote ) :: [a :: [[make-root ( t , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify Ponens end quote ) :: [[make-root ( t , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify end quote ) :: [[make-root ( t , quote [[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote] end quote ) :: [[make-root ( t , quote [LAP4' Init Deref Ponens at [h unquote]] at [r unquote] end quote ) :: [[make-root ( t , quote LAP4' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote LAP4' Init Deref Ponens end quote ) :: [[make-root ( t , quote LAP4' Init Deref end quote ) :: [[make-root ( t , quote LAP4' Init end quote ) :: [[make-root ( t , quote LAP4' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [r :: true]]] :: [r prime :: true]]] :: true]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote h unquote imply [r prime unquote] end quote ) :: [h :: [r prime :: true]] BE [asterisk IN LET asterisk BE [r IN LET s [[ hook-uni ]] BE [asterisk IN LET asterisk BE [u IN LET unify ( t second , v , u ) BE [asterisk IN LET asterisk BE [u IN LET s [[ hook-uni -> u ]] BE [asterisk IN LET asterisk BE [s IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-at ( lgcvar ) as "0" enddef

f.unitac-At ( " )

Index 23 of page Peano

lgcdef lgcname of f.unitac-At ( lgcvar ) as "f.unitac-At ( ""! )" enddef

define value of f.unitac-At ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET unieval ( t first , s , c ) BE [asterisk IN LET asterisk BE [s IN LET f.unitac-adapt ( "all" , s , c ) BE [asterisk IN LET asterisk BE [s IN LET s [[ hook-arg ]] BE [asterisk IN LET asterisk BE [a IN LET s [[ hook-res ]] BE [asterisk IN LET asterisk BE [r IN if .not. [r r= quote x imply y end quote] then error ( t , LocateProofLine ( t , c ) diag ( "Malformed result of hypothetical reasoning" ) disp ( r ) end diagnose ) else LET r first BE [asterisk IN LET asterisk BE [h IN LET r second BE [asterisk IN LET asterisk BE [r IN LET r First BE [asterisk IN LET asterisk BE [x IN LET r Second BE [asterisk IN LET asterisk BE [y IN LET s [[ hook-idx ]] BE [asterisk IN LET asterisk BE [i IN LET s [[ hook-idx -> i + 1 ]] BE [asterisk IN LET asterisk BE [s IN LET univar ( a , x , i ) BE [asterisk IN LET asterisk BE [v IN LET f.subst ( y , [x :: v] :: <<>> , c ) BE [asterisk IN LET asterisk BE [r prime IN LET make-root ( t , quote a unquote ;; [[[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify Ponens] end quote ) :: [a :: [[make-root ( t , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify Ponens end quote ) :: [[make-root ( t , quote [[[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote]] Verify end quote ) :: [[make-root ( t , quote [[LAP4' Init Deref Ponens at [h unquote]] at [r unquote]] at [r prime unquote] end quote ) :: [[make-root ( t , quote [LAP4' Init Deref Ponens at [h unquote]] at [r unquote] end quote ) :: [[make-root ( t , quote LAP4' Init Deref Ponens at [h unquote] end quote ) :: [[make-root ( t , quote LAP4' Init Deref Ponens end quote ) :: [[make-root ( t , quote LAP4' Init Deref end quote ) :: [[make-root ( t , quote LAP4' Init end quote ) :: [[make-root ( t , quote LAP4' end quote ) :: true] :: true]] :: true]] :: true]] :: [h :: true]]] :: [r :: true]]] :: [r prime :: true]]] :: true]] :: true]] :: true]] BE [asterisk IN LET asterisk BE [a IN LET make-root ( r , quote h unquote imply [r prime unquote] end quote ) :: [h :: [r prime :: true]] BE [asterisk IN LET asterisk BE [r IN [s [[ hook-arg -> a ]] [[ hook-res -> r ]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of f.unitac-At ( lgcvar ) as "0" enddef

sub ( " , " , " , " )

Index 24 of page Peano

lgcdef lgcname of sub ( lgcvar , lgcvar , lgcvar , lgcvar ) as "sub ( ""! , ""! , ""! , ""! )" enddef

Define tex show of sub ( a , b , x , t ) as "".[ a ][" \sim \langle "[ b ][" \, | \, "[ x ][" \, := "[ t ]" \rangle"]]] end define

define macro of sub ( a , b , x , t ) as \ x . expand ( quote macro define sub ( a , b , x , t ) as \ c . sub0 ( quote a end quote , quote b end quote , quote x end quote , quote t end quote , c ) end define end quote , x ) end define

lgcdef lgccharge of sub ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

sub0 ( " , " , " , " , " )

Index 25 of page Peano

lgcdef lgcname of sub0 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "sub0 ( ""! , ""! , ""! , ""! , ""! )" enddef

define value of sub0 ( a , b , x , t , c ) as norm [a is val : [b is val : [x is val : [t is val : [c is val : [x objectvar ( c ) .and. sub1 ( a , b , x , t , c )]]]]]] end define

lgcdef lgccharge of sub0 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

sub1 ( " , " , " , " , " )

Index 26 of page Peano

lgcdef lgcname of sub1 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "sub1 ( ""! , ""! , ""! , ""! , ""! )" enddef

define value of sub1 ( a , b , x , t , c ) as norm [a is val : [b is val : [x is val : [t is val : [c is val : if [b r= quote f.allfunc \ u . v end quote] .and. [b First t= x] then a t= b else if b t= x then a t= t else [[a r= b] .and. sub* ( a tail , b tail , x , t , c )]]]]]] end define

lgcdef lgccharge of sub1 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

sub* ( " , " , " , " , " )

Index 27 of page Peano

lgcdef lgcname of sub* ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "sub* ( ""! , ""! , ""! , ""! , ""! )" enddef

define value of sub* ( a , b , x , t , c ) as norm [a is val : [b is val : [x is val : [t is val : [c is val : [a atom .or. [sub1 ( a head , b head , x , t , c ) .and. sub* ( a tail , b tail , x , t , c )]]]]]]] end define

lgcdef lgccharge of sub* ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

f.subst ( " , " , " )

Index 28 of page Peano

lgcdef lgcname of f.subst ( lgcvar , lgcvar , lgcvar ) as "f.subst ( ""! , ""! , ""! )" enddef

define value of f.subst ( x , s , c ) as norm [x is val : [s is val : [c is val : LET lookup ( x , s , true ) BE [asterisk IN LET asterisk BE [d IN if .not. d then d else LET x valuedef ( c ) BE [asterisk IN LET asterisk BE [d IN if d = 1 then x else if d != 0 then x head :: f.subst* ( x tail , s , c ) else [x head :: [x first :: [f.subst ( x second , remove ( x first , s ) , c ) :: <<>>]]]]]]]]]] end define

lgcdef lgccharge of f.subst ( lgcvar , lgcvar , lgcvar ) as "0" enddef

f.subst* ( " , " , " )

Index 29 of page Peano

lgcdef lgcname of f.subst* ( lgcvar , lgcvar , lgcvar ) as "f.subst* ( ""! , ""! , ""! )" enddef

define value of f.subst* ( x , s , c ) as norm [x is val : [s is val : [c is val : if x atom then true else [f.subst ( x head , s , c ) :: f.subst* ( x tail , s , c )]]]] end define

lgcdef lgccharge of f.subst* ( lgcvar , lgcvar , lgcvar ) as "0" enddef

inst ( " , " )

Index 30 of page Peano

lgcdef lgcname of inst ( lgcvar , lgcvar ) as "inst ( ""! , ""! )" enddef

define macro of inst ( x , y ) as \ x . expand ( quote macro define inst ( x , y ) as \ c . inst0 ( quote x end quote , quote y end quote , c ) end define end quote , x ) end define

lgcdef lgccharge of inst ( lgcvar , lgcvar ) as "0" enddef

inst0 ( " , " , " )

Index 31 of page Peano

lgcdef lgcname of inst0 ( lgcvar , lgcvar , lgcvar ) as "inst0 ( ""! , ""! , ""! )" enddef

define value of inst0 ( x , y , c ) as norm [x is val : [y is val : [c is val : .not. [inst1 ( x , y , c ) catch head]]]] end define

lgcdef lgccharge of inst0 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

inst1 ( " , " , " )

Index 32 of page Peano

lgcdef lgcname of inst1 ( lgcvar , lgcvar , lgcvar ) as "inst1 ( ""! , ""! , ""! )" enddef

define value of inst1 ( x , y , c ) as norm [x is val : [y is val : [c is val : LET inst-strip ( x , true , c ) BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [x IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [u IN LET inst-strip ( y , true , c ) BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [y IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [v IN LET inst-zip ( u , v ) BE [asterisk IN LET asterisk BE [s IN inst2 ( x , y , s , true , c )]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of inst1 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

inst-strip ( " , " , " )

Index 33 of page Peano

lgcdef lgcname of inst-strip ( lgcvar , lgcvar , lgcvar ) as "inst-strip ( ""! , ""! , ""! )" enddef

define value of inst-strip ( x , v , c ) as norm [x is val : [v is val : [c is val : if .not. [x metadef ( c )] then x :: v else if .not. [x valuedef ( c )] then x :: v else if x mathdef ( c ) != "all" then x :: v else if x tail then exception else LET x first BE [asterisk IN LET asterisk BE [x IN if .not. [x metadef ( c )] then exception else if x valuedef ( c ) != 0 then exception else inst-strip ( x second , x first :: v , c )]]]]] end define

lgcdef lgccharge of inst-strip ( lgcvar , lgcvar , lgcvar ) as "0" enddef

inst-zip ( " , " )

Index 34 of page Peano

lgcdef lgcname of inst-zip ( lgcvar , lgcvar ) as "inst-zip ( ""! , ""! )" enddef

define value of inst-zip ( x , y ) as norm [x is val : [y is val : if x then if y then true else exception else [[x head :: [y head]] :: inst-zip ( x tail , y tail )]]] end define

lgcdef lgccharge of inst-zip ( lgcvar , lgcvar ) as "0" enddef

inst2 ( " , " , " , " , " )

Index 35 of page Peano

lgcdef lgcname of inst2 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "inst2 ( ""! , ""! , ""! , ""! , ""! )" enddef

define value of inst2 ( x , y , s , b , c ) as norm [x is val : [y is val : [s is val : [b is val : [c is val : LET lookup ( x , s , false ) BE [asterisk IN LET asterisk BE [d IN if d then [x :: y] :: s else if d pairp then if inst3 ( d , b , c ) then s else exception else if .not. [x r= y] then exception else if .not. [x metadef ( c )] then exception else LET x valuedef ( c ) BE [asterisk IN LET asterisk BE [d IN if d = 1 then if x first = [y first] then s else exception else if d != 0 then inst2* ( x tail , y tail , s , b , c ) else LET x first BE [asterisk IN LET asterisk BE [v IN if .not. [v = [y first]] then exception else if .not. [x objectvar ( c )] then exception else LET remove ( v , s ) BE [asterisk IN LET asterisk BE [s IN inst2 ( x second , y second , s , b set+ v , c )]]]]]]]]]]]]] end define

lgcdef lgccharge of inst2 ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

inst2* ( " , " , " , " , " )

Index 36 of page Peano

lgcdef lgcname of inst2* ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "inst2* ( ""! , ""! , ""! , ""! , ""! )" enddef

define value of inst2* ( x , y , s , b , c ) as norm [x is val : [y is val : [s is val : [b is val : [c is val : if x then s else inst2* ( x tail , y tail , inst2 ( x head , y head , s , b , c ) , b , c )]]]]] end define

lgcdef lgccharge of inst2* ( lgcvar , lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

inst3 ( " , " , " )

Index 37 of page Peano

lgcdef lgcname of inst3 ( lgcvar , lgcvar , lgcvar ) as "inst3 ( ""! , ""! , ""! )" enddef

define value of inst3 ( x , b , c ) as norm [x is val : [b is val : [c is val : if .not. [x metadef ( c )] then false else if .not. [x mathdef ( c )] then inst3* ( x tail , b , c ) else LET x valuedef ( c ) BE [asterisk IN LET asterisk BE [d IN if d then .not. [x member b] else if d = 1 then true else if d != 0 then inst3* ( x tail , b , c ) else inst3 ( x second , b set- [x first] , c )]]]]] end define

lgcdef lgccharge of inst3 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

inst3* ( " , " , " )

Index 38 of page Peano

lgcdef lgcname of inst3* ( lgcvar , lgcvar , lgcvar ) as "inst3* ( ""! , ""! , ""! )" enddef

define value of inst3* ( x , b , c ) as norm [x is val : [b is val : [c is val : if x then true else [inst3 ( x head , b , c ) .and. inst3* ( x tail , b , c )]]]] end define

lgcdef lgccharge of inst3* ( lgcvar , lgcvar , lgcvar ) as "0" enddef

def ( " , " )

Index 39 of page Peano

lgcdef lgcname of def ( lgcvar , lgcvar ) as "def ( ""! , ""! )" enddef

define macro of def ( a , b ) as \ x . expand ( quote macro define def ( a , b ) as \ c . def0 ( quote a end quote , quote b end quote , c ) end define end quote , x ) end define

lgcdef lgccharge of def ( lgcvar , lgcvar ) as "0" enddef

def0 ( " , " , " )

Index 40 of page Peano

lgcdef lgcname of def0 ( lgcvar , lgcvar , lgcvar ) as "def0 ( ""! , ""! , ""! )" enddef

define value of def0 ( a , b , c ) as norm [a is val : [b is val : [c is val : [[def1 ( a , b , c ) .or. def2 ( a , b , c )] .or. def2 ( b , a , c )]]]] end define

lgcdef lgccharge of def0 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

def0* ( " , " , " )

Index 41 of page Peano

lgcdef lgcname of def0* ( lgcvar , lgcvar , lgcvar ) as "def0* ( ""! , ""! , ""! )" enddef

define value of def0* ( a , b , c ) as norm [a is val : [b is val : [c is val : [a atom .or. [def0 ( a head , b head , c ) .and. def0* ( a tail , b tail , c )]]]]] end define

lgcdef lgccharge of def0* ( lgcvar , lgcvar , lgcvar ) as "0" enddef

def1 ( " , " , " )

Index 42 of page Peano

lgcdef lgcname of def1 ( lgcvar , lgcvar , lgcvar ) as "def1 ( ""! , ""! , ""! )" enddef

define value of def1 ( a , b , c ) as norm [a is val : [b is val : [c is val : LET a metadef ( c ) BE [asterisk IN LET asterisk BE [v IN if v = "var" then a t= b else if .not. v then false else LET a valuedef ( c ) BE [asterisk IN LET asterisk BE [v IN if v = 0 then [a first t= [b first]] .and. def0 ( a second , b second , c ) else if v = 1 then a first = [b first] else [[a r= b] .and. def0* ( a tail , b tail , c )]]]]]]]] end define

lgcdef lgccharge of def1 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

def2 ( " , " , " )

Index 43 of page Peano

lgcdef lgcname of def2 ( lgcvar , lgcvar , lgcvar ) as "def2 ( ""! , ""! , ""! )" enddef

define value of def2 ( a , b , c ) as norm [a is val : [b is val : [c is val : [[[a metadef ( c ) = true] .and. [a valuedef ( c ) = true]] .and. LET a def ( c , math ) BE [asterisk IN LET asterisk BE [v IN if [v .or. [v third ref = 0]] .or. .not. checked-def ( a ref , c ) then false else LET zip ( v second tail , a tail ) BE [asterisk IN LET asterisk BE [s IN def3 ( v third , b , s , c )]]]]]]]] end define

lgcdef lgccharge of def2 ( lgcvar , lgcvar , lgcvar ) as "0" enddef

def3 ( " , " , " , " )

Index 44 of page Peano

lgcdef lgcname of def3 ( lgcvar , lgcvar , lgcvar , lgcvar ) as "def3 ( ""! , ""! , ""! , ""! )" enddef

define value of def3 ( a , b , s , c ) as norm [a is val : [b is val : [s is val : [c is val : if .not. [a metadef ( c )] then false else LET a valuedef ( c ) BE [asterisk IN LET asterisk BE [v IN if v = 0 then [b valuedef ( c ) = 0] .and. def3 ( a second , b second , [a first :: [b first]] :: s , c ) else if v = 1 then false else LET a mathdef ( c ) BE [asterisk IN LET asterisk BE [w IN if v .and. [w .or. [w ref = 0]] then b t= lookup ( a , s , true ) else [[a r= b] .and. def3* ( a tail , b tail , s , c )]]]]]]]]] end define

lgcdef lgccharge of def3 ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

def3* ( " , " , " , " )

Index 45 of page Peano

lgcdef lgcname of def3* ( lgcvar , lgcvar , lgcvar , lgcvar ) as "def3* ( ""! , ""! , ""! , ""! )" enddef

define value of def3* ( a , b , s , c ) as norm [a is val : [b is val : [s is val : [c is val : [a atom .or. [def3 ( a head , b head , s , c ) .and. def3* ( a tail , b tail , s , c )]]]]]] end define

lgcdef lgccharge of def3* ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

defcheck

Index 46 of page Peano

lgcdef lgcname of defcheck as "defcheck" enddef

define value of defcheck as \ c . defcheck1 ( c ) end define

lgcdef lgccharge of defcheck as "0" enddef

checked-def ( " , " )

Index 47 of page Peano

lgcdef lgcname of checked-def ( lgcvar , lgcvar ) as "checked-def ( ""! , ""! )" enddef

define value of checked-def ( r , c ) as norm [r is val : [c is val : LET c [[ r ]] [[ "codex" ]] [[ r ]] [[ 0 ]] [[ 0 ]] [[ "claim" ]] third BE [asterisk IN LET asterisk BE [x IN claiming ( quote defcheck end quote , x )]]]] end define

lgcdef lgccharge of checked-def ( lgcvar , lgcvar ) as "0" enddef

defcheck1 ( " )

Index 48 of page Peano

lgcdef lgcname of defcheck1 ( lgcvar ) as "defcheck1 ( ""! )" enddef

define value of defcheck1 ( c ) as norm [c is val : LET c [[ 0 ]] BE [asterisk IN LET asterisk BE [r IN LET c [[ r ]] [[ "codex" ]] [[ r ]] BE [asterisk IN LET asterisk BE [a IN LET defcheck2 ( a , c ) catch BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [e IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [v IN if v != true then diagnose v end diagnose else if .not. e then true else diagnose show quote "In definition soundness checker: unprocessed exception" end quote end show end diagnose]]]]]]]]]]]]] end define

lgcdef lgccharge of defcheck1 ( lgcvar ) as "0" enddef

defcheck2 ( " , " )

Index 49 of page Peano

lgcdef lgcname of defcheck2 ( lgcvar , lgcvar ) as "defcheck2 ( ""! , ""! )" enddef

define value of defcheck2 ( a , c ) as norm [a is val : [c is val : if a = true then true else if .not. [a head intp] then defcheck2 ( a head , c ) .and. defcheck2 ( a tail , c ) else LET a tail [[ 0 ]] [[ math ]] BE [asterisk IN LET asterisk BE [v IN if v .or. [v third ref = 0] then true else if valid-def ( v third , v second tail , v second :: <<>> , c ) then true else error ( v second , diag ( "Definition soundness check of" ) form ( v second ) diag ( "failed." ) diag ( "Error could be in any, transitively used definition" ) diag ( "or could be that the definition is circular." ) end diagnose )]]]] end define

lgcdef lgccharge of defcheck2 ( lgcvar , lgcvar ) as "0" enddef

valid-def ( " , " , " , " )

Index 50 of page Peano

lgcdef lgcname of valid-def ( lgcvar , lgcvar , lgcvar , lgcvar ) as "valid-def ( ""! , ""! , ""! , ""! )" enddef

define value of valid-def ( a , b , s , c ) as norm [a is val : [b is val : [s is val : [c is val : if .not. [a metadef ( c )] then false else LET a valuedef ( c ) BE [asterisk IN LET asterisk BE [v IN if v = 0 then valid-def ( a second , a first :: b , s , c ) else if v = 1 then false else if .not. v then valid-def* ( a tail , b , s , c ) else LET a def ( c , math ) BE [asterisk IN LET asterisk BE [v IN if v then a member b else if .not. valid-def* ( a tail , b , s , c ) then false else if v third ref = 0 then true else if v second ref != [c [[ 0 ]]] then claiming ( v second ref , c ) else if v second member s then false else valid-def ( v third , v second tail , v second :: s , c )]]]]]]]] end define

lgcdef lgccharge of valid-def ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

valid-def* ( " , " , " , " )

Index 51 of page Peano

lgcdef lgcname of valid-def* ( lgcvar , lgcvar , lgcvar , lgcvar ) as "valid-def* ( ""! , ""! , ""! , ""! )" enddef

define value of valid-def* ( a , b , s , c ) as norm [a is val : [b is val : [s is val : [c is val : [a atom .or. [valid-def ( a head , b , s , c ) .and. valid-def* ( a tail , b , s , c )]]]]]] end define

lgcdef lgccharge of valid-def* ( lgcvar , lgcvar , lgcvar , lgcvar ) as "0" enddef

Prop

Index 52 of page Peano

lgcdef lgcname of Prop as "Prop" enddef

lgcdef lgccharge of Prop as "0" enddef

define tactic of Prop as \ u . tactic-Prop ( u ) end define

define statement of Prop as A1 oplus [A2 oplus [A3 oplus [MP oplus Def]]] end define

FOL

Index 53 of page Peano

lgcdef lgcname of FOL as "FOL" enddef

lgcdef lgccharge of FOL as "0" enddef

define tactic of FOL as \ u . tactic-FOL ( u ) end define

define statement of FOL as Prop oplus [A4 oplus [AP4 oplus [A5 oplus Gen]]] end define

PA

Index 54 of page Peano

lgcdef lgcname of PA as "PA" enddef

lgcdef lgccharge of PA as "0" enddef

define tactic of PA as \ u . tactic-FOL ( u ) end define

define statement of PA as FOL oplus [S1 oplus [S2 oplus [S3 oplus [S4 oplus [S5 oplus [S6 oplus [S7 oplus [S8 oplus S9]]]]]]]] end define

MP

Index 55 of page Peano

lgcdef lgcname of MP as "MP" enddef

lgcdef lgccharge of MP as "0" enddef

define unitac of MP as \ u . unitac-rule ( u ) end define

define statement of MP as All #x : All #y : [[#x imply #y] infer [#x infer #y]] end define

Gen

Index 56 of page Peano

lgcdef lgcname of Gen as "Gen" enddef

lgcdef lgccharge of Gen as "0" enddef

define unitac of Gen as \ u . unitac-rule ( u ) end define

define statement of Gen as All #u : All #x : [#x infer f.allfunc \ #u . #x] end define

Def

Index 57 of page Peano

lgcdef lgcname of Def as "Def" enddef

lgcdef lgccharge of Def as "0" enddef

define unitac of Def as \ u . unitac-rule ( u ) end define

define statement of Def as All #x : All #y : [[\ c . def0 ( quote #x end quote , quote #y end quote , c )] endorse [#x infer #y]] end define

A1

Index 58 of page Peano

lgcdef lgcname of A1 as "A1" enddef

lgcdef lgccharge of A1 as "0" enddef

define unitac of A1 as \ u . unitac-rule ( u ) end define

define statement of A1 as All #x : All #y : [#x imply [#y imply #x]] end define

A2

Index 59 of page Peano

lgcdef lgcname of A2 as "A2" enddef

lgcdef lgccharge of A2 as "0" enddef

define unitac of A2 as \ u . unitac-rule ( u ) end define

define statement of A2 as All #x : All #y : All #z : [[#x imply [#y imply #z]] imply [[#x imply #y] imply [#x imply #z]]] end define

A3

Index 60 of page Peano

lgcdef lgcname of A3 as "A3" enddef

lgcdef lgccharge of A3 as "0" enddef

define unitac of A3 as \ u . unitac-rule ( u ) end define

define statement of A3 as All #x : All #y : [[[not #y] imply not #x] imply [[[not #y] imply #x] imply #y]] end define

A4

Index 61 of page Peano

lgcdef lgcname of A4 as "A4" enddef

lgcdef lgccharge of A4 as "0" enddef

define unitac of A4 as \ u . unitac-rule ( u ) end define

define statement of A4 as All #t : All #x : All #a : All #b : [[\ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c )] endorse [[f.allfunc \ #x . #a] imply #b]] end define

AP4

Index 62 of page Peano

lgcdef lgcname of AP4 as "AP4" enddef

lgcdef lgccharge of AP4 as "0" enddef

define unitac of AP4 as \ u . unitac-rule ( u ) end define

define statement of AP4 as All #a : All #b : [[\ c . inst0 ( quote #a end quote , quote #b end quote , c )] endorse [#a imply #b]] end define

A5

Index 63 of page Peano

lgcdef lgcname of A5 as "A5" enddef

lgcdef lgccharge of A5 as "0" enddef

define unitac of A5 as \ u . unitac-rule ( u ) end define

define statement of A5 as All #x : All #a : All #b : [[\ c . [quote #x end quote objectavoid ( c ) quote #a end quote]] endorse [[f.allfunc \ #x . [#a imply #b]] imply [#a imply f.allfunc \ #x . #b]]] end define

tt

Index 64 of page Peano

lgcdef lgcname of tt as "tt" enddef

Define tex show of tt as " \mathtt{\mathbf{T}}" end define

lgcdef lgccharge of tt as "0" enddef

define math of tt as ff imply ff end define

ff

Index 65 of page Peano

lgcdef lgcname of ff as "ff" enddef

Define tex show of ff as " \mathtt{\mathbf{F}}" end define

lgcdef lgccharge of ff as "0" enddef

define math of ff as "ff" end define

S1

Index 66 of page Peano

lgcdef lgcname of S1 as "S1" enddef

lgcdef lgccharge of S1 as "0" enddef

define unitac of S1 as \ u . unitac-rule ( u ) end define

define statement of S1 as f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = y] imply [[x = z] imply [y = z]]] end define

S2

Index 67 of page Peano

lgcdef lgcname of S2 as "S2" enddef

lgcdef lgccharge of S2 as "0" enddef

define unitac of S2 as \ u . unitac-rule ( u ) end define

define statement of S2 as f.allfunc \ x . f.allfunc \ y . [[x = y] imply [x suc = [y suc]]] end define

S3

Index 68 of page Peano

lgcdef lgcname of S3 as "S3" enddef

lgcdef lgccharge of S3 as "0" enddef

define unitac of S3 as \ u . unitac-rule ( u ) end define

define statement of S3 as f.allfunc \ x . not [0 = [x suc]] end define

S4

Index 69 of page Peano

lgcdef lgcname of S4 as "S4" enddef

lgcdef lgccharge of S4 as "0" enddef

define unitac of S4 as \ u . unitac-rule ( u ) end define

define statement of S4 as [f.allfunc \ x . [x suc = [y suc]]] imply [x = y] end define

S5

Index 70 of page Peano

lgcdef lgcname of S5 as "S5" enddef

lgcdef lgccharge of S5 as "0" enddef

define unitac of S5 as \ u . unitac-rule ( u ) end define

define statement of S5 as f.allfunc \ x . [[x + 0] = x] end define

S6

Index 71 of page Peano

lgcdef lgcname of S6 as "S6" enddef

lgcdef lgccharge of S6 as "0" enddef

define unitac of S6 as \ u . unitac-rule ( u ) end define

define statement of S6 as f.allfunc \ x . f.allfunc \ y . [[x + [y suc]] = [[x + y] suc]] end define

S7

Index 72 of page Peano

lgcdef lgcname of S7 as "S7" enddef

lgcdef lgccharge of S7 as "0" enddef

define unitac of S7 as \ u . unitac-rule ( u ) end define

define statement of S7 as f.allfunc \ x . [[x * 0] = 0] end define

S8

Index 73 of page Peano

lgcdef lgcname of S8 as "S8" enddef

lgcdef lgccharge of S8 as "0" enddef

define unitac of S8 as \ u . unitac-rule ( u ) end define

define statement of S8 as f.allfunc \ x . f.allfunc \ y . [[x * [y suc]] = [[x * y] + x]] end define

S9

Index 74 of page Peano

lgcdef lgcname of S9 as "S9" enddef

lgcdef lgccharge of S9 as "0" enddef

define unitac of S9 as \ u . unitac-rule ( u ) end define

define statement of S9 as All #x : All #a : All #z : All #i : [[\ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c )] endorse [[\ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c )] endorse [#z imply [[f.allfunc \ #x . [#a imply #i]] imply #a]]]] end define

Mend1.8

Index 75 of page Peano

lgcdef lgcname of Mend1.8 as "Mend1.8" enddef

lgcdef lgccharge of Mend1.8 as "0" enddef

define proof of Mend1.8 as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #x : Line L03 : A2 >> [#x imply [[#y imply #x] imply #x]] imply [[#x imply [#y imply #x]] imply [#x imply #x]] ; Line L04 : A1 >> #x imply [[#y imply #x] imply #x] ; Line L05 : [MP ponens L03] ponens L04 >> [#x imply [#y imply #x]] imply [#x imply #x] ; Line L06 : A1 >> #x imply [#y imply #x] ; [[[MP ponens L05] ponens L06] conclude [#x imply #x]] end quote , tacstate0 , c ) end define

define unitac of Mend1.8 as \ u . unitac-lemma ( u ) end define

define statement of Mend1.8 as Prop infer All #x : [#x imply #x] end define

A1'

Index 76 of page Peano

lgcdef lgcname of A1' as "A1'" enddef

lgcdef lgccharge of A1' as "0" enddef

define proof of A1' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : Line L03 : Premise >> #a ; [[[MP ponens A1] ponens L03] conclude [#h imply #a]] end quote , tacstate0 , c ) end define

define unitac of A1' as \ u . unitac-lemma ( u ) end define

define statement of A1' as Prop infer All #h : All #a : [#a infer [#h imply #a]] end define

A2'

Index 77 of page Peano

lgcdef lgcname of A2' as "A2'" enddef

lgcdef lgccharge of A2' as "0" enddef

define proof of A2' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : All #b : Line L03 : Premise >> #h imply [#a imply #b] ; Line L04 : Premise >> #h imply #a ; [[[MP ponens [[MP ponens A2] ponens L03]] ponens L04] conclude [#h imply #b]] end quote , tacstate0 , c ) end define

define unitac of A2' as \ u . unitac-lemma ( u ) end define

define statement of A2' as Prop infer All #h : All #a : All #b : [[#h imply [#a imply #b]] infer [[#h imply #a] infer [#h imply #b]]] end define

Mend1.47b

Index 78 of page Peano

lgcdef lgcname of Mend1.47b as "Mend1.47b" enddef

lgcdef lgccharge of Mend1.47b as "0" enddef

define proof of Mend1.47b as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : All #c : Line L03 : Premise >> #a imply #b ; Line L04 : Premise >> #b imply #c ; Line L05 : A1' ponens L04 >> #a imply [#b imply #c] ; [[[A2' ponens L05] ponens L03] conclude [#a imply #c]] end quote , tacstate0 , c ) end define

define unitac of Mend1.47b as \ u . unitac-lemma ( u ) end define

define statement of Mend1.47b as Prop infer All #a : All #b : All #c : [[#a imply #b] infer [[#b imply #c] infer [#a imply #c]]] end define

Mend1.47c

Index 79 of page Peano

lgcdef lgcname of Mend1.47c as "Mend1.47c" enddef

lgcdef lgccharge of Mend1.47c as "0" enddef

define proof of Mend1.47c as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : All #c : Line L03 : Premise >> #a imply [#b imply #c] ; Line L04 : [MP ponens A2] ponens L03 >> [#a imply #b] imply [#a imply #c] ; Line L05 : A1' ponens L04 >> #b imply [[#a imply #b] imply [#a imply #c]] ; Line L06 : [MP ponens A2] ponens L05 >> [#b imply [#a imply #b]] imply [#b imply [#a imply #c]] ; [[[MP ponens L06] ponens [A1 Conclude]] conclude [#b imply [#a imply #c]]] end quote , tacstate0 , c ) end define

define unitac of Mend1.47c as \ u . unitac-lemma ( u ) end define

define statement of Mend1.47c as Prop infer All #a : All #b : All #c : [[#a imply [#b imply #c]] infer [#b imply [#a imply #c]]] end define

Mend1.47d

Index 80 of page Peano

lgcdef lgcname of Mend1.47d as "Mend1.47d" enddef

lgcdef lgccharge of Mend1.47d as "0" enddef

define proof of Mend1.47d as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : All #b : Line L03 : A3 >> [[not #a] imply not #b] imply [[[not #a] imply #b] imply #a] ; Line L04 : Mend1.47c ponens L03 >> [[not #a] imply #b] imply [[[not #a] imply not #b] imply #a] ; Line L05 : A1 >> #b imply [[not #a] imply #b] ; Line L06 : [Mend1.47b ponens L05] ponens L04 >> #b imply [[[not #a] imply not #b] imply #a] ; [[Mend1.47c ponens L06] conclude [[[not #a] imply not #b] imply [#b imply #a]]] end quote , tacstate0 , c ) end define

define unitac of Mend1.47d as \ u . unitac-lemma ( u ) end define

define statement of Mend1.47d as Prop infer All #a : All #b : [[[not #a] imply not #b] imply [#b imply #a]] end define

Mend1.11b

Index 81 of page Peano

lgcdef lgcname of Mend1.11b as "Mend1.11b" enddef

lgcdef lgccharge of Mend1.11b as "0" enddef

define proof of Mend1.11b as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #a : Line L03 : Mend1.8 >> [#a imply ff] imply [#a imply ff] ; Line L04 : Mend1.47c ponens L03 >> #a imply [[#a imply ff] imply ff] ; Line L05 : Def ponens L04 >> #a imply [[not #a] imply ff] ; [[Def ponens L05] conclude [#a imply not not #a]] end quote , tacstate0 , c ) end define

define unitac of Mend1.11b as \ u . unitac-lemma ( u ) end define

define statement of Mend1.11b as Prop infer All #a : [#a imply not not #a] end define

Mend1.48d

Index 82 of page Peano

lgcdef lgcname of Mend1.48d as "Mend1.48d" enddef

lgcdef lgccharge of Mend1.48d as "0" enddef

define proof of Mend1.48d as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : Line L03 : Mend1.8 >> ff imply ff ; Line L04 : Def ponens L03 >> not ff ; Line L05 : A1' ponens L04 >> [not not #x] imply not ff ; Line L06 : [MP ponens Mend1.47d] ponens L05 >> ff imply not #x ; Line L07 : A1' ponens L06 >> #h imply [ff imply not #x] ; Line L08 : [MP ponens A2] ponens L07 >> [#h imply ff] imply [#h imply not #x] ; Line L09 : Def ponens L08 >> [not #h] imply [#h imply not #x] ; Line L10 : Mend1.11b >> [#h imply not #x] imply not not [#h imply not #x] ; Line L11 : [Mend1.47b ponens L09] ponens L10 >> [not #h] imply not not [#h imply not #x] ; Line L12 : [MP ponens Mend1.47d] ponens L11 >> [not [#h imply not #x]] imply #h ; [[Def ponens L12] conclude [[#h and #x] imply #h]] end quote , tacstate0 , c ) end define

define unitac of Mend1.48d as \ u . unitac-lemma ( u ) end define

define statement of Mend1.48d as Prop infer All #h : All #x : [[#h and #x] imply #h] end define

Mend1.48e

Index 83 of page Peano

lgcdef lgcname of Mend1.48e as "Mend1.48e" enddef

lgcdef lgccharge of Mend1.48e as "0" enddef

define proof of Mend1.48e as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : Line L03 : A1 >> [not #x] imply [#h imply not #x] ; Line L04 : Mend1.11b >> [#h imply not #x] imply not not [#h imply not #x] ; Line L05 : [Mend1.47b ponens L03] ponens L04 >> [not #x] imply not not [#h imply not #x] ; Line L06 : [MP ponens Mend1.47d] ponens L05 >> [not [#h imply not #x]] imply #x ; [[Def ponens L06] conclude [[#h and #x] imply #x]] end quote , tacstate0 , c ) end define

define unitac of Mend1.48e as \ u . unitac-lemma ( u ) end define

define statement of Mend1.48e as Prop infer All #h : All #x : [[#h and #x] imply #x] end define

Lnexthyp

Index 84 of page Peano

lgcdef lgcname of Lnexthyp as "Lnexthyp" enddef

lgcdef lgccharge of Lnexthyp as "0" enddef

define proof of Lnexthyp as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : All #y : Line L03 : Premise >> #h imply #y ; Line L04 : Mend1.48d >> [#h and #x] imply #h ; [[[Mend1.47b ponens L04] ponens L03] conclude [[#h and #x] imply #y]] end quote , tacstate0 , c ) end define

define unitac of Lnexthyp as \ u . unitac-lemma ( u ) end define

define statement of Lnexthyp as Prop infer All #h : All #x : All #y : [[#h imply #y] infer [[#h and #x] imply #y]] end define

Lcurry

Index 85 of page Peano

lgcdef lgcname of Lcurry as "Lcurry" enddef

lgcdef lgccharge of Lcurry as "0" enddef

define proof of Lcurry as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #x : All #y : Line L03 : Premise >> [#h and #x] imply #y ; Line L04 : Def ponens L03 >> [not [#h imply not #x]] imply #y ; Line L05 : Mend1.11b >> #y imply not not #y ; Line L06 : [Mend1.47b ponens L04] ponens L05 >> [not [#h imply not #x]] imply not not #y ; Line L07 : [MP ponens Mend1.47d] ponens L06 >> [not #y] imply [#h imply not #x] ; Line L08 : Mend1.47c ponens L07 >> #h imply [[not #y] imply not #x] ; Line L09 : Mend1.47d >> [[not #y] imply not #x] imply [#x imply #y] ; [[[Mend1.47b ponens L08] ponens L09] conclude [#h imply [#x imply #y]]] end quote , tacstate0 , c ) end define

define unitac of Lcurry as \ u . unitac-lemma ( u ) end define

define statement of Lcurry as Prop infer All #h : All #x : All #y : [[[#h and #x] imply #y] infer [#h imply [#x imply #y]]] end define

LTruth

Index 86 of page Peano

lgcdef lgcname of LTruth as "LTruth" enddef

lgcdef lgccharge of LTruth as "0" enddef

define proof of LTruth as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; Line L02 : Mend1.8 >> ff imply ff ; [[Def ponens L02] conclude tt] end quote , tacstate0 , c ) end define

define unitac of LTruth as \ u . unitac-lemma ( u ) end define

define statement of LTruth as Prop infer tt end define

LElimHyp

Index 87 of page Peano

lgcdef lgcname of LElimHyp as "LElimHyp" enddef

lgcdef lgccharge of LElimHyp as "0" enddef

define proof of LElimHyp as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #x : Line L03 : Premise >> tt imply #x ; Line L04 : LTruth >> tt ; [[[MP ponens L03] ponens L04] conclude #x] end quote , tacstate0 , c ) end define

define unitac of LElimHyp as \ u . unitac-lemma ( u ) end define

define statement of LElimHyp as Prop infer All #x : [[tt imply #x] infer #x] end define

LA4'

Index 88 of page Peano

lgcdef lgcname of LA4' as "LA4'" enddef

lgcdef lgccharge of LA4' as "0" enddef

define proof of LA4' as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #t : All #x : All #a : All #b : Line L03 : Condition >> \ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c ) ; Line L04 : Premise >> #h imply f.allfunc \ #x . #a ; Line L05 : A4 probans L03 >> [f.allfunc \ #x . #a] imply #b ; [[[Mend1.47b ponens L04] ponens L05] conclude [#h imply #b]] end quote , tacstate0 , c ) end define

define unitac of LA4' as \ u . unitac-lemma ( u ) end define

define statement of LA4' as FOL infer All #h : All #t : All #x : All #a : All #b : [[\ c . sub0 ( quote #b end quote , quote #a end quote , quote #x end quote , quote #t end quote , c )] endorse [[#h imply f.allfunc \ #x . #a] infer [#h imply #b]]] end define

LAP4'

Index 89 of page Peano

lgcdef lgcname of LAP4' as "LAP4'" enddef

lgcdef lgccharge of LAP4' as "0" enddef

define proof of LAP4' as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #a : All #b : Line L03 : Condition >> \ c . inst0 ( quote #a end quote , quote #b end quote , c ) ; Line L04 : Premise >> #h imply #a ; Line L05 : AP4 probans L03 >> #a imply #b ; [[[Mend1.47b ponens L04] ponens L05] conclude [#h imply #b]] end quote , tacstate0 , c ) end define

define unitac of LAP4' as \ u . unitac-lemma ( u ) end define

define statement of LAP4' as FOL infer All #h : All #a : All #b : [[\ c . inst0 ( quote #a end quote , quote #b end quote , c )] endorse [[#h imply #a] infer [#h imply #b]]] end define

MP'

Index 90 of page Peano

lgcdef lgcname of MP' as "MP'" enddef

lgcdef lgccharge of MP' as "0" enddef

define proof of MP' as \ p . \ c . taceval ( quote Line L01 : Premise >> Prop ; All #h : All #a : All #b : Line L03 : Premise >> #h imply [#a imply #b] ; Line L04 : Premise >> #h imply #a ; Line L05 : A2 >> [#h imply [#a imply #b]] imply [[#h imply #a] imply [#h imply #b]] ; Line L06 : [MP ponens L05] ponens L03 >> [#h imply #a] imply [#h imply #b] ; [[[MP ponens L06] ponens L04] conclude [#h imply #b]] end quote , tacstate0 , c ) end define

define unitac of MP' as \ u . unitac-lemma ( u ) end define

define statement of MP' as Prop infer All #h : All #a : All #b : [[#h imply [#a imply #b]] infer [[#h imply #a] infer [#h imply #b]]] end define

Gen1

Index 91 of page Peano

lgcdef lgcname of Gen1 as "Gen1" enddef

lgcdef lgccharge of Gen1 as "0" enddef

define proof of Gen1 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #a : Line L03 : Condition >> \ c . [quote #x end quote objectavoid ( c ) quote #h end quote] ; Line L04 : Premise >> #h imply #a ; Line L05 : Gen ponens L04 >> f.allfunc \ #x . [#h imply #a] ; Line L06 : A5 probans L03 >> [f.allfunc \ #x . [#h imply #a]] imply [#h imply f.allfunc \ #x . #a] ; [[[MP ponens L06] ponens L05] conclude [#h imply f.allfunc \ #x . #a]] end quote , tacstate0 , c ) end define

define unitac of Gen1 as \ u . unitac-lemma ( u ) end define

define statement of Gen1 as FOL infer All #h : All #x : All #a : [[\ c . [quote #x end quote objectavoid ( c ) quote #h end quote]] endorse [[#h imply #a] infer [#h imply f.allfunc \ #x . #a]]] end define

Gen2

Index 92 of page Peano

lgcdef lgcname of Gen2 as "Gen2" enddef

lgcdef lgccharge of Gen2 as "0" enddef

define proof of Gen2 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #y : All #a : Line L03 : Condition >> \ c . [quote #x end quote objectavoid ( c ) quote #h end quote] ; Line L04 : Condition >> \ c . [quote #y end quote objectavoid ( c ) quote #h end quote] ; Line L05 : Premise >> #h imply #a ; Line L06 : [Gen1 probans L04] ponens L05 >> #h imply f.allfunc \ #y . #a ; [[[Gen1 probans L03] ponens L06] conclude [#h imply f.allfunc \ #x . f.allfunc \ #y . #a]] end quote , tacstate0 , c ) end define

define unitac of Gen2 as \ u . unitac-lemma ( u ) end define

define statement of Gen2 as FOL infer All #h : All #x : All #y : All #a : [[\ c . [quote #x end quote objectavoid ( c ) quote #h end quote]] endorse [[\ c . [quote #y end quote objectavoid ( c ) quote #h end quote]] endorse [[#h imply #a] infer [#h imply f.allfunc \ #x . f.allfunc \ #y . #a]]]] end define

Gen3

Index 93 of page Peano

lgcdef lgcname of Gen3 as "Gen3" enddef

lgcdef lgccharge of Gen3 as "0" enddef

define proof of Gen3 as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; All #h : All #x : All #y : All #z : All #a : Line L03 : Condition >> \ c . [quote #x end quote objectavoid ( c ) quote #h end quote] ; Line L04 : Condition >> \ c . [quote #y end quote objectavoid ( c ) quote #h end quote] ; Line L05 : Condition >> \ c . [quote #z end quote objectavoid ( c ) quote #h end quote] ; Line L06 : Premise >> #h imply #a ; Line L07 : [[Gen2 probans L04] probans L05] ponens L06 >> #h imply f.allfunc \ #y . f.allfunc \ #z . #a ; [[[Gen1 probans L03] ponens L07] conclude [#h imply f.allfunc \ #x . f.allfunc \ #y . f.allfunc \ #z . #a]] end quote , tacstate0 , c ) end define

define unitac of Gen3 as \ u . unitac-lemma ( u ) end define

define statement of Gen3 as FOL infer All #h : All #x : All #y : All #z : All #a : [[\ c . [quote #x end quote objectavoid ( c ) quote #h end quote]] endorse [[\ c . [quote #y end quote objectavoid ( c ) quote #h end quote]] endorse [[\ c . [quote #z end quote objectavoid ( c ) quote #h end quote]] endorse [[#h imply #a] infer [#h imply f.allfunc \ #x . f.allfunc \ #y . f.allfunc \ #z . #a]]]]] end define

Induction

Index 94 of page Peano

lgcdef lgcname of Induction as "Induction" enddef

lgcdef lgccharge of Induction as "0" enddef

define proof of Induction as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; All #x : All #h : All #a : All #z : All #i : Line L03 : Condition >> \ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c ) ; Line L04 : Condition >> \ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c ) ; Line L05 : Condition >> \ c . [quote #x end quote objectavoid ( c ) quote #h end quote] ; Line L06 : Premise >> #h imply #z ; Line L07 : Premise >> #h imply [#a imply #i] ; Line L08 : [Gen1 probans L05] ponens L07 >> #h imply f.allfunc \ #x . [#a imply #i] ; Line L09 : [S9 probans L03] probans L04 >> #z imply [[f.allfunc \ #x . [#a imply #i]] imply #a] ; Line L10 : A1' ponens L09 >> #h imply [#z imply [[f.allfunc \ #x . [#a imply #i]] imply #a]] ; Line L11 : [A2' ponens L10] ponens L06 >> #h imply [[f.allfunc \ #x . [#a imply #i]] imply #a] ; [[[A2' ponens L11] ponens L08] conclude [#h imply #a]] end quote , tacstate0 , c ) end define

define unitac of Induction as \ u . unitac-lemma ( u ) end define

define statement of Induction as PA infer All #x : All #h : All #a : All #z : All #i : [[\ c . sub0 ( quote #z end quote , quote #a end quote , quote #x end quote , quote 0 end quote , c )] endorse [[\ c . sub0 ( quote #i end quote , quote #a end quote , quote #x end quote , quote #x suc end quote , c )] endorse [[\ c . [quote #x end quote objectavoid ( c ) quote #h end quote]] endorse [[#h imply #z] infer [[#h imply [#a imply #i]] infer [#h imply #a]]]]]] end define

hook-hyp

Index 95 of page Peano

lgcdef lgcname of hook-hyp as "hook-hyp" enddef

define value of hook-hyp as norm "hyp" end define

lgcdef lgccharge of hook-hyp as "0" enddef

tactic-Prop ( " )

Index 96 of page Peano

lgcdef lgcname of tactic-Prop ( lgcvar ) as "tactic-Prop ( ""! )" enddef

define value of tactic-Prop ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [x IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [y IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET make-root ( t , quote x unquote infer [[Prop Rule conclude Prop] ;; tactic-ded ( true , y unquote )] end quote ) :: [x :: [[make-root ( t , quote [Prop Rule conclude Prop] ;; tactic-ded ( true , y unquote ) end quote ) :: [[make-root ( t , quote Prop Rule conclude Prop end quote ) :: [[make-root ( t , quote Prop Rule end quote ) :: [[make-root ( t , quote Prop end quote ) :: true] :: true]] :: [[make-root ( t , quote Prop end quote ) :: true] :: true]]] :: [[make-root ( t , quote tactic-ded ( true , y unquote ) end quote ) :: [[make-root ( t , quote true end quote ) :: true] :: [y :: true]]] :: true]]] :: true]] BE [asterisk IN LET asterisk BE [t IN taceval ( t , s , c )]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-Prop ( lgcvar ) as "0" enddef

tactic-FOL ( " )

Index 97 of page Peano

lgcdef lgcname of tactic-FOL ( lgcvar ) as "tactic-FOL ( ""! )" enddef

define value of tactic-FOL ( u ) as norm [u is val : LET u BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk BE [t IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [s IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [c IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET t BE [asterisk IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET asterisk prime head BE [asterisk IN LET asterisk prime tail BE [asterisk prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET asterisk BE [x IN LET asterisk prime prime head BE [asterisk IN LET asterisk prime prime tail BE [asterisk prime prime IN LET [if asterisk atom then asterisk else [asterisk head]] :: [[if asterisk atom then asterisk else [asterisk tail]] :: true] BE [asterisk prime prime prime IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET asterisk BE [y IN LET asterisk prime prime prime head BE [asterisk IN LET asterisk prime prime prime tail BE [asterisk prime prime prime IN LET make-root ( t , quote x unquote infer [[Prop Rule conclude Prop] ;; [[FOL Rule conclude FOL] ;; tactic-ded ( true , y unquote )]] end quote ) :: [x :: [[make-root ( t , quote [Prop Rule conclude Prop] ;; [[FOL Rule conclude FOL] ;; tactic-ded ( true , y unquote )] end quote ) :: [[make-root ( t , quote Prop Rule conclude Prop end quote ) :: [[make-root ( t , quote Prop Rule end quote ) :: [[make-root ( t , quote Prop end quote ) :: true] :: true]] :: [[make-root ( t , quote Prop end quote ) :: true] :: true]]] :: [[make-root ( t , quote [FOL Rule conclude FOL] ;; tactic-ded ( true , y unquote ) end quote ) :: [[make-root ( t , quote FOL Rule conclude FOL end quote ) :: [[make-root ( t , quote FOL Rule end quote ) :: [[make-root ( t , quote FOL end quote ) :: true] :: true]] :: [[make-root ( t , quote FOL end quote ) :: true] :: true]]] :: [[make-root ( t , quote tactic-ded ( true , y unquote ) end quote ) :: [[make-root ( t , quote true end quote ) :: true] :: [y :: true]]] :: true]]] :: true]]] :: true]] BE [asterisk IN LET asterisk BE [t IN LET taceval ( t , s , c ) BE [asterisk IN LET asterisk BE [r IN r]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]] end define

lgcdef lgccharge of tactic-FOL ( lgcvar ) as "0" enddef

lemma-x

Index 98 of page Peano

lgcdef lgcname of lemma-x as "lemma-x" enddef

lgcdef lgccharge of lemma-x as "0" enddef

define proof of lemma-x as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; Line L02 : Prop Rule >> Prop ; Line L03 : Hypothesis >> x ; Line L04 : Hypothesis >> y ; [L03 conclude x] end quote , tacstate0 , c ) end define

define unitac of lemma-x as \ u . unitac-lemma ( u ) end define

define statement of lemma-x as FOL infer [x imply [y imply x]] end define

lemma-y

Index 99 of page Peano

lgcdef lgcname of lemma-y as "lemma-y" enddef

lgcdef lgccharge of lemma-y as "0" enddef

define proof of lemma-y as \ p . \ c . taceval ( quote Line L01 : Premise >> FOL ; Line L02 : Prop Rule >> Prop ; Line L03 : Hypothesis >> h ; [lemma-x conclude [x imply [y imply x]]] end quote , tacstate0 , c ) end define

define unitac of lemma-y as \ u . unitac-lemma ( u ) end define

define statement of lemma-y as FOL infer [h imply [x imply [y imply x]]] end define

lemma-z

Index 100 of page Peano

lgcdef lgcname of lemma-z as "lemma-z" enddef

lgcdef lgccharge of lemma-z as "0" enddef

define proof of lemma-z as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; [S5 conclude [[x + 0] = x]] end quote , tacstate0 , c ) end define

define unitac of lemma-z as \ u . unitac-lemma ( u ) end define

define statement of lemma-z as PA infer [h imply [i imply [[x + 0] = x]]] end define

lemma-u

Index 101 of page Peano

lgcdef lgcname of lemma-u as "lemma-u" enddef

lgcdef lgccharge of lemma-u as "0" enddef

define proof of lemma-u as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Deduction ; Line L05 : S5 >> [x + 0] = x ; [[[S1 mp L05] mp L05] conclude [x = x]] end quote , tacstate0 , c ) end define

define unitac of lemma-u as \ u . unitac-lemma ( u ) end define

define statement of lemma-u as PA infer [x = x] end define

lemma-v

Index 102 of page Peano

lgcdef lgcname of lemma-v as "lemma-v" enddef

lgcdef lgccharge of lemma-v as "0" enddef

define proof of lemma-v as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; [[S5 f.at x] conclude [[x + 0] = x]] end quote , tacstate0 , c ) end define

define unitac of lemma-v as \ u . unitac-lemma ( u ) end define

define statement of lemma-v as PA infer [h imply [i imply [[x + 0] = x]]] end define

lemma-w

Index 103 of page Peano

lgcdef lgcname of lemma-w as "lemma-w" enddef

lgcdef lgccharge of lemma-w as "0" enddef

define proof of lemma-w as \ p . \ c . taceval ( quote Line L01 : Premise >> PA ; Line L02 : FOL Rule >> FOL ; Line L03 : Prop Rule >> Prop ; Line L04 : Hypothesis >> h ; Line L05 : Hypothesis >> i ; [S5 f.At conclude [[x + 0] = x]] end quote , tacstate0 , c ) end define

define unitac of lemma-w as \ u . unitac-lemma ( u ) end define

define statement of lemma-w as PA infer [h imply [i imply [[x + 0] = x]]] end define

hyp

Index 104 of page Peano

lgcdef lgcname of hyp as "hyp" enddef

lgcdef lgccharge of hyp as "0" enddef

3.2a

Index 105 of page Peano

lgcdef lgcname of 3.2a as "3.2a" enddef

lgcdef lgccharge of 3.2a as "0" enddef

define proof of 3.2a as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> [x + 0] = x ; Line L02 : [S1 mp L01] mp L01 >> x = x ; [[Gen1 ponens L02] conclude f.allfunc \ x . [x = x]] end quote , c ) end define

define unitac of 3.2a as \ u . unitac-lemma ( u ) end define

define statement of 3.2a as PA infer f.allfunc \ x . [x = x] end define

3.2b

Index 106 of page Peano

lgcdef lgcname of 3.2b as "3.2b" enddef

lgcdef lgccharge of 3.2b as "0" enddef

define proof of 3.2b as \ p . \ c . taceval1 ( quote PA end quote , quote Line L00 : Block >> Begin ; Line L01 : Hypothesis >> x = y ; Line L02 : 3.2a >> x = x ; [[[S1 mp L01] mp L02] conclude [y = x]] line L04 : Block >> End ; [[Gen2 ponens L04] conclude f.allfunc \ x . f.allfunc \ y . [[x = y] imply [y = x]]] end quote , c ) end define

define unitac of 3.2b as \ u . unitac-lemma ( u ) end define

define statement of 3.2b as PA infer f.allfunc \ x . f.allfunc \ y . [[x = y] imply [y = x]] end define

3.2c

Index 107 of page Peano

lgcdef lgcname of 3.2c as "3.2c" enddef

lgcdef lgccharge of 3.2c as "0" enddef

define proof of 3.2c as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : Block >> Begin ; Line L02 : Hypothesis >> x = y ; Line L03 : Hypothesis >> y = z ; Line L04 : 3.2b mp L02 >> y = x ; [[[S1 mp L04] mp L03] conclude [x = z]] line L06 : Block >> End ; [[Gen3 ponens L06] conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = y] imply [[y = z] imply [x = z]]]] end quote , c ) end define

define unitac of 3.2c as \ u . unitac-lemma ( u ) end define

define statement of 3.2c as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = y] imply [[y = z] imply [x = z]]] end define

3.2d

Index 108 of page Peano

lgcdef lgcname of 3.2d as "3.2d" enddef

lgcdef lgccharge of 3.2d as "0" enddef

define proof of 3.2d as \ p . \ c . taceval1 ( quote PA end quote , quote Line L00 : Block >> Begin ; Line L01 : Hypothesis >> x = z ; Line L02 : Hypothesis >> y = z ; Line L03 : 3.2b mp L02 >> z = y ; [[[3.2c mp L01] mp L03] conclude [x = y]] line L05 : Block >> End ; [[Gen3 ponens L05] conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = z] imply [[y = z] imply [x = y]]]] end quote , c ) end define

define unitac of 3.2d as \ u . unitac-lemma ( u ) end define

define statement of 3.2d as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = z] imply [[y = z] imply [x = y]]] end define

3.2e

Index 109 of page Peano

lgcdef lgcname of 3.2e as "3.2e" enddef

lgcdef lgccharge of 3.2e as "0" enddef

define proof of 3.2e as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : Block >> Begin ; Line L02 : Hypothesis >> x = y ; Line L03 : S5 >> [x + 0] = x ; Line L04 : [3.2c mp L03] mp L02 >> [x + 0] = y ; Line L05 : S5 >> [y + 0] = y ; [[[3.2d mp L04] mp L05] conclude [[x + 0] = [y + 0]]] line L07 : Block >> End ; Line L08 : Block >> Begin ; Line L09 : Hypothesis >> [x = y] imply [[x + z] = [y + z]] ; Line L10 : Hypothesis >> x = y ; Line L11 : [MP' ponens L09] ponens L10 >> [x + z] = [y + z] ; Line L12 : S2 mp L11 >> [x + z] suc = [[y + z] suc] ; Line L13 : S6 >> [x + [z suc]] = [[x + z] suc] ; Line L14 : [3.2c mp L13] mp L12 >> [x + [z suc]] = [[y + z] suc] ; Line L15 : S6 >> [y + [z suc]] = [[y + z] suc] ; [[[3.2d mp L14] mp L15] conclude [[x + [z suc]] = [y + [z suc]]]] line L17 : Block >> End ; Line L18 : [[Induction at z] ponens L07] ponens L17 >> [x = y] imply [[x + z] = [y + z]] ; [[Gen3 ponens L18] conclude f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = y] imply [[x + z] = [y + z]]]] end quote , c ) end define

define unitac of 3.2e as \ u . unitac-lemma ( u ) end define

define statement of 3.2e as PA infer f.allfunc \ x . f.allfunc \ y . f.allfunc \ z . [[x = y] imply [[x + z] = [y + z]]] end define

3.2f

Index 110 of page Peano

lgcdef lgcname of 3.2f as "3.2f" enddef

lgcdef lgccharge of 3.2f as "0" enddef

define proof of 3.2f as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> [0 + 0] = 0 ; Line L02 : 3.2b mp L01 >> 0 = [0 + 0] ; Line L03 : Block >> Begin ; Line L04 : Hypothesis >> x = [0 + x] ; Line L05 : S2 mp L04 >> x suc = [[0 + x] suc] ; Line L06 : S6 >> [0 + [x suc]] = [[0 + x] suc] ; [[[3.2d mp L05] mp L06] conclude [x suc = [0 + [x suc]]]] line L08 : Block >> End ; Line L09 : [[Induction at x] ponens L02] ponens L08 >> x = [0 + x] ; [[Gen1 ponens L09] conclude f.allfunc \ x . [x = [0 + x]]] end quote , c ) end define

define unitac of 3.2f as \ u . unitac-lemma ( u ) end define

define statement of 3.2f as PA infer f.allfunc \ x . [x = [0 + x]] end define

3.2g

Index 111 of page Peano

lgcdef lgcname of 3.2g as "3.2g" enddef

lgcdef lgccharge of 3.2g as "0" enddef

define proof of 3.2g as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> [x suc + 0] = [x suc] ; Line L02 : S5 >> [x + 0] = x ; Line L03 : S2 mp L02 >> [x + 0] suc = [x suc] ; Line L04 : [3.2d mp L01] mp L03 >> [x suc + 0] = [[x + 0] suc] ; Line L05 : Block >> Begin ; Line L06 : Hypothesis >> [x suc + y] = [[x + y] suc] ; Line L07 : S2 mp L06 >> [x suc + y] suc = [[x + y] suc suc] ; Line L08 : S6 >> [x suc + [y suc]] = [[x suc + y] suc] ; Line L09 : [3.2c mp L08] mp L07 >> [x suc + [y suc]] = [[x + y] suc suc] ; Line L10 : S6 >> [x + [y suc]] = [[x + y] suc] ; Line L11 : S2 mp L10 >> [x + [y suc]] suc = [[x + y] suc suc] ; [[[3.2d mp L09] mp L11] conclude [[x suc + [y suc]] = [[x + [y suc]] suc]]] line L13 : Block >> End ; Line L14 : [[Induction at y] ponens L04] ponens L13 >> [x suc + y] = [[x + y] suc] ; [[Gen2 ponens L14] conclude f.allfunc \ x . f.allfunc \ y . [[x suc + y] = [[x + y] suc]]] end quote , c ) end define

define unitac of 3.2g as \ u . unitac-lemma ( u ) end define

define statement of 3.2g as PA infer f.allfunc \ x . f.allfunc \ y . [[x suc + y] = [[x + y] suc]] end define

3.2h

Index 112 of page Peano

lgcdef lgcname of 3.2h as "3.2h" enddef

lgcdef lgccharge of 3.2h as "0" enddef

define proof of 3.2h as \ p . \ c . taceval1 ( quote PA end quote , quote Line L01 : S5 >> [x + 0] = x ; Line L02 : 3.2f >> x = [0 + x] ; Line L03 : [3.2c mp L01] mp L02 >> [x + 0] = [0 + x] ; Line L04 : Block >> Begin ; Line L05 : Hypothesis >> [x + y] = [y + x] ; Line L06 : S2 mp L05 >> [x + y] suc = [[y + x] suc] ; Line L07 : S6 >> [x + [y suc]] = [[x + y] suc] ; Line L08 : [3.2c mp L07] mp L06 >> [x + [y suc]] = [[y + x] suc] ; Line L09 : 3.2g >> [y suc + x] = [[y + x] suc] ; [[[3.2d mp L08] mp L09] conclude [[x + [y suc]] = [y suc + x]]] line L11 : Block >> End ; Line L12 : [[Induction at y] ponens L03] ponens L11 >> [x + y] = [y + x] ; [[Gen2 ponens L12] conclude f.allfunc \ x . f.allfunc \ y . [[x + y] = [y + x]]] end quote , c ) end define

define unitac of 3.2h as \ u . unitac-lemma ( u ) end define

define statement of 3.2h as PA infer f.allfunc \ x . f.allfunc \ y . [[x + y] = [y + x]] end define

" First

Index 113 of page Peano

lgcdef lgcname of lgcvar First as ""-""! First" enddef

Define tex show of x First as "".[ x ]" {}^{\underline{1}}" end define

define value of x First as norm [x is val : [x first first]] end define

lgcdef lgccharge of lgcvar First as "4" enddef

" Second

Index 114 of page Peano

lgcdef lgcname of lgcvar Second as ""-""! Second" enddef

Define tex show of x Second as "".[ x ]" {}^{\underline{2}}" end define

define value of x Second as norm [x is val : [x first second]] end define

lgcdef lgccharge of lgcvar Second as "4" enddef

" suc

Index 115 of page Peano

lgcdef lgcname of lgcvar suc as ""-""! suc" enddef

Define tex show of x suc as "".[ x ]" {}'" end define

define value of x suc as norm [x is val : [x + 1]] end define

lgcdef lgccharge of lgcvar suc as "4" enddef

not "

Index 116 of page Peano

lgcdef lgcname of not lgcvar as "not ""!" enddef

Define tex show of not x as " \neg "[ x ]"". end define

lgcdef lgccharge of not lgcvar as "22" enddef

define math of not x as x imply ff end define

" and "

Index 117 of page Peano

lgcdef lgcname of lgcvar and lgcvar as ""-""! and ""!" enddef

Define tex show of x and y as "".[ x ][" \wedge "[ y ]"".] end define

lgcdef lgccharge of lgcvar and lgcvar as "24" enddef

define math of x and y as not [x imply not y] end define

" or "

Index 118 of page Peano

lgcdef lgcname of lgcvar or lgcvar as ""-""! or ""!" enddef

Define tex show of x or y as "".[ x ][" \vee "[ y ]"".] end define

lgcdef lgccharge of lgcvar or lgcvar as "26" enddef

define math of x or y as [not x] imply y end define

all " : "

Index 119 of page Peano

lgcdef lgcname of all lgcvar : lgcvar as "all ""! : ""!" enddef

Define tex show of all x : y as " \forall "[ x ][" \colon \linebreak[0] "[ y ]"".] end define

define macro of all u : v as \ x . expand-all ( x ) end define

lgcdef lgccharge of all lgcvar : lgcvar as "28" enddef

f.allfunc "

Index 120 of page Peano

lgcdef lgcname of f.allfunc lgcvar as "f.allfunc ""!" enddef

lgcdef lgccharge of f.allfunc lgcvar as "28" enddef

define math of f.allfunc x as "all" end define

exist " : "

Index 121 of page Peano

lgcdef lgcname of exist lgcvar : lgcvar as "exist ""! : ""!" enddef

Define tex show of exist x : y as " \exists "[ x ][" \colon \linebreak[0] "[ y ]"".] end define

lgcdef lgccharge of exist lgcvar : lgcvar as "28" enddef

f.existfunc "

Index 122 of page Peano

lgcdef lgcname of f.existfunc lgcvar as "f.existfunc ""!" enddef

lgcdef lgccharge of f.existfunc lgcvar as "28" enddef

" imply "

Index 123 of page Peano

lgcdef lgcname of lgcvar imply lgcvar as ""-""! imply ""!" enddef

Define tex show of x imply y as "".[ x ][" \Rightarrow "[ y ]"".] end define

lgcdef lgccharge of lgcvar imply lgcvar as "29" enddef

define math of x imply y as "imply" end define

" when "

Index 124 of page Peano

lgcdef lgcname of lgcvar when lgcvar as ""-""! when ""!" enddef

Define tex show of x when y as "".[ x ][" \Leftarrow "[ y ]"".] end define

lgcdef lgccharge of lgcvar when lgcvar as "29" enddef

define math of x when y as y imply x end define

" iff "

Index 125 of page Peano

lgcdef lgcname of lgcvar iff lgcvar as ""-""! iff ""!" enddef

Define tex show of x iff y as "".[ x ][" \Leftrightarrow "[ y ]"".] end define

lgcdef lgccharge of lgcvar iff lgcvar as "29" enddef

define math of x iff y as [x imply y] and [y imply x] end define

" avoid "

Index 126 of page Peano

lgcdef lgcname of lgcvar avoid lgcvar as ""-""! avoid ""!" enddef

Define tex show of x avoid y as "".[ x ][" \# "[ y ]"".] end define

define macro of x avoid y as \ x . expand ( quote macro define x avoid y as \ c . [quote x end quote objectavoid ( c ) quote y end quote] end define end quote , x ) end define

lgcdef lgccharge of lgcvar avoid lgcvar as "36" enddef

" f.At

Index 127 of page Peano

lgcdef lgcname of lgcvar f.At as ""-""! f.At" enddef

Define tex show of x f.At as "".[ x ]" {}^{\underline{@}}" end define

lgcdef lgccharge of lgcvar f.At as "38" enddef

define unitac of x f.At as \ u . f.unitac-At ( u ) end define

" Mp

Index 128 of page Peano

lgcdef lgcname of lgcvar Mp as ""-""! Mp" enddef

Define tex show of x Mp as "".[ x ]" {}^{\unrhd}" end define

lgcdef lgccharge of lgcvar Mp as "38" enddef

define unitac of x Mp as \ u . f.unitac-Ponens ( u ) end define

" mp "

Index 129 of page Peano

lgcdef lgcname of lgcvar mp lgcvar as ""-""! mp ""!" enddef

Define tex show of x mp y as "".[ x ][" \unrhd "[ y ]"".] end define

lgcdef lgccharge of lgcvar mp lgcvar as "40" enddef

define unitac of x mp y as \ u . f.unitac-ponens ( u ) end define

" f.at "

Index 130 of page Peano

lgcdef lgcname of lgcvar f.at lgcvar as ""-""! f.at ""!" enddef

Define tex show of x f.at y as "".[ x ][" \mathrel{\underline{@}} "[ y ]"".] end define

lgcdef lgccharge of lgcvar f.at lgcvar as "40" enddef

define unitac of x f.at y as \ u . f.unitac-at ( u ) end define

line " : Hypothesis >> " ; "

Index 131 of page Peano

Define tex use of line x : Hypothesis >> z ; u as " \newline% \makebox[0.1\textwidth]{}% \parbox[b]{0.4\textwidth}{\raggedright% \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]["{:}$}}% $Hypothesis {} \gg {}$}% \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% $"[ z ]["$\hfill \makebox[0mm][l]{\quad ;}} "[ u ]"".]] end define

lgcdef lgcname of line lgcvar : Hypothesis >> lgcvar ; lgcvar as "line ""! : Hypothesis >> ""! ; ""!" enddef

Define tex show of line x : Hypothesis >> z ; u as " L "[ x ][" \colon Hypothesis \gg "[ z ][" ; "[ u ]"".]] end define

define macro of line l : Hypothesis >> x ; n as \ x . expand ( quote macro define line l : Hypothesis >> x ; n as Line l : Hypothesis >> x ; n end define end quote , x ) end define

lgcdef lgccharge of line lgcvar : Hypothesis >> lgcvar ; lgcvar as "45" enddef

define locate of line asterisk : Hypothesis >> asterisk ; asterisk as "line" :: 1 end define

Line " : Hypothesis >> " ; "

Index 132 of page Peano

lgcdef lgcname of Line lgcvar : Hypothesis >> lgcvar ; lgcvar as "Line ""! : Hypothesis >> ""! ; ""!" enddef

lgcdef lgccharge of Line lgcvar : Hypothesis >> lgcvar ; lgcvar as "45" enddef

define tactic of Line l : Hypothesis >> x ; n as \ u . tactic-hyp ( u ) end define

line " : Deduction ; "

Index 133 of page Peano

Define tex use of line x : Deduction ; u as " \newline% \makebox[0.1\textwidth]{}% \parbox[b]{0.4\textwidth}{\raggedright% \makebox[0mm][r]{\makebox[0.1\textwidth][l]{$"[ x ]["{:}$}}% $Deduction$}% \parbox[t]{0.4\textwidth}{\raggedright\setlength{\leftskip}{\indentation}% {}\hfill \makebox[0mm][l]{\quad ;}} "[ u ]"".] end define

lgcdef lgcname of line lgcvar : Deduction ; lgcvar as "line ""! : Deduction ; ""!" enddef

Define tex show of line x : Deduction ; u as " L "[ x ][" \colon Deduction ; "[ u ]"".] end define

define macro of line l : Deduction ; n as \ x . expand ( quote macro define line l : Deduction ; n as Line l : Deduction ; n end define end quote , x ) end define

lgcdef lgccharge of line lgcvar : Deduction ; lgcvar as "45" enddef

define locate of line asterisk : Deduction ; asterisk as "line" :: 1 end define

Line " : Deduction ; "

Index 134 of page Peano

lgcdef lgcname of Line lgcvar : Deduction ; lgcvar as "Line ""! : Deduction ; ""!" enddef

lgcdef lgccharge of Line lgcvar : Deduction ; lgcvar as "45" enddef

define tactic of Line l : Deduction ; n as \ u . tactic-dummyhyp ( u ) end define

Charges

0

check
base
Peano
expand-all ( " )
expand-all1 ( " , " , " )
is-meta-term ( " , " )
unitac-hyp
unitac-lemma-hyp ( " )
unitac-rule-hyp ( " )
unitac-conclude-hyp ( " )
tactic-hyp ( " )
tactic-dummyhyp ( " )
tactic-ded ( " , " )
tactic-first-hyp ( " , " , " )
add-first-hyp* ( " , " , " )
add-first-hyp ( " , " , " )
tactic-next-hyp ( " , " , " , " )
add-next-hyp* ( " , " , " )
add-next-hyp ( " , " , " )
f.unitac-adapt ( " , " , " )
f.unitac-adapt-all ( " , " , " , " , " , " , " , " , " )
f.tacfresh ( " )
f.unitac-ponens ( " )
f.unitac-Ponens ( " )
f.unitac-at ( " )
f.unitac-At ( " )
sub ( " , " , " , " )
sub0 ( " , " , " , " , " )
sub1 ( " , " , " , " , " )
sub* ( " , " , " , " , " )
f.subst ( " , " , " )
f.subst* ( " , " , " )
inst ( " , " )
inst0 ( " , " , " )
inst1 ( " , " , " )
inst-strip ( " , " , " )
inst-zip ( " , " )
inst2 ( " , " , " , " , " )
inst2* ( " , " , " , " , " )
inst3 ( " , " , " )
inst3* ( " , " , " )
def ( " , " )
def0 ( " , " , " )
def0* ( " , " , " )
def1 ( " , " , " )
def2 ( " , " , " )
def3 ( " , " , " , " )
def3* ( " , " , " , " )
defcheck
checked-def ( " , " )
defcheck1 ( " )
defcheck2 ( " , " )
valid-def ( " , " , " , " )
valid-def* ( " , " , " , " )
Prop
FOL
PA
MP
Gen
Def
A1
A2
A3
A4
AP4
A5
tt
ff
S1
S2
S3
S4
S5
S6
S7
S8
S9
Mend1.8
A1'
A2'
Mend1.47b
Mend1.47c
Mend1.47d
Mend1.11b
Mend1.48d
Mend1.48e
Lnexthyp
Lcurry
LTruth
LElimHyp
LA4'
LAP4'
MP'
Gen1
Gen2
Gen3
Induction
hook-hyp
tactic-Prop ( " )
tactic-FOL ( " )
lemma-x
lemma-y
lemma-z
lemma-u
lemma-v
lemma-w
hyp
3.2a
3.2b
3.2c
3.2d
3.2e
3.2f
3.2g
3.2h

2

+"

4

"#
" factorial
" First
" Second
" suc

6

" ' "

8

- "

10

" Times "

12

" set+ "
" Plus "

14

PlusTag "

16

" div "

17

" LazyPair "

19

" ,, "

20

" member "
" = "

22

p.not "
Not "
not "

24

" And "
" and "

26

" Or "
" or "

28

all " : "
f.allfunc "
exist " : "
f.existfunc "

29

" p.imply "
" Iff "
" imply "
" when "
" iff "

30

" Select " else " end select

32

metadeclare "
\ " . "

33

norm "

34

" reduce to "

36

" avoid "

38

" Init
" f.At
" Mp

40

" at "
" mp "
" f.at "

41

" infer "

42

All " : "

43

" oplus "

44

" conclude "

45

line " : " >> " ; "
line " : Hypothesis >> " ; "
Line " : Hypothesis >> " ; "
line " : Deduction ; "
Line " : Deduction ; "

47

" ;; "

48

" proves "

49

axiom " : " end axiom

50

" endline

51

dbug ( " ) "
" lgcthen "

52

" linebreak "

54

" & "

56

" \\ "

The Logiweb compiler (lgc) GRD-2009-11-28.UTC:11:17:40.281380