Theorem eqappend ≪ | index | src | ≫ 

theorem eqappend {a: nat} (l1 l2 r1 r2: nat):
  $ l1 ++ l2 = r1 ++ r2 <->
    E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2) $;
StepHypRefExpression
1 eor 
(len l1 <= len r1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)) ->
  (len r1 <= len l1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)) ->
  len l1 <= len r1 \/ len r1 <= len l1 ->
  l1 ++ l2 = r1 ++ r2 ->
  E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
2 eqcom 
l1 ++ l2 = r1 ++ r2 -> r1 ++ r2 = l1 ++ l2
3 eqappendlem 
len l1 <= len r1 /\ r1 ++ r2 = l1 ++ l2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2)
4 orl 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2
5 4 eximi 
E. a (r1 = l1 ++ a /\ l2 = a ++ r2) -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
6 3, 5 rsyl 
len l1 <= len r1 /\ r1 ++ r2 = l1 ++ l2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
7 6 exp 
len l1 <= len r1 -> r1 ++ r2 = l1 ++ l2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
8 2, 7 syl5 
len l1 <= len r1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
9 1, 8 ax_mp 
(len r1 <= len l1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)) ->
  len l1 <= len r1 \/ len r1 <= len l1 ->
  l1 ++ l2 = r1 ++ r2 ->
  E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
10 eqappendlem 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> E. a (l1 = r1 ++ a /\ r2 = a ++ l2)
11 orr 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2
12 11 eximi 
E. a (l1 = r1 ++ a /\ r2 = a ++ l2) -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
13 10, 12 rsyl 
len r1 <= len l1 /\ l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
14 13 exp 
len r1 <= len l1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
15 9, 14 ax_mp 
len l1 <= len r1 \/ len r1 <= len l1 -> l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
16 leorle 
len l1 <= len r1 \/ len r1 <= len l1
17 15, 16 ax_mp 
l1 ++ l2 = r1 ++ r2 -> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)
18 eor 
(r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 ++ l2 = r1 ++ r2) ->
  (l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2) ->
  r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2 ->
  l1 ++ l2 = r1 ++ r2
19 eqcom 
(l1 ++ a) ++ r2 = l1 ++ a ++ r2 -> l1 ++ a ++ r2 = (l1 ++ a) ++ r2
20 appendass 
(l1 ++ a) ++ r2 = l1 ++ a ++ r2
21 19, 20 ax_mp 
l1 ++ a ++ r2 = (l1 ++ a) ++ r2
22 eqidd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 = l1
23 id 
l2 = a ++ r2 -> l2 = a ++ r2
24 23 anwr 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l2 = a ++ r2
25 22, 24 appendeqd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 ++ l2 = l1 ++ a ++ r2
26 id 
r1 = l1 ++ a -> r1 = l1 ++ a
27 26 anwl 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r1 = l1 ++ a
28 eqidd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r2 = r2
29 27, 28 appendeqd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r1 ++ r2 = (l1 ++ a) ++ r2
30 25, 29 eqeqd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> (l1 ++ l2 = r1 ++ r2 <-> l1 ++ a ++ r2 = (l1 ++ a) ++ r2)
31 21, 30 mpbiri 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 ++ l2 = r1 ++ r2
32 18, 31 ax_mp 
(l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2) -> r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2
33 appendass 
(r1 ++ a) ++ l2 = r1 ++ a ++ l2
34 id 
l1 = r1 ++ a -> l1 = r1 ++ a
35 34 anwl 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 = r1 ++ a
36 eqidd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l2 = l2
37 35, 36 appendeqd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = (r1 ++ a) ++ l2
38 eqidd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r1 = r1
39 id 
r2 = a ++ l2 -> r2 = a ++ l2
40 39 anwr 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r2 = a ++ l2
41 38, 40 appendeqd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r1 ++ r2 = r1 ++ a ++ l2
42 37, 41 eqeqd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> (l1 ++ l2 = r1 ++ r2 <-> (r1 ++ a) ++ l2 = r1 ++ a ++ l2)
43 33, 42 mpbiri 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2
44 32, 43 ax_mp 
r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2
45 44 eex 
E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2) -> l1 ++ l2 = r1 ++ r2
46 17, 45 ibii 
l1 ++ l2 = r1 ++ r2 <-> E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2)

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)