Logiweb extract of multzero

Up Help

Date of publication

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

Bibliography

[0] multzero (014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806)
[2] Peano (0176CD88B275E1404092783C6E442E09C246B342FAA4A9B28DBBD8BB0806)
[3] base (01AB1F51C8C17606A5C0331B5689B4858C796547B9A0A4AEF0BCB2BB0806)

Definitions

multzero

Index 0 of page multzero

lgcdef lgcname of multzero as "multzero" enddef

lgcdef lgccharge of multzero as "0" enddef

3.2l

Index 1 of page multzero

lgcdef lgcname of 3.2l as "3.2l" enddef

Define tex show of 3.2l as " \mathbf{3.2l}" end define

lgcdef lgccharge of 3.2l as "0" enddef

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

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

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

Charges

check
Peano
base
multzero
3.2l

+"

"#
" First
" factorial

" ' "

- "

" Times "

" set+ "
" Plus "

PlusTag "

" div "

" LazyPair "

" ,, "

" member "
" = "

p.not "
not "
Not "

" and "
" And "

" or "
" Or "

all " : "

" p.imply "
" imply "
" Iff "

30

" Select " else " end select

\ " . "

norm "

" reduce to "

" avoid "

" Init
" f.At

" at "
" mp "

" infer "

All " : "

" oplus "

" conclude "

45

line " : " >> " ; "
line " : Hypothesis >> " ; "

" ;; "

" proves "

49

axiom " : " end axiom

" endline

dbug ( " ) "
" lgcthen "

" linebreak "

" & "

56

" \\ "

The Logiweb compiler (lgc) GRD-2009-11-28.UTC:11:18:19.637871