---

Step * 1 of Lemma bool_bar_induction


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]
BY
{ (Decide ⌜↑R[s]⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [A]  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  R  :  (T  List)  {}\mrightarrow{}  \mBbbB{}@i
4.  \mforall{}s:\{s:T  List|  \muparrow{}R[s]\}  .  A[s]@i
5.  \mforall{}s:\{s:T  List|  \mneg{}\muparrow{}R[s]\}  .  ((\mforall{}t:T.  A[s  @  [t]])  {}\mRightarrow{}  A[s])@i
6.  \mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  (\muparrow{}R[map(alpha;upto(n))]))@i
7.  s  :  T  List@i
8.  \mforall{}t:T.  A[s  @  [t]]@i
\mvdash{}  A[s]


By

---

Latex:
(Decide  \mkleeneopen{}\muparrow{}R[s]\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index