1470 lines
37 KiB
Text
Generated
1470 lines
37 KiB
Text
Generated
'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
|