Step | Hyp | Ref | Expression |
1 |
|
eqeq |
take (l1 ++ l2) (len l1) = l1 -> take (r1 ++ r2) (len r1) = r1 -> (take (l1 ++ l2) (len l1) = take (r1 ++ r2) (len r1) <-> l1 = r1) |
2 |
|
eqtr |
take (l1 ++ l2) (len l1) = take l1 (len l1) -> take l1 (len l1) = l1 -> take (l1 ++ l2) (len l1) = l1 |
3 |
|
takeappend1 |
len l1 <= len l1 -> take (l1 ++ l2) (len l1) = take l1 (len l1) |
4 |
|
leid |
len l1 <= len l1 |
5 |
3, 4 |
ax_mp |
take (l1 ++ l2) (len l1) = take l1 (len l1) |
6 |
2, 5 |
ax_mp |
take l1 (len l1) = l1 -> take (l1 ++ l2) (len l1) = l1 |
7 |
|
takeall |
len l1 <= len l1 -> take l1 (len l1) = l1 |
8 |
7, 4 |
ax_mp |
take l1 (len l1) = l1 |
9 |
6, 8 |
ax_mp |
take (l1 ++ l2) (len l1) = l1 |
10 |
1, 9 |
ax_mp |
take (r1 ++ r2) (len r1) = r1 -> (take (l1 ++ l2) (len l1) = take (r1 ++ r2) (len r1) <-> l1 = r1) |
11 |
|
eqtr |
take (r1 ++ r2) (len r1) = take r1 (len r1) -> take r1 (len r1) = r1 -> take (r1 ++ r2) (len r1) = r1 |
12 |
|
takeappend1 |
len r1 <= len r1 -> take (r1 ++ r2) (len r1) = take r1 (len r1) |
13 |
|
leid |
len r1 <= len r1 |
14 |
12, 13 |
ax_mp |
take (r1 ++ r2) (len r1) = take r1 (len r1) |
15 |
11, 14 |
ax_mp |
take r1 (len r1) = r1 -> take (r1 ++ r2) (len r1) = r1 |
16 |
|
takeall |
len r1 <= len r1 -> take r1 (len r1) = r1 |
17 |
16, 13 |
ax_mp |
take r1 (len r1) = r1 |
18 |
15, 17 |
ax_mp |
take (r1 ++ r2) (len r1) = r1 |
19 |
10, 18 |
ax_mp |
take (l1 ++ l2) (len l1) = take (r1 ++ r2) (len r1) <-> l1 = r1 |
20 |
|
anr |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = r1 ++ r2 |
21 |
|
anl |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> len l1 = len r1 |
22 |
20, 21 |
takeeqd |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> take (l1 ++ l2) (len l1) = take (r1 ++ r2) (len r1) |
23 |
19, 22 |
sylib |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 |
24 |
|
appendcan1 |
l1 ++ l2 = l1 ++ r2 <-> l2 = r2 |
25 |
23 |
appendeq1d |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ r2 = r1 ++ r2 |
26 |
20, 25 |
eqtr4d |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l1 ++ l2 = l1 ++ r2 |
27 |
24, 26 |
sylib |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l2 = r2 |
28 |
23, 27 |
iand |
len l1 = len r1 /\ l1 ++ l2 = r1 ++ r2 -> l1 = r1 /\ l2 = r2 |
29 |
|
anrl |
len l1 = len r1 /\ (l1 = r1 /\ l2 = r2) -> l1 = r1 |
30 |
|
anrr |
len l1 = len r1 /\ (l1 = r1 /\ l2 = r2) -> l2 = r2 |
31 |
29, 30 |
appendeqd |
len l1 = len r1 /\ (l1 = r1 /\ l2 = r2) -> l1 ++ l2 = r1 ++ r2 |
32 |
28, 31 |
ibida |
len l1 = len r1 -> (l1 ++ l2 = r1 ++ r2 <-> l1 = r1 /\ l2 = r2) |