---

Step * 1 of Lemma AF-induction

.....antecedent..... 
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) ⟶ ℙ
⊢ ∀n:ℕ. ∀s:AF-spread-law(x,y.R[x;y])-consistent-seq(n).
    ((∀t:{t:T?| AF-spread-law(x,y.R[x;y]) n s t} . ∀a:{a:T| AF-spread-law(x,y.R[x;y]) (n + 1) s.t@n (inl a)} .  Q[a])
    ⇒ (∀a:{a:T| AF-spread-law(x,y.R[x;y]) n s (inl a)} . Q[a]))
BY
{ (Auto
   THEN OnMaybeHyp 6 (\h. (BHyp h
                           THEN Auto
                           THEN (InstHyp [⌜inl a⌝] (-3)⋅ THENA Auto)
                           THEN BHyp -1 
                           THEN DVar `s'
                           THEN DSetVars
                           THEN MemTypeCD
                           THEN Auto
                           THEN All (RepUR ``AF-spread-law seq-add``)
                           THEN (UnivCD THENA Auto)
                           THEN AutoSplit))
   ) }

---

Latex:

---

Latex:
.....antecedent..... 
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{}
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}s:AF-spread-law(x,y.R[x;y])-consistent-seq(n).
        ((\mforall{}t:\{t:T?|  AF-spread-law(x,y.R[x;y])  n  s  t\}  .  \mforall{}a:\{a:T| 
                                                                                                            AF-spread-law(x,y.R[x;y])  (n  +  1)  s.t@n 
                                                                                                            (inl  a)\}  .
                Q[a])
        {}\mRightarrow{}  (\mforall{}a:\{a:T|  AF-spread-law(x,y.R[x;y])  n  s  (inl  a)\}  .  Q[a]))


By

---

Latex:
(Auto
  THEN  OnMaybeHyp  6  (\mbackslash{}h.  (BHyp  h
                                                  THEN  Auto
                                                  THEN  (InstHyp  [\mkleeneopen{}inl  a\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
                                                  THEN  BHyp  -1 
                                                  THEN  DVar  `s'
                                                  THEN  DSetVars
                                                  THEN  MemTypeCD
                                                  THEN  Auto
                                                  THEN  All  (RepUR  ``AF-spread-law  seq-add``)
                                                  THEN  (UnivCD  THENA  Auto)
                                                  THEN  AutoSplit))
  )

---

Home Index