---

Step * 1 of Lemma pairwise-implies


1. [T] : Type
2. L : T List
3. [P] : T ⟶ T ⟶ ℙ'
4. ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]
5. x : T
6. y : T
7. i1 : ℕ
8. i1 < ||L||
9. x = L[i1] ∈ T
10. i : ℕ
11. i < ||L||
12. y = L[i] ∈ T
⊢ (L[i1] = L[i] ∈ T) ∨ P[L[i1];L[i]] ∨ P[L[i];L[i1]]
BY
{ (((Decide ⌜i1 < i⌝⋅ THENA Auto) THEN Try ((Sel 2 (D 0)⋅ THEN CompleteAuto)))
   THEN (Decide ⌜i < i1⌝⋅ THENA Auto)
   THEN Try ((Sel 3 (D 0)⋅ THEN Complete (Auto)))
   THEN Sel 1 (D 0)
   THEN Auto) }

1
1. T : Type
2. L : T List
3. P : T ⟶ T ⟶ ℙ'
4. ∀i:ℕ||L||. ∀j:ℕi.  P[L[j];L[i]]
5. x : T
6. y : T
7. i1 : ℕ
8. i1 < ||L||
9. x = L[i1] ∈ T
10. i : ℕ
11. i < ||L||
12. y = L[i] ∈ T
13. ¬i1 < i
14. ¬i < i1
⊢ L[i1] = L[i] ∈ T

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  L  :  T  List
3.  [P]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}'
4.  \mforall{}i:\mBbbN{}||L||.  \mforall{}j:\mBbbN{}i.    P[L[j];L[i]]
5.  x  :  T
6.  y  :  T
7.  i1  :  \mBbbN{}
8.  i1  <  ||L||
9.  x  =  L[i1]
10.  i  :  \mBbbN{}
11.  i  <  ||L||
12.  y  =  L[i]
\mvdash{}  (L[i1]  =  L[i])  \mvee{}  P[L[i1];L[i]]  \mvee{}  P[L[i];L[i1]]


By

---

Latex:
(((Decide  \mkleeneopen{}i1  <  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Try  ((Sel  2  (D  0)\mcdot{}  THEN  CompleteAuto)))
  THEN  (Decide  \mkleeneopen{}i  <  i1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  ((Sel  3  (D  0)\mcdot{}  THEN  Complete  (Auto)))
  THEN  Sel  1  (D  0)
  THEN  Auto)

---

Home Index