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 id 
l2 = a ++ r2 -> l2 = a ++ r2
23 22 anwr 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l2 = a ++ r2
24 23 appendeq2d 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 ++ l2 = l1 ++ a ++ r2
25 id 
r1 = l1 ++ a -> r1 = l1 ++ a
26 25 anwl 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r1 = l1 ++ a
27 26 appendeq1d 
r1 = l1 ++ a /\ l2 = a ++ r2 -> r1 ++ r2 = (l1 ++ a) ++ r2
28 24, 27 eqeqd 
r1 = l1 ++ a /\ l2 = a ++ r2 -> (l1 ++ l2 = r1 ++ r2 <-> l1 ++ a ++ r2 = (l1 ++ a) ++ r2)
29 21, 28 mpbiri 
r1 = l1 ++ a /\ l2 = a ++ r2 -> l1 ++ l2 = r1 ++ r2
30 18, 29 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
31 appendass 
(r1 ++ a) ++ l2 = r1 ++ a ++ l2
32 id 
l1 = r1 ++ a -> l1 = r1 ++ a
33 32 anwl 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 = r1 ++ a
34 33 appendeq1d 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = (r1 ++ a) ++ l2
35 id 
r2 = a ++ l2 -> r2 = a ++ l2
36 35 anwr 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r2 = a ++ l2
37 36 appendeq2d 
l1 = r1 ++ a /\ r2 = a ++ l2 -> r1 ++ r2 = r1 ++ a ++ l2
38 34, 37 eqeqd 
l1 = r1 ++ a /\ r2 = a ++ l2 -> (l1 ++ l2 = r1 ++ r2 <-> (r1 ++ a) ++ l2 = r1 ++ a ++ l2)
39 31, 38 mpbiri 
l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2
40 30, 39 ax_mp 
r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2 -> l1 ++ l2 = r1 ++ r2
41 40 eex 
E. a (r1 = l1 ++ a /\ l2 = a ++ r2 \/ l1 = r1 ++ a /\ r2 = a ++ l2) -> l1 ++ l2 = r1 ++ r2
42 17, 41 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)