(26) (d+SO)=(Sd+O)
(27) Vd:(d+SO)=(Sd+O)
(28) Vc:Vd:(d+Sc)=(Sd+c)
transitivity
(lines 23,25)
generalization
induction
(lines 18,27)
[S can be slipped back and forth in an addition.]
(29) Vb:(c+Sb)=S(c+b)
(30) (c+Sd)=S(c+d)
(31) Vb:(d+Sb)=S(d+b)
(32) (d+Sc)=S(d+c)
(33) S(d+c)=(d+Sc)
(34) Vd:(d+Sc)=(Sd+c)
specification
(line 1)
specification
specification
(line 1)
specification
symmetry
specification
(line 28)
(35) (d+Sc)=(Sd+c) specification
(36) [ push
(37) Vc:(c+d)=(d+c) premise
(38) (c+d)=(d+c) specification
(39) S(c+d)=S(d+c) add S
(40) (c+Sd)=S(c+d) carryover 30
(41) (c+Sd)=S(d+c) transitivity
(42) S(d+c)=(d+Sc) carryover 33
(43) (c+Sd)=(d+Sc) transitivity
(44) (d+Sc)=(Sd+c) carryover 35
(45) (c +Sd) =(Sd +c) transitivity
(46) Vc:(c+Sd)=(Sd+c) generalization
(47) ] pop
(48) <Vc:(c+d)=(d+cPVc:(c+Sd)=(Sd+c» fantasy rule
(49) Vd:<Ve:(c+d)=(d+cPVc:(c+Sd)=(Sd+c» generalization
[If d commutes with every c, then Sd does too.]
(50) (c+O)=c
(51) Va:(O+a)=a
(52) (O+c)=c
(53) c=(O+c)
226
specification
(line 20)
previous
theorem
specification
symmetry
Typographical Number Theory