## Logiweb extract of multzero

Up
Help
### Table of contents

Date of publication

Bibliography

Definitions

Charges

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)

`[0] multzero (014E20344F3D486370710A10269E83D974EB8E9787EFB994A0BBD8BB0806)`

[1] check (014E93CEDBCA44EB611BC0974861950432277A602795E9B4F2BAD8BB0806)

[2] Peano (0176CD88B275E1404092783C6E442E09C246B342FAA4A9B28DBBD8BB0806)

[3] base (01AB1F51C8C17606A5C0331B5689B4858C796547B9A0A4AEF0BCB2BB0806)

#### 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

#### 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

`" \\ "`

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