---

Step * of Lemma bool-bar-induction

∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
  ∀R:(T List) ⟶ 𝔹
    ((∀s:{s:T List| ↑R[s]} . A[s])
    ⇒ (∀s:{s:T List| ¬↑R[s]} . ((∀t:T. A[s @ [t]]) ⇒ A[s]))
    ⇒ (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[map(alpha;upto(n))])))
    ⇒ A[[]])
BY
{ (Auto
   THEN RenameVar `b' (-3)
   THEN RenameVar `i' (-2)
   THEN UseWitness ⌜bbar-recursion(R;
                                   b;
                                   i;
                                   [])⌝⋅
   THEN Auto
   THEN Reduce 0
   THEN BackThruSomeHyp) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RenameVar  `b'  (-3)
  THEN  RenameVar  `i'  (-2)
  THEN  UseWitness  \mkleeneopen{}bbar-recursion(R;
                                                                  b;
                                                                  i;
                                                                  [])\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Reduce  0
  THEN  BackThruSomeHyp)

---

Home Index