Theorem revlen ≪ | index | src | ≫ 

theorem revlen (l: nat): $ len (rev l) = len l $;
StepHypRefExpression
1 id 
_1 = l -> _1 = l
2 1 reveqd 
_1 = l -> rev _1 = rev l
3 2 leneqd 
_1 = l -> len (rev _1) = len (rev l)
4 1 leneqd 
_1 = l -> len _1 = len l
5 3, 4 eqeqd 
_1 = l -> (len (rev _1) = len _1 <-> len (rev l) = len l)
6 id 
_1 = 0 -> _1 = 0
7 6 reveqd 
_1 = 0 -> rev _1 = rev 0
8 7 leneqd 
_1 = 0 -> len (rev _1) = len (rev 0)
9 6 leneqd 
_1 = 0 -> len _1 = len 0
10 8, 9 eqeqd 
_1 = 0 -> (len (rev _1) = len _1 <-> len (rev 0) = len 0)
11 id 
_1 = a2 -> _1 = a2
12 11 reveqd 
_1 = a2 -> rev _1 = rev a2
13 12 leneqd 
_1 = a2 -> len (rev _1) = len (rev a2)
14 11 leneqd 
_1 = a2 -> len _1 = len a2
15 13, 14 eqeqd 
_1 = a2 -> (len (rev _1) = len _1 <-> len (rev a2) = len a2)
16 id 
_1 = a1 : a2 -> _1 = a1 : a2
17 16 reveqd 
_1 = a1 : a2 -> rev _1 = rev (a1 : a2)
18 17 leneqd 
_1 = a1 : a2 -> len (rev _1) = len (rev (a1 : a2))
19 16 leneqd 
_1 = a1 : a2 -> len _1 = len (a1 : a2)
20 18, 19 eqeqd 
_1 = a1 : a2 -> (len (rev _1) = len _1 <-> len (rev (a1 : a2)) = len (a1 : a2))
21 leneq 
rev 0 = 0 -> len (rev 0) = len 0
22 rev0 
rev 0 = 0
23 21, 22 ax_mp 
len (rev 0) = len 0
24 leneq 
rev (a1 : a2) = rev a2 |> a1 -> len (rev (a1 : a2)) = len (rev a2 |> a1)
25 revS 
rev (a1 : a2) = rev a2 |> a1
26 24, 25 ax_mp 
len (rev (a1 : a2)) = len (rev a2 |> a1)
27 snoclen 
len (rev a2 |> a1) = suc (len (rev a2))
28 lenS 
len (a1 : a2) = suc (len a2)
29 suceq 
len (rev a2) = len a2 -> suc (len (rev a2)) = suc (len a2)
30 28, 29 syl6eqr 
len (rev a2) = len a2 -> suc (len (rev a2)) = len (a1 : a2)
31 27, 30 syl5eq 
len (rev a2) = len a2 -> len (rev a2 |> a1) = len (a1 : a2)
32 26, 31 syl5eq 
len (rev a2) = len a2 -> len (rev (a1 : a2)) = len (a1 : a2)
33 5, 10, 15, 20, 23, 32 listind 
len (rev l) = len 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)