Theorem revappend ≪ | index | src | ≫ 

theorem revappend (l1 l2: nat): $ rev (l1 ++ l2) = rev l2 ++ rev l1 $;
StepHypRefExpression
1 id 
_1 = l1 -> _1 = l1
2 eqidd 
_1 = l1 -> l2 = l2
3 1, 2 appendeqd 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
4 3 reveqd 
_1 = l1 -> rev (_1 ++ l2) = rev (l1 ++ l2)
5 eqidd 
_1 = l1 -> rev l2 = rev l2
6 1 reveqd 
_1 = l1 -> rev _1 = rev l1
7 5, 6 appendeqd 
_1 = l1 -> rev l2 ++ rev _1 = rev l2 ++ rev l1
8 4, 7 eqeqd 
_1 = l1 -> (rev (_1 ++ l2) = rev l2 ++ rev _1 <-> rev (l1 ++ l2) = rev l2 ++ rev l1)
9 id 
_1 = 0 -> _1 = 0
10 eqidd 
_1 = 0 -> l2 = l2
11 9, 10 appendeqd 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
12 11 reveqd 
_1 = 0 -> rev (_1 ++ l2) = rev (0 ++ l2)
13 eqidd 
_1 = 0 -> rev l2 = rev l2
14 9 reveqd 
_1 = 0 -> rev _1 = rev 0
15 13, 14 appendeqd 
_1 = 0 -> rev l2 ++ rev _1 = rev l2 ++ rev 0
16 12, 15 eqeqd 
_1 = 0 -> (rev (_1 ++ l2) = rev l2 ++ rev _1 <-> rev (0 ++ l2) = rev l2 ++ rev 0)
17 id 
_1 = a2 -> _1 = a2
18 eqidd 
_1 = a2 -> l2 = l2
19 17, 18 appendeqd 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
20 19 reveqd 
_1 = a2 -> rev (_1 ++ l2) = rev (a2 ++ l2)
21 eqidd 
_1 = a2 -> rev l2 = rev l2
22 17 reveqd 
_1 = a2 -> rev _1 = rev a2
23 21, 22 appendeqd 
_1 = a2 -> rev l2 ++ rev _1 = rev l2 ++ rev a2
24 20, 23 eqeqd 
_1 = a2 -> (rev (_1 ++ l2) = rev l2 ++ rev _1 <-> rev (a2 ++ l2) = rev l2 ++ rev a2)
25 id 
_1 = a1 : a2 -> _1 = a1 : a2
26 eqidd 
_1 = a1 : a2 -> l2 = l2
27 25, 26 appendeqd 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
28 27 reveqd 
_1 = a1 : a2 -> rev (_1 ++ l2) = rev (a1 : a2 ++ l2)
29 eqidd 
_1 = a1 : a2 -> rev l2 = rev l2
30 25 reveqd 
_1 = a1 : a2 -> rev _1 = rev (a1 : a2)
31 29, 30 appendeqd 
_1 = a1 : a2 -> rev l2 ++ rev _1 = rev l2 ++ rev (a1 : a2)
32 28, 31 eqeqd 
_1 = a1 : a2 -> (rev (_1 ++ l2) = rev l2 ++ rev _1 <-> rev (a1 : a2 ++ l2) = rev l2 ++ rev (a1 : a2))
33 eqtr4 
rev (0 ++ l2) = rev l2 -> rev l2 ++ rev 0 = rev l2 -> rev (0 ++ l2) = rev l2 ++ rev 0
34 reveq 
0 ++ l2 = l2 -> rev (0 ++ l2) = rev l2
35 append0 
0 ++ l2 = l2
36 34, 35 ax_mp 
rev (0 ++ l2) = rev l2
37 33, 36 ax_mp 
rev l2 ++ rev 0 = rev l2 -> rev (0 ++ l2) = rev l2 ++ rev 0
38 eqtr 
rev l2 ++ rev 0 = rev l2 ++ 0 -> rev l2 ++ 0 = rev l2 -> rev l2 ++ rev 0 = rev l2
39 appendeq2 
rev 0 = 0 -> rev l2 ++ rev 0 = rev l2 ++ 0
40 rev0 
rev 0 = 0
41 39, 40 ax_mp 
rev l2 ++ rev 0 = rev l2 ++ 0
42 38, 41 ax_mp 
rev l2 ++ 0 = rev l2 -> rev l2 ++ rev 0 = rev l2
43 append02 
rev l2 ++ 0 = rev l2
44 42, 43 ax_mp 
rev l2 ++ rev 0 = rev l2
45 37, 44 ax_mp 
rev (0 ++ l2) = rev l2 ++ rev 0
46 eqtr 
rev (a1 : a2 ++ l2) = rev (a1 : (a2 ++ l2)) -> rev (a1 : (a2 ++ l2)) = rev (a2 ++ l2) |> a1 -> rev (a1 : a2 ++ l2) = rev (a2 ++ l2) |> a1
47 reveq 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> rev (a1 : a2 ++ l2) = rev (a1 : (a2 ++ l2))
48 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
49 47, 48 ax_mp 
rev (a1 : a2 ++ l2) = rev (a1 : (a2 ++ l2))
50 46, 49 ax_mp 
rev (a1 : (a2 ++ l2)) = rev (a2 ++ l2) |> a1 -> rev (a1 : a2 ++ l2) = rev (a2 ++ l2) |> a1
51 revS 
rev (a1 : (a2 ++ l2)) = rev (a2 ++ l2) |> a1
52 50, 51 ax_mp 
rev (a1 : a2 ++ l2) = rev (a2 ++ l2) |> a1
53 appendeq2 
rev (a1 : a2) = rev a2 |> a1 -> rev l2 ++ rev (a1 : a2) = rev l2 ++ (rev a2 |> a1)
54 revS 
rev (a1 : a2) = rev a2 |> a1
55 53, 54 ax_mp 
rev l2 ++ rev (a1 : a2) = rev l2 ++ (rev a2 |> a1)
56 appendsnoc 
rev l2 ++ (rev a2 |> a1) = rev l2 ++ rev a2 |> a1
57 snoceq1 
rev (a2 ++ l2) = rev l2 ++ rev a2 -> rev (a2 ++ l2) |> a1 = rev l2 ++ rev a2 |> a1
58 56, 57 syl6eqr 
rev (a2 ++ l2) = rev l2 ++ rev a2 -> rev (a2 ++ l2) |> a1 = rev l2 ++ (rev a2 |> a1)
59 55, 58 syl6eqr 
rev (a2 ++ l2) = rev l2 ++ rev a2 -> rev (a2 ++ l2) |> a1 = rev l2 ++ rev (a1 : a2)
60 52, 59 syl5eq 
rev (a2 ++ l2) = rev l2 ++ rev a2 -> rev (a1 : a2 ++ l2) = rev l2 ++ rev (a1 : a2)
61 8, 16, 24, 32, 45, 60 listind 
rev (l1 ++ l2) = rev l2 ++ rev l1

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)