---

Step * of Lemma basic-bar-induction

∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
  ((∀s:T List. Dec(R[s]))
  ⇒ (∀s:T List. (R[s] ⇒ A[s]))
  ⇒ (∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s]))
  ⇒ (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[map(alpha;upto(n))]))
  ⇒ A[[]])
BY
{ ((InstLemma Obid: bar-induction) []⋅ THEN RepeatFor 6 ((ParallelLast' THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:(T  List)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}s:T  List.  Dec(R[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  (R[s]  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}s:T  List.  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s]))
    {}\mRightarrow{}  (\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  R[map(alpha;upto(n))]))
    {}\mRightarrow{}  A[[]])


By

---

Latex:
((InstLemma  Obid:  bar-induction)  []\mcdot{}  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))  THEN  Auto)

---

Home Index