Logiweb extract of multzero

Table of contents

Date of publication
Bibliography
Definitions
Charges

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)
[1] check (014E93CEDBCA44EB611BC0974861950432277A602795E9B4F2BAD8BB0806)
[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

0

check
Peano
base
multzero
3.2l

2

+"

4

"#
" First
" factorial

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 " : "

29

" p.imply "
" imply "
" Iff "

30

" Select " else " end select

32

metadeclare "
\ " . "

33

norm "

34

" reduce to "

36

" avoid "

38

" Init
" f.At

40

" at "
" mp "

41

" infer "

42

All " : "

43

" oplus "

44

" conclude "

45

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

47

" ;; "

48

" proves "

49

axiom " : " end axiom

50

" endline

51

dbug ( " ) "
" lgcthen "

52

" linebreak "

54

" & "

56

" \\ "