diff options
| author | Georg Brandl <georg@python.org> | 2021-01-18 21:24:00 +0100 |
|---|---|---|
| committer | Georg Brandl <georg@python.org> | 2021-01-18 22:08:36 +0100 |
| commit | 2a3d3a7d5b9c60dedf6638d876161d9563faebcf (patch) | |
| tree | 809c0b4a686db98f5954afa1944404cd9652c6b2 /tests/lexers/tnt | |
| parent | f0445be718da83541ea3401aad882f3937147263 (diff) | |
| download | pygments-git-examplefiles.tar.gz | |
Move test_examplefiles to new tests/lexers scheme.examplefiles
Diffstat (limited to 'tests/lexers/tnt')
| -rw-r--r-- | tests/lexers/tnt/example.txt | 1554 |
1 files changed, 1554 insertions, 0 deletions
diff --git a/tests/lexers/tnt/example.txt b/tests/lexers/tnt/example.txt new file mode 100644 index 00000000..0a571369 --- /dev/null +++ b/tests/lexers/tnt/example.txt @@ -0,0 +1,1554 @@ +---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 |