Theorem sucb1 | index | src |

theorem sucb1 (a: nat): $ suc (b1 a) = b0 (suc a) $;
StepHypRefExpression
1 eqtr2
b0 (suc a) = suc (a + suc a) -> suc (a + suc a) = suc (b1 a) -> suc (b1 a) = b0 (suc a)
2 addS1
suc a + suc a = suc (a + suc a)
3 2 conv b0
b0 (suc a) = suc (a + suc a)
4 1, 3 ax_mp
suc (a + suc a) = suc (b1 a) -> suc (b1 a) = b0 (suc a)
5 suceq
a + suc a = b1 a -> suc (a + suc a) = suc (b1 a)
6 addS
a + suc a = suc (a + a)
7 6 conv b0, b1
a + suc a = b1 a
8 5, 7 ax_mp
suc (a + suc a) = suc (b1 a)
9 4, 8 ax_mp
suc (b1 a) = b0 (suc a)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano2, peano5, addeq, add0, addS)