---

Step * 2 of Lemma AF-induction


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))
4. AFx,y:T.R[x;y]
5. [Q] : T ⟶ ℙ
6. ∀t:T. ((∀s:{s:T| ¬R[t;s]} . Q[s]) ⇒ Q[t])
7. t : T
8. AF-spread-law(x,y.R[x;y]) ∈ n:ℕ ⟶ (ℕn ⟶ (T?)) ⟶ (T?) ⟶ ℙ
9. AFbar() ∈ n:ℕ ⟶ AF-spread-law(x,y.R[x;y])-consistent-seq(n) ⟶ ℙ
10. ∀x:Top. ∀a:{a:T| AF-spread-law(x,y.R[x;y]) 0 x (inl a)} .  Q[a]
⊢ Q[t]
BY
{ (RepUR ``AF-spread-law`` -1 THEN InstHyp [⌜0⌝;⌜t⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))
4.  AFx,y:T.R[x;y]
5.  [Q]  :  T  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}t:T.  ((\mforall{}s:\{s:T|  \mneg{}R[t;s]\}  .  Q[s])  {}\mRightarrow{}  Q[t])
7.  t  :  T
8.  AF-spread-law(x,y.R[x;y])  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  (T?))  {}\mrightarrow{}  (T?)  {}\mrightarrow{}  \mBbbP{}
9.  AFbar()  \mmember{}  n:\mBbbN{}  {}\mrightarrow{}  AF-spread-law(x,y.R[x;y])-consistent-seq(n)  {}\mrightarrow{}  \mBbbP{}
10.  \mforall{}x:Top.  \mforall{}a:\{a:T|  AF-spread-law(x,y.R[x;y])  0  x  (inl  a)\}  .    Q[a]
\mvdash{}  Q[t]


By

---

Latex:
(RepUR  ``AF-spread-law``  -1  THEN  InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index