---

Step * 1 of Lemma AF-induction-iff


1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))))
4. ∀x,y:T.  Dec(R+[x;y])
5. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])
⊢ AFx,y:T.¬(R+ x y)
BY
{ (D 0 THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t]) supposing ∃R':T ⟶ T ⟶ ℙ. (AFx,y:T.R'[x;y] ∧ (∀x,y:T.  (R+[x;y] ⇒ (¬R'[x;y]))))
4. ∀x,y:T.  Dec(R+[x;y])
5. ∀Q:T ⟶ ℙ. TI(T;x,y.R[x;y];t.Q[t])
6. f : ℕ ⟶ T
⊢ ↓∃i,j:ℕ. (i < j ∧ (¬(R+ (f i) (f j))))

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  TI(T;x,y.R[x;y];t.Q[t]) 
      supposing  \mexists{}R':T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}.  (AFx,y:T.R'[x;y]  \mwedge{}  (\mforall{}x,y:T.    (R\msupplus{}[x;y]  {}\mRightarrow{}  (\mneg{}R'[x;y]))))
4.  \mforall{}x,y:T.    Dec(R\msupplus{}[x;y])
5.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.  TI(T;x,y.R[x;y];t.Q[t])
\mvdash{}  AFx,y:T.\mneg{}(R\msupplus{}  x  y)


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index