equal
deleted
inserted
replaced
13 shows "1 = Suc 0" |
13 shows "1 = Suc 0" |
14 and "2 = Suc 1" |
14 and "2 = Suc 1" |
15 and "3 = Suc 2" |
15 and "3 = Suc 2" |
16 and "4 = Suc 3" |
16 and "4 = Suc 3" |
17 and "5 = Suc 4" |
17 and "5 = Suc 4" |
18 and "6 = Suc 5" by arith+ |
18 and "6 = Suc 5" |
|
19 and "7 = Suc 6" |
|
20 and "8 = Suc 7" |
|
21 and "9 = Suc 8" |
|
22 and "10 = Suc 9" |
|
23 by arith+ |
19 |
24 |
20 text {* |
25 text {* |
21 The {\em Copying} TM, which duplicates its input. |
26 The {\em Copying} TM, which duplicates its input. |
22 *} |
27 *} |
23 |
28 |