---

Step * of Lemma AF-induction2

∀[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 InstLemma `AF-induction` [⌜T⌝;⌜λ2x y.¬R[x;y]⌝;⌜Q⌝]⋅ THEN Auto THEN RepeatFor 5 (ParallelLast)) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  InstLemma  `AF-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.\mneg{}R[x;y]\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RepeatFor  5  (ParallelLast))

---

Home Index