---

Step * of Lemma proper-iseg-append

∀[T:Type]. ∀L1,L2,L3,L4:T List.  L1 @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (L1 = L2 ∈ (T List)) supposing ||L1|| = ||L2|| ∈ ℤ
BY
{ (RepeatFor 2 (InductionOnList) THEN Reduce 0 THEN Auto THEN Auto') }

1
1. [T] : Type
2. u : T
3. v : T List
4. ∀L2,L3,L4:T List.  v @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (v = L2 ∈ (T List)) supposing ||v|| = ||L2|| ∈ ℤ
5. u1 : T
6. v1 : T List
7. ∀L3,L4:T List.  [u / v] @ L3 < v1 @ L4 ⇐⇒ L3 < L4 ∧ ([u / v] = v1 ∈ (T List)) supposing ||[u / v]|| = ||v1|| ∈ ℤ
8. L3 : T List
9. L4 : T List
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. [u / (v @ L3)] < [u1 / (v1 @ L4)]
⊢ L3 < L4

2
1. T : Type
2. u : T
3. v : T List
4. ∀L2,L3,L4:T List.  v @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (v = L2 ∈ (T List)) supposing ||v|| = ||L2|| ∈ ℤ
5. u1 : T
6. v1 : T List
7. ∀L3,L4:T List.  [u / v] @ L3 < v1 @ L4 ⇐⇒ L3 < L4 ∧ ([u / v] = v1 ∈ (T List)) supposing ||[u / v]|| = ||v1|| ∈ ℤ
8. L3 : T List
9. L4 : T List
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. [u / (v @ L3)] < [u1 / (v1 @ L4)]
⊢ [u / v] = [u1 / v1] ∈ (T List)

3
1. [T] : Type
2. u : T
3. v : T List
4. ∀L2,L3,L4:T List.  v @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (v = L2 ∈ (T List)) supposing ||v|| = ||L2|| ∈ ℤ
5. u1 : T
6. v1 : T List
7. ∀L3,L4:T List.  [u / v] @ L3 < v1 @ L4 ⇐⇒ L3 < L4 ∧ ([u / v] = v1 ∈ (T List)) supposing ||[u / v]|| = ||v1|| ∈ ℤ
8. L3 : T List
9. L4 : T List
10. (||v|| + 1) = (||v1|| + 1) ∈ ℤ
11. L3 < L4
12. [u / v] = [u1 / v1] ∈ (T List)
⊢ [u / (v @ L3)] < [u1 / (v1 @ L4)]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L1,L2,L3,L4:T  List.    L1  @  L3  <  L2  @  L4  \mLeftarrow{}{}\mRightarrow{}  L3  <  L4  \mwedge{}  (L1  =  L2)  supposing  ||L1||  =  ||L2||


By

---

Latex:
(RepeatFor  2  (InductionOnList)  THEN  Reduce  0  THEN  Auto  THEN  Auto')

---

Home Index