Theorem repeatadd ≪ | index | src | ≫ 

theorem repeatadd (a m n: nat): $ repeat a (m + n) = repeat a m ++ repeat a n $;
StepHypRefExpression
1 eqidd 
_1 = m -> a = a
2 id 
_1 = m -> _1 = m
3 eqidd 
_1 = m -> n = n
4 2, 3 addeqd 
_1 = m -> _1 + n = m + n
5 1, 4 repeateqd 
_1 = m -> repeat a (_1 + n) = repeat a (m + n)
6 1, 2 repeateqd 
_1 = m -> repeat a _1 = repeat a m
7 eqidd 
_1 = m -> repeat a n = repeat a n
8 6, 7 appendeqd 
_1 = m -> repeat a _1 ++ repeat a n = repeat a m ++ repeat a n
9 5, 8 eqeqd 
_1 = m -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (m + n) = repeat a m ++ repeat a n)
10 eqidd 
_1 = 0 -> a = a
11 id 
_1 = 0 -> _1 = 0
12 eqidd 
_1 = 0 -> n = n
13 11, 12 addeqd 
_1 = 0 -> _1 + n = 0 + n
14 10, 13 repeateqd 
_1 = 0 -> repeat a (_1 + n) = repeat a (0 + n)
15 10, 11 repeateqd 
_1 = 0 -> repeat a _1 = repeat a 0
16 eqidd 
_1 = 0 -> repeat a n = repeat a n
17 15, 16 appendeqd 
_1 = 0 -> repeat a _1 ++ repeat a n = repeat a 0 ++ repeat a n
18 14, 17 eqeqd 
_1 = 0 -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (0 + n) = repeat a 0 ++ repeat a n)
19 eqidd 
_1 = a1 -> a = a
20 id 
_1 = a1 -> _1 = a1
21 eqidd 
_1 = a1 -> n = n
22 20, 21 addeqd 
_1 = a1 -> _1 + n = a1 + n
23 19, 22 repeateqd 
_1 = a1 -> repeat a (_1 + n) = repeat a (a1 + n)
24 19, 20 repeateqd 
_1 = a1 -> repeat a _1 = repeat a a1
25 eqidd 
_1 = a1 -> repeat a n = repeat a n
26 24, 25 appendeqd 
_1 = a1 -> repeat a _1 ++ repeat a n = repeat a a1 ++ repeat a n
27 23, 26 eqeqd 
_1 = a1 -> (repeat a (_1 + n) = repeat a _1 ++ repeat a n <-> repeat a (a1 + n) = repeat a a1 ++ repeat a n)
28 eqidd 
_1 = suc a1 -> a = a
29 id 
_1 = suc a1 -> _1 = suc a1
30 eqidd 
_1 = suc a1 -> n = n
31 29, 30 addeqd 
_1 = suc a1 -> _1 + n = suc a1 + n
32 28, 31 repeateqd 
_1 = suc a1 -> repeat a (_1 + n) = repeat a (suc a1 + n)
33 28, 29 repeateqd 
_1 = suc a1 -> repeat a _1 = repeat a (suc a1)
34 eqidd 
_1 = suc a1 -> repeat a n = repeat a n
35 33, 34 appendeqd 
_1 = suc a1 -> repeat a _1 ++ repeat a n = repeat a (suc a1) ++ repeat a n
36 32, 35 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)
37 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
38 repeateq2 
0 + n = n -> repeat a (0 + n) = repeat a n
39 add01 
0 + n = n
40 38, 39 ax_mp 
repeat a (0 + n) = repeat a n
41 37, 40 ax_mp 
repeat a 0 ++ repeat a n = repeat a n -> repeat a (0 + n) = repeat a 0 ++ repeat a n
42 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
43 appendeq1 
repeat a 0 = 0 -> repeat a 0 ++ repeat a n = 0 ++ repeat a n
44 repeat0 
repeat a 0 = 0
45 43, 44 ax_mp 
repeat a 0 ++ repeat a n = 0 ++ repeat a n
46 42, 45 ax_mp 
0 ++ repeat a n = repeat a n -> repeat a 0 ++ repeat a n = repeat a n
47 append0 
0 ++ repeat a n = repeat a n
48 46, 47 ax_mp 
repeat a 0 ++ repeat a n = repeat a n
49 41, 48 ax_mp 
repeat a (0 + n) = repeat a 0 ++ repeat a n
50 repeateq2 
suc a1 + n = suc (a1 + n) -> repeat a (suc a1 + n) = repeat a (suc (a1 + n))
51 addS1 
suc a1 + n = suc (a1 + n)
52 50, 51 ax_mp 
repeat a (suc a1 + n) = repeat a (suc (a1 + n))
53 appendeq1 
repeat a (suc a1) = a : repeat a a1 -> repeat a (suc a1) ++ repeat a n = a : repeat a a1 ++ repeat a n
54 repeatS 
repeat a (suc a1) = a : repeat a a1
55 53, 54 ax_mp 
repeat a (suc a1) ++ repeat a n = a : repeat a a1 ++ repeat a n
56 repeatS 
repeat a (suc (a1 + n)) = a : repeat a (a1 + n)
57 appendS 
a : repeat a a1 ++ repeat a n = a : (repeat a a1 ++ repeat a n)
58 conseq2 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> a : repeat a (a1 + n) = a : (repeat a a1 ++ repeat a n)
59 56, 57, 58 eqtr4g 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> repeat a (suc (a1 + n)) = a : repeat a a1 ++ repeat a n
60 52, 55, 59 eqtr4g 
repeat a (a1 + n) = repeat a a1 ++ repeat a n -> repeat a (suc a1 + n) = repeat a (suc a1) ++ repeat a n
61 9, 18, 27, 36, 49, 60 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)