Theorem repeatadd ≪ | index | src | ≫ 

theorem repeatadd (a m n: nat): $ repeat a (m + n) = repeat a m ++ repeat a n $;
StepHypRefExpression
1 id 
_1 = m -> _1 = m
2 1 addeq1d 
_1 = m -> _1 + n = m + n
3 2 repeateq2d 
_1 = m -> repeat a (_1 + n) = repeat a (m + n)
4 1 repeateq2d 
_1 = m -> repeat a _1 = repeat a m
5 4 appendeq1d 
_1 = m -> repeat a _1 ++ repeat a n = repeat a m ++ repeat a n
6 3, 5 eqeqd 
_1 = m -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (m + n) = repeat a m ++ repeat a n)
7 id 
_1 = 0 -> _1 = 0
8 7 addeq1d 
_1 = 0 -> _1 + n = 0 + n
9 8 repeateq2d 
_1 = 0 -> repeat a (_1 + n) = repeat a (0 + n)
10 7 repeateq2d 
_1 = 0 -> repeat a _1 = repeat a 0
11 10 appendeq1d 
_1 = 0 -> repeat a _1 ++ repeat a n = repeat a 0 ++ repeat a n
12 9, 11 eqeqd 
_1 = 0 -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (0 + n) = repeat a 0 ++ repeat a n)
13 id 
_1 = a1 -> _1 = a1
14 13 addeq1d 
_1 = a1 -> _1 + n = a1 + n
15 14 repeateq2d 
_1 = a1 -> repeat a (_1 + n) = repeat a (a1 + n)
16 13 repeateq2d 
_1 = a1 -> repeat a _1 = repeat a a1
17 16 appendeq1d 
_1 = a1 -> repeat a _1 ++ repeat a n = repeat a a1 ++ repeat a n
18 15, 17 eqeqd 
_1 = a1 -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (a1 + n) = repeat a a1 ++ repeat a n)
19 id 
_1 = suc a1 -> _1 = suc a1
20 19 addeq1d 
_1 = suc a1 -> _1 + n = suc a1 + n
21 20 repeateq2d 
_1 = suc a1 -> repeat a (_1 + n) = repeat a (suc a1 + n)
22 19 repeateq2d 
_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
23 22 appendeq1d 
_1 = suc a1 -> repeat a _1 ++ repeat a n = repeat a (suc a1) ++ repeat a n
24 21, 23 eqeqd 
_1 = suc a1 -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (suc a1 + n) = repeat a (suc a1) ++ repeat a n)
25 eqtr4 
repeat a (0 + n) = repeat a n -> repeat a 0 ++ repeat a n = repeat a n -> repeat a (0 + n) = repeat a 0 ++ repeat a n
26 repeateq2 
0 + n = n -> repeat a (0 + n) = repeat a n
27 add01 
0 + n = n
28 26, 27 ax_mp 
repeat a (0 + n) = repeat a n
29 25, 28 ax_mp 
repeat a 0 ++ repeat a n = repeat a n -> repeat a (0 + n) = repeat a 0 ++ repeat a n
30 eqtr 
repeat a 0 ++ repeat a n = 0 ++ repeat a n -> 0 ++ repeat a n = repeat a n -> repeat a 0 ++ repeat a n = repeat a n
31 appendeq1 
repeat a 0 = 0 -> repeat a 0 ++ repeat a n = 0 ++ repeat a n
32 repeat0 
repeat a 0 = 0
33 31, 32 ax_mp 
repeat a 0 ++ repeat a n = 0 ++ repeat a n
34 30, 33 ax_mp 
0 ++ repeat a n = repeat a n -> repeat a 0 ++ repeat a n = repeat a n
35 append0 
0 ++ repeat a n = repeat a n
36 34, 35 ax_mp 
repeat a 0 ++ repeat a n = repeat a n
37 29, 36 ax_mp 
repeat a (0 + n) = repeat a 0 ++ repeat a n
38 repeateq2 
suc a1 + n = suc (a1 + n) -> repeat a (suc a1 + n) = repeat a (suc (a1 + n))
39 addS1 
suc a1 + n = suc (a1 + n)
40 38, 39 ax_mp 
repeat a (suc a1 + n) = repeat a (suc (a1 + n))
41 appendeq1 
repeat a (suc a1) = a : repeat a a1 -> repeat a (suc a1) ++ repeat a n = a : repeat a a1 ++ repeat a n
42 repeatS 
repeat a (suc a1) = a : repeat a a1
43 41, 42 ax_mp 
repeat a (suc a1) ++ repeat a n = a : repeat a a1 ++ repeat a n
44 repeatS 
repeat a (suc (a1 + n)) = a : repeat a (a1 + n)
45 appendS 
a : repeat a a1 ++ repeat a n = a : (repeat a a1 ++ repeat a n)
46 conseq2 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> a : repeat a (a1 + n) = a : (repeat a a1 ++ repeat a n)
47 44, 45, 46 eqtr4g 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> repeat a (suc (a1 + n)) = a : repeat a a1 ++ repeat a n
48 40, 43, 47 eqtr4g 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> repeat a (suc a1 + n) = repeat a (suc a1) ++ repeat a n
49 6, 12, 18, 24, 37, 48 ind 
repeat a (m + n) = repeat a m ++ repeat a n

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)