---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 fantasy rule 18 Ac: 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 fantasy rule 49 Ad: 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