---

Step * 2 of Lemma agree_on_equiv


1. T : Type
2. P : T ⟶ ℙ
3. ∀a,b:T List.
     (((||a|| = ||b|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T))))
     ⇒ ((||b|| = ||a|| ∈ ℤ) c∧ (∀i:ℕ||b||. ((P[b[i]] ∨ P[a[i]]) ⇒ (b[i] = a[i] ∈ T)))))
4. a : T List
5. b : T List
6. c : T List
7. (||a|| = ||b|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T)))
8. (||b|| = ||c|| ∈ ℤ) c∧ (∀i:ℕ||b||. ((P[b[i]] ∨ P[c[i]]) ⇒ (b[i] = c[i] ∈ T)))
9. ||a|| = ||c|| ∈ ℤ
10. i : ℕ||a||
11. P[a[i]] ∨ P[c[i]]
⊢ a[i] = c[i] ∈ T
BY
{ SplitAndHyps }

1
1. T : Type
2. P : T ⟶ ℙ
3. ∀a,b:T List.
     (((||a|| = ||b|| ∈ ℤ) c∧ (∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T))))
     ⇒ ((||b|| = ||a|| ∈ ℤ) c∧ (∀i:ℕ||b||. ((P[b[i]] ∨ P[a[i]]) ⇒ (b[i] = a[i] ∈ T)))))
4. a : T List
5. b : T List
6. c : T List
7. ||a|| = ||b|| ∈ ℤ
8. ∀i:ℕ||a||. ((P[a[i]] ∨ P[b[i]]) ⇒ (a[i] = b[i] ∈ T))
9. ||b|| = ||c|| ∈ ℤ
10. ∀i:ℕ||b||. ((P[b[i]] ∨ P[c[i]]) ⇒ (b[i] = c[i] ∈ T))
11. ||a|| = ||c|| ∈ ℤ
12. i : ℕ||a||
13. P[a[i]] ∨ P[c[i]]
⊢ a[i] = c[i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:T  List.
          (((||a||  =  ||b||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||a||.  ((P[a[i]]  \mvee{}  P[b[i]])  {}\mRightarrow{}  (a[i]  =  b[i]))))
          {}\mRightarrow{}  ((||b||  =  ||a||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||b||.  ((P[b[i]]  \mvee{}  P[a[i]])  {}\mRightarrow{}  (b[i]  =  a[i])))))
4.  a  :  T  List
5.  b  :  T  List
6.  c  :  T  List
7.  (||a||  =  ||b||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||a||.  ((P[a[i]]  \mvee{}  P[b[i]])  {}\mRightarrow{}  (a[i]  =  b[i])))
8.  (||b||  =  ||c||)  c\mwedge{}  (\mforall{}i:\mBbbN{}||b||.  ((P[b[i]]  \mvee{}  P[c[i]])  {}\mRightarrow{}  (b[i]  =  c[i])))
9.  ||a||  =  ||c||
10.  i  :  \mBbbN{}||a||
11.  P[a[i]]  \mvee{}  P[c[i]]
\mvdash{}  a[i]  =  c[i]


By

---

Latex:
SplitAndHyps

---

Home Index