---input---
101 Aa:Ab:(a+Sb)=S(a+b)	axiom 3
102 Ab:(0+Sb)=S(0+b)	specification
103 (0+Sb)=S(0+b)	specification
104 [			push
105	(0+b)=b		premise
106	S(0+b)=Sb	add S
107	(0+Sb)=S(0+b)	carry over line 103
108	(0+Sb)=Sb	transitivity
109 ]			pop
110 <(0+b)=b](0+Sb)=Sb>		fantasy rule
111 Ab:<(0+b)=b](0+Sb)=Sb>	generalization
112 Aa:(a+0)=a		axiom 2
113 (0+0)=0		specification
114 Ab:(0+b)=b		induction (lines 111, 113)
115 (0+a)=a		specification
116 Aa:(0+a)=a		generalization

01 Aa:Ab:(a+Sb)=S(a+b)	axiom 3
02 Ab:(d+Sb)=S(d+b)	specification
03 (d+SSc)=S(d+Sc)	specification
04 Ab:(Sd+Sb)=S(Sd+b)	specification (line 01)
05 (Sd+Sc)=S(Sd+c)	specification
06 S(Sd+c)=(Sd+Sc)	symmetry
07 [			push
08 	Ad:(d+Sc)=(Sd+c)	premise
09	(d+Sc)=(Sd+c)		specification
10	S(d+Sc)=S(Sd+c)		add S
11	(d+SSc)=S(d+Sc) 	carry over 03
12	(d+SSc)=S(Sd+c)		transitivity
13	S(Sd+c)=(Sd+Sc)		carry over 06
14	(d+SSc)=(Sd+Sc)		transitivity
15	Ad:(d+SSc)=(Sd+Sc)	generalization
16 ]			pop
17 <Ad:(d+Sc)=(Sd+c)]Ad:(d+SSc)=(Sd+Sc)>	fantasy rule
18 Ac:<Ad:(d+Sc)=(Sd+c)]Ad:(d+SSc)=(Sd+Sc)>	generalization
19 (d+S0)=S(d+0)	specification (line 02)
20 Aa:(a+0)=a		axiom 1
21 (d+0)=d		specification
22 S(d+0)=Sd		add S
23 (d+S0)=Sd		transitivity (lines 19,22)
24 (Sd+0)=Sd		specification (line 20)
25 Sd=(Sd+0)		symmetry
26 (d+S0)=(Sd+0)	transitivity (lines 23,25)
27 Ad:(d+S0)=(Sd+0)	generalization

28 Ac:Ad:(d+Sc)=(Sd+c)	induction (lines 18,27)
   [S can be slipped back and forth in an addition.]

29 Ab:(c+Sb)=S(c+b)	specification (line 01)
30 (c+Sd)=S(c+d)	specification
31 Ab:(d+Sb)=S(d+b)	specification (line 01)
32 (d+Sc)=S(d+c)	specification
33 S(d+c)=(d+Sc)	symmetry
34 Ad:(d+Sc)=(Sd+c)	specification (line 28)
35 (d+Sc)=(Sd+c)	specification
36 [			push
37	Ac:(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)		carry over 30
41	(c+Sd)=S(d+c)		transitivity
42	S(d+c)=(d+Sc)		carry over 33
43	(c+Sd)=(d+Sc)		transitivity
44	(d+Sc)=(Sd+c)		carry over 35
45	(c+Sd)=(Sd+c)		transitivity
46	Ac:(c+Sd)=(Sd+c)	generalization
47 ]			pop
48 <Ac:(c+d)=(d+c)]Ac:(c+Sd)=(Sd+c)>	fantasy rule
49 Ad:<Ac:(c+d)=(d+c)]Ac:(c+Sd)=(Sd+c)>	generalization
   [If d commutes with every c, then Sd does too.]

50 (c+0)=c		specification (line 20)
51 Aa:(0+a)=a		carry over 116
52 (0+c)=c		specification
53 c=(0+c)		symmetry
54 (c+0)=(0+c)		transitivity (lines 50,53)
55 Ac:(c+0)=(0+c)	generalization
   [0 commutes with every c.]

56 Ad:Ac:(c+d)=(d+c)	induction (lines 49,55)
   [Therefore, every d commmutes with every c.]

---tokens---
'101'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'axiom '      Keyword
'3'           Literal.Number.Integer
'\n'          Text

'102'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'103'         Literal.Number.Integer
' '           Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'104'         Literal.Number.Integer
' '           Text
'['           Keyword
'\t\t\t'      Text
'push'        Keyword
'\n'          Text

'105'         Literal.Number.Integer
'\t'          Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'='           Operator
'b'           Name.Variable
'\t\t'        Text
'premise'     Keyword
'\n'          Text

'106'         Literal.Number.Integer
'\t'          Text
'S'           Literal.Number.Integer
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
'\t'          Text
'add S'       Keyword
'\n'          Text

'107'         Literal.Number.Integer
'\t'          Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'carry over line ' Keyword
'103'         Literal.Number.Integer
'\n'          Text

'108'         Literal.Number.Integer
'\t'          Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
'\t'          Text
'transitivity' Keyword
'\n'          Text

'109'         Literal.Number.Integer
' '           Text
']'           Keyword
'\t\t\t'      Text
'pop'         Keyword
'\n'          Text

'110'         Literal.Number.Integer
' '           Text
'<'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'='           Operator
'b'           Name.Variable
']'           Operator
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
'>'           Punctuation
'\t\t'        Text
'fantasy rule' Keyword
'\n'          Text

'111'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'<'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'='           Operator
'b'           Name.Variable
']'           Operator
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
'>'           Punctuation
'\t'          Text
'generalization' Keyword
'\n'          Text

'112'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'a'           Name.Variable
'\t\t'        Text
'axiom '      Keyword
'2'           Literal.Number.Integer
'\n'          Text

'113'         Literal.Number.Integer
' '           Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'0'           Literal.Number.Integer
'\t\t'        Text
'specification' Keyword
'\n'          Text

'114'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'='           Operator
'b'           Name.Variable
'\t\t'        Text
'induction'   Keyword
' '           Text
'('           Punctuation
'lines '      Text
'111, 113'    Literal.Number.Integer
')'           Punctuation
'\n'          Text

'115'         Literal.Number.Integer
' '           Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'a'           Name.Variable
')'           Punctuation
'='           Operator
'a'           Name.Variable
'\t\t'        Text
'specification' Keyword
'\n'          Text

'116'         Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'a'           Name.Variable
')'           Punctuation
'='           Operator
'a'           Name.Variable
'\t\t'        Text
'generalization' Keyword
'\n\n'        Text

'01'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'axiom '      Keyword
'3'           Literal.Number.Integer
'\n'          Text

'02'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'03'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'04'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'01'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'05'          Literal.Number.Integer
' '           Text
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'06'          Literal.Number.Integer
' '           Text
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'symmetry'    Keyword
'\n'          Text

'07'          Literal.Number.Integer
' '           Text
'['           Keyword
'\t\t\t'      Text
'push'        Keyword
'\n'          Text

'08'          Literal.Number.Integer
' \t'         Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'premise'     Keyword
'\n'          Text

'09'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'specification' Keyword
'\n'          Text

'10'          Literal.Number.Integer
'\t'          Text
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'add S'       Keyword
'\n'          Text

'11'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
' \t'         Text
'carry over ' Keyword
'03'          Literal.Number.Integer
'\n'          Text

'12'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
'\n'          Text

'13'          Literal.Number.Integer
'\t'          Text
'S'           Literal.Number.Integer
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'carry over ' Keyword
'06'          Literal.Number.Integer
'\n'          Text

'14'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
'\n'          Text

'15'          Literal.Number.Integer
'\t'          Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'generalization' Keyword
'\n'          Text

'16'          Literal.Number.Integer
' '           Text
']'           Keyword
'\t\t\t'      Text
'pop'         Keyword
'\n'          Text

'17'          Literal.Number.Integer
' '           Text
'<'           Punctuation
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
']'           Operator
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'>'           Punctuation
'\t'          Text
'fantasy rule' Keyword
'\n'          Text

'18'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'<'           Punctuation
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
']'           Operator
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'SS'          Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'>'           Punctuation
'\t'          Text
'generalization' Keyword
'\n'          Text

'19'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'\t'          Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'02'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'20'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'('           Punctuation
'a'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'a'           Name.Variable
'\t\t'        Text
'axiom '      Keyword
'1'           Literal.Number.Integer
'\n'          Text

'21'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'd'           Name.Variable
'\t\t'        Text
'specification' Keyword
'\n'          Text

'22'          Literal.Number.Integer
' '           Text
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
'\t\t'        Text
'add S'       Keyword
'\n'          Text

'23'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
'\t\t'        Text
'transitivity' Keyword
' '           Text
'('           Punctuation
'lines '      Text
'19,22'       Literal.Number.Integer
')'           Punctuation
'\n'          Text

'24'          Literal.Number.Integer
' '           Text
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
'\t\t'        Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'20'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'25'          Literal.Number.Integer
' '           Text
'S'           Literal.Number.Integer
'd'           Name.Variable
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'\t\t'        Text
'symmetry'    Keyword
'\n'          Text

'26'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'\t'          Text
'transitivity' Keyword
' '           Text
'('           Punctuation
'lines '      Text
'23,25'       Literal.Number.Integer
')'           Punctuation
'\n'          Text

'27'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'\t'          Text
'generalization' Keyword
'\n\n'        Text

'28'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'induction'   Keyword
' '           Text
'('           Punctuation
'lines '      Text
'18,27'       Literal.Number.Integer
')'           Punctuation
'\n   '       Text
'[S can be slipped back and forth in an addition.]' Comment
'\n\n'        Text

'29'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'01'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'30'          Literal.Number.Integer
' '           Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'31'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'b'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'b'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'b'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'01'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'32'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'33'          Literal.Number.Integer
' '           Text
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'symmetry'    Keyword
'\n'          Text

'34'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'28'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'35'          Literal.Number.Integer
' '           Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'specification' Keyword
'\n'          Text

'36'          Literal.Number.Integer
' '           Text
'['           Keyword
'\t\t\t'      Text
'push'        Keyword
'\n'          Text

'37'          Literal.Number.Integer
'\t'          Text
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'premise'     Keyword
'\n'          Text

'38'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'specification' Keyword
'\n'          Text

'39'          Literal.Number.Integer
'\t'          Text
'S'           Literal.Number.Integer
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'add S'       Keyword
'\n'          Text

'40'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'\t\t'        Text
'carry over ' Keyword
'30'          Literal.Number.Integer
'\n'          Text

'41'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
'\n'          Text

'42'          Literal.Number.Integer
'\t'          Text
'S'           Literal.Number.Integer
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'carry over ' Keyword
'33'          Literal.Number.Integer
'\n'          Text

'43'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
'\n'          Text

'44'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'c'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'carry over ' Keyword
'35'          Literal.Number.Integer
'\n'          Text

'45'          Literal.Number.Integer
'\t'          Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
'\n'          Text

'46'          Literal.Number.Integer
'\t'          Text
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'generalization' Keyword
'\n'          Text

'47'          Literal.Number.Integer
' '           Text
']'           Keyword
'\t\t\t'      Text
'pop'         Keyword
'\n'          Text

'48'          Literal.Number.Integer
' '           Text
'<'           Punctuation
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
']'           Operator
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'>'           Punctuation
'\t'          Text
'fantasy rule' Keyword
'\n'          Text

'49'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'<'           Punctuation
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
']'           Operator
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'S'           Literal.Number.Integer
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'S'           Literal.Number.Integer
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'>'           Punctuation
'\t'          Text
'generalization' Keyword
'\n   '       Text
'[If d commutes with every c, then Sd does too.]' Comment
'\n\n'        Text

'50'          Literal.Number.Integer
' '           Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'c'           Name.Variable
'\t\t'        Text
'specification' Keyword
' '           Text
'('           Punctuation
'line '       Text
'20'          Literal.Number.Integer
')'           Punctuation
'\n'          Text

'51'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'a'           Name.Variable
':'           Punctuation
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'a'           Name.Variable
')'           Punctuation
'='           Operator
'a'           Name.Variable
'\t\t'        Text
'carry over ' Keyword
'116'         Literal.Number.Integer
'\n'          Text

'52'          Literal.Number.Integer
' '           Text
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'='           Operator
'c'           Name.Variable
'\t\t'        Text
'specification' Keyword
'\n'          Text

'53'          Literal.Number.Integer
' '           Text
'c'           Name.Variable
'='           Operator
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'symmetry'    Keyword
'\n'          Text

'54'          Literal.Number.Integer
' '           Text
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t\t'        Text
'transitivity' Keyword
' '           Text
'('           Punctuation
'lines '      Text
'50,53'       Literal.Number.Integer
')'           Punctuation
'\n'          Text

'55'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'0'           Literal.Number.Integer
')'           Punctuation
'='           Operator
'('           Punctuation
'0'           Literal.Number.Integer
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'generalization' Keyword
'\n   '       Text
'[0 commutes with every c.]' Comment
'\n\n'        Text

'56'          Literal.Number.Integer
' '           Text
'A'           Keyword.Declaration
'd'           Name.Variable
':'           Punctuation
'A'           Keyword.Declaration
'c'           Name.Variable
':'           Punctuation
'('           Punctuation
'c'           Name.Variable
'+'           Operator
'd'           Name.Variable
')'           Punctuation
'='           Operator
'('           Punctuation
'd'           Name.Variable
'+'           Operator
'c'           Name.Variable
')'           Punctuation
'\t'          Text
'induction'   Keyword
' '           Text
'('           Punctuation
'lines '      Text
'49,55'       Literal.Number.Integer
')'           Punctuation
'\n   '       Text
'[Therefore, every d commmutes with every c.]' Comment
'\n'          Text
