Theorem revappend ≪ | index | src | ≫ 

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