---

Step * of Lemma AF-induction

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀[Q:T ⟶ ℙ]. TI(T;x,y.¬R[x;y];t.Q[t])) supposing 
     (AFx,y:T.R[x;y] and 
     (∀x,y,z:T.  ((¬R[x;y]) ⇒ (¬R[y;z]) ⇒ (¬R[x;z]))))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (InstLemma `AF-spread-law_wf` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
   THEN (InstLemma `AFbar_wf` [⌜T⌝;⌜R⌝]⋅ THENA Auto)
   THEN InstLemma `basic_strong_bar_induction` [⌜T?⌝;⌜AF-spread-law(x,y.R[x;y])⌝;⌜AFbar()⌝;
   ⌜λ2n s.∀a:{a:T| AF-spread-law(x,y.R[x;y]) n s (inl a)} . Q[a]⌝]⋅
   THEN Try (Complete (Auto))
   THEN Try ((InstLemma `AF-path-barred` [⌜T⌝;⌜R⌝] ⋅ THEN Complete (Auto)))
   THEN Try (((InstLemma `at_AFbar` [⌜T⌝;⌜R⌝]⋅ THENA Auto) THEN RepeatFor 3 (ParallelLast') THEN Complete (Auto)))) }

1
.....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]))

2
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]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}[Q:T  {}\mrightarrow{}  \mBbbP{}].  TI(T;x,y.\mneg{}R[x;y];t.Q[t]))  supposing 
          (AFx,y:T.R[x;y]  and 
          (\mforall{}x,y,z:T.    ((\mneg{}R[x;y])  {}\mRightarrow{}  (\mneg{}R[y;z])  {}\mRightarrow{}  (\mneg{}R[x;z]))))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (InstLemma  `AF-spread-law\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `AFbar\_wf`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `basic\_strong\_bar\_induction`  [\mkleeneopen{}T?\mkleeneclose{};\mkleeneopen{}AF-spread-law(x,y.R[x;y])\mkleeneclose{};\mkleeneopen{}AFbar()\mkleeneclose{};
  \mkleeneopen{}\mlambda{}\msubtwo{}n  s.\mforall{}a:\{a:T|  AF-spread-law(x,y.R[x;y])  n  s  (inl  a)\}  .  Q[a]\mkleeneclose{}]\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((InstLemma  `AF-path-barred`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]  \mcdot{}  THEN  Complete  (Auto)))
  THEN  Try  (((InstLemma  `at\_AFbar`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{}]\mcdot{}  THENA  Auto)
                        THEN  RepeatFor  3  (ParallelLast')
                        THEN  Complete  (Auto))))

---

Home Index