---

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 InstLemma `basic-bar-induction` [⌜T⌝;⌜λ2s.↑R[s]⌝;⌜A⌝]⋅ THEN Auto) }

1
1. [T] : Type
2. [A] : (T List) ⟶ ℙ
3. R : (T List) ⟶ 𝔹@i
4. ∀s:{s:T List| ↑R[s]} . A[s]@i
5. ∀s:{s:T List| ¬↑R[s]} . ((∀t:T. A[s @ [t]]) ⇒ A[s])@i
6. ∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[map(alpha;upto(n))]))@i
7. s : T List@i
8. ∀t:T. A[s @ [t]]@i
⊢ A[s]

---

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  InstLemma  `basic-bar-induction`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}s.\muparrow{}R[s]\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index