'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