TM: 0 B1R 0 D0L 0 C1R 0 F0R 0 C1L 0 A1L 0 E0L 0 G1L 0 A1L 0 B0R 0 C0R 0 E0R
tape / proofs; generated by unibb prover; 2010-Jul-24 05:55:24
PROOF #1
43. 1 {0}5 {1}2 {0}4 <C {1}2
44. 1 {0}5 {1}2 {0}3 <C {1}3
0. 1F {0}5:F {1}2:F {0}4:F|a <C {1}2:F|b
1. 1F {0}5:F {1}2:F {0}3:T|a - 1 <C {1}3:T|b + 1
XSTEPS: 1 =
STEPS: 1
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a - 1...
linearity OK
minimum a - 1 => 2
2. variable = b + 1...
linearity OK
minimum --
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #2
61. {10}2 {0}2 B> {1}8
64. {10}2 {0}5 B> {1}5
0. {10}2:F {0}2:F|a B> {1}8:F|b
1. {10}2:F {0}3:T|a + 1 F> {1}7:T|b - 1
2. {10}2:F {0}4:T|a + 2 E> {1}6:T|b - 2
3. {10}2:F {0}5:T|a + 3 B> {1}5:T|b - 3
XSTEPS: 3 =
STEPS: 3
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 3...
linearity OK
minimum --
2. variable = b - 3...
linearity OK
minimum b - 3 => 4
CONDITIONS ON NEW EXPONENTS...
proved - normal proof
PROOF #3
80. {10}2 {0}8 1 {0}4 F>
92. {10}2 {0}7 1 {0}7 F>
0. {10}2:F {0}8:F|b 1F {0}4:F|a F>
1. {10}2:F {0}8:F|b 1F {0}5:T|a + 1 C>
2. {10}2:F {0}8:F|b 1F {0}5:T|a + 1 <C 1T
xmod: 1
xvar_min: a + -1 val=2 remaining exponent: 1 part_down=1
xmod taken from proof:
3. {10}2:F {0}8:F|b 1F {0}4:T|a + 0 <C {1}2:T proof used (1)
4. {10}2:F {0}8:F|b 1F {0}1:T <C {1}5:T|a + 1
5. {10}2:F {0}8:F|b 1F <C {1}6:T|a + 2
6. {10}2:F {0}8:F|b <A {1}7:T|a + 3
7. {10}2:F {0}7:T|b - 1 1T B> {1}7:T|a + 3
8. {10}2:F {0}7:T|b - 1 1T0T F> {1}6:T|a + 2
9. {10}2:F {0}7:T|b - 1 1T {0}2:T E> {1}5:T|a + 1
xmod derived from transition: a + -1 / 3
xvar_min: a + -3 val=4 remaining exponent: 1 part_down=3
xmod taken from proof:
10. {10}2:F {0}7:T|b - 1 1T {0}3:T B> {1}4:T|a + 0 proof used (2)
11. {10}2:F {0}7:T|b - 1 1T {0}6:T|a + 2 B> {1}1:T
12. {10}2:F {0}7:T|b - 1 1T {0}7:T|a + 3 F>
XSTEPS: 10 =
STEPS: 16
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 3...
linearity OK
minimum a + -3 => 4
2. variable = b - 1...
linearity OK
minimum b - 1 => 2
CONDITIONS ON NEW EXPONENTS...
a + -1 / 3... OK
proved - normal proof
PROOF #4
157. 1 {0}35 {1}2 {0}4 F>
206. 1 {0}31 {1}2 {0}31 F>
0. 1F {0}35:F|b {1}2:F {0}4:F|a F>
1. 1F {0}35:F|b {1}2:F {0}5:T|a + 1 C>
2. 1F {0}35:F|b {1}2:F {0}5:T|a + 1 <C 1T
xmod: 1
xvar_min: a + -1 val=2 remaining exponent: 1 part_down=1
xmod taken from proof:
3. 1F {0}35:F|b {1}2:F {0}4:T|a + 0 <C {1}2:T proof used (1)
4. 1F {0}35:F|b {1}2:F {0}1:T <C {1}5:T|a + 1
5. 1F {0}35:F|b {1}2:F <C {1}6:T|a + 2
6. 1F {0}35:F|b 1T <A {1}7:T|a + 3
7. 1F {0}35:F|b <D 0T {1}7:T|a + 3
8. 1F {0}34:T|b - 1 <E {0}2:T {1}7:T|a + 3
9. 1F {0}33:T|b - 2 <A 1T {0}2:T {1}7:T|a + 3
10. 1F {0}32:T|b - 3 1T B> 1T {0}2:T {1}7:T|a + 3
11. 1F {0}32:T|b - 3 1T0T F> {0}2:T {1}7:T|a + 3
12. 1F {0}32:T|b - 3 1T {0}2:T C> 0T {1}7:T|a + 3
xmod taken from proof:
13. 1F {0}32:T|b - 3 1T {0}2:T <C {1}8:T|a + 4 proof used (1)
14. 1F {0}32:T|b - 3 1T {0}1:T <C {1}9:T|a + 5
15. 1F {0}32:T|b - 3 1T <C {1}10:T|a + 6
16. 1F {0}32:T|b - 3 <A {1}11:T|a + 7
17. 1F {0}31:T|b - 4 1T B> {1}11:T|a + 7
18. 1F {0}31:T|b - 4 1T0T F> {1}10:T|a + 6
19. 1F {0}31:T|b - 4 1T {0}2:T E> {1}9:T|a + 5
xmod derived from transition: a + 2 / 3
xvar_min: a + 0 val=1 remaining exponent: 2 part_down=3
xmod taken from proof:
20. 1F {0}31:T|b - 4 1T {0}3:T B> {1}8:T|a + 4 proof used (2)
21. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 B> {1}2:T
22. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 F> 1T
23. 1F {0}31:T|b - 4 1T {0}11:T|a + 7 E>
24. 1F {0}31:T|b - 4 1T {0}11:T|a + 7 <A 1T
25. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T B> 1T
26. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T0T F>
27. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T {0}2:T C>
28. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T {0}2:T <C 1T
29. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T0T <C {1}2:T
30. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 1T <C {1}3:T
31. 1F {0}31:T|b - 4 1T {0}10:T|a + 6 <A {1}4:T
32. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 1T B> {1}4:T
33. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 1T0T F> {1}3:T
34. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 1T {0}2:T E> {1}2:T
35. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 1T {0}3:T B> 1T
xmod: 1
xvar_min: a + 4 val=-3 remaining exponent: 1 part_down=1
xmod taken from proof:
xmod original: a + -1 / 3 xmod replaced: 4 + -1 / 3 xmod shrinked: 4 + -1 / 3
36. 1F {0}31:T|b - 4 1T {0}9:T|a + 5 1T {0}4:T F> proof used (3)
37. 1F {0}31:T|b - 4 1T {0}1:T 1T {0}28:T|a + 4 * 3 + 4 F>
38. 1F {0}31:T|b - 4 1T {0}1:T 1T {0}29:T|a + 4 * 3 + 5 C>
39. 1F {0}31:T|b - 4 1T {0}1:T 1T {0}29:T|a + 4 * 3 + 5 <C 1T
xmod: 1
xvar_min: a + 4 * 3 + 3 val=-4 remaining exponent: 1 part_down=1
xmod taken from proof:
40. 1F {0}31:T|b - 4 1T {0}1:T 1T {0}28:T|a + 4 * 3 + 4 <C {1}2:T proof used (1)
41. 1F {0}31:T|b - 4 1T {0}1:T 1T {0}1:T <C {1}29:T|a + 4 * 3 + 5
42. 1F {0}31:T|b - 4 1T {0}1:T 1T <C {1}30:T|a + 4 * 3 + 6
43. 1F {0}31:T|b - 4 1T {0}1:T <A {1}31:T|a + 4 * 3 + 7
44. 1F {0}31:T|b - 4 {1}2:T B> {1}31:T|a + 4 * 3 + 7
45. 1F {0}31:T|b - 4 {1}2:T 0T F> {1}30:T|a + 4 * 3 + 6
46. 1F {0}31:T|b - 4 {1}2:T {0}2:T E> {1}29:T|a + 4 * 3 + 5
xmod derived from transition: a + 4 * 3 + 3 / 3
xvar_min: a + 4 * 3 + 1 val=-4 remaining exponent: 1 part_down=3
xmod taken from proof:
47. 1F {0}31:T|b - 4 {1}2:T {0}3:T B> {1}28:T|a + 4 * 3 + 4 proof used (2)
48. 1F {0}31:T|b - 4 {1}2:T {0}30:T|a + 4 * 3 + 6 B> {1}1:T
49. 1F {0}31:T|b - 4 {1}2:T {0}31:T|a + 4 * 3 + 7 F>
XSTEPS: 43 =
STEPS: 187
# STEPS, HEAD... OK
CONFIGURATION SIMILARITY, LINEAR EXPONENT CHANGE, MINIMUM...
1. variable = a + 4 * 3 + 7...
linearity KO
minimum a + -1 => 2
2. variable = b - 4...
linearity OK
minimum b - 4 => 5
CONDITIONS ON NEW EXPONENTS...
a + 2 / 3... OK
a + 4 * 3 + 3 / 3... OK
proved - normal proof