Theorem revsnoc | index | src |

theorem revsnoc (a l: nat): $ rev (l |> a) = a : rev l $;
StepHypRefExpression
1 eqtr
rev (l |> a) = rev (a : 0) ++ rev l -> rev (a : 0) ++ rev l = a : rev l -> rev (l |> a) = a : rev l
2 revappend
rev (l ++ a : 0) = rev (a : 0) ++ rev l
3 2 conv snoc
rev (l |> a) = rev (a : 0) ++ rev l
4 1, 3 ax_mp
rev (a : 0) ++ rev l = a : rev l -> rev (l |> a) = a : rev l
5 eqtr
rev (a : 0) ++ rev l = a : 0 ++ rev l -> a : 0 ++ rev l = a : rev l -> rev (a : 0) ++ rev l = a : rev l
6 appendeq1
rev (a : 0) = a : 0 -> rev (a : 0) ++ rev l = a : 0 ++ rev l
7 revsn
rev (a : 0) = a : 0
8 6, 7 ax_mp
rev (a : 0) ++ rev l = a : 0 ++ rev l
9 5, 8 ax_mp
a : 0 ++ rev l = a : rev l -> rev (a : 0) ++ rev l = a : rev l
10 eqtr
a : 0 ++ rev l = a : (0 ++ rev l) -> a : (0 ++ rev l) = a : rev l -> a : 0 ++ rev l = a : rev l
11 appendS
a : 0 ++ rev l = a : (0 ++ rev l)
12 10, 11 ax_mp
a : (0 ++ rev l) = a : rev l -> a : 0 ++ rev l = a : rev l
13 conseq2
0 ++ rev l = rev l -> a : (0 ++ rev l) = a : rev l
14 append0
0 ++ rev l = rev l
15 13, 14 ax_mp
a : (0 ++ rev l) = a : rev l
16 12, 15 ax_mp
a : 0 ++ rev l = a : rev l
17 9, 16 ax_mp
rev (a : 0) ++ rev l = a : rev l
18 4, 17 ax_mp
rev (l |> a) = a : rev l

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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)