---

Step * of Lemma W-type-induction

∀[A:Type]
  ((∀x,y:A.  Dec(x = y ∈ A))
  ⇒ (∀[B:A ⟶ Type]. ∀[P:W-type(A; a.B[a]) ⟶ ℙ].
        ((∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])) ⇒ (∀w:W-type(A; a.B[a]). P[w]))))
BY
{ (Auto
   THEN ((InstLemma `bool-bar-induction` [⌜a:A ⟶ (B[a]?)⌝;⌜λ2s.case Wselect(w;s) of inl(w) => P[w] | inr(z) => True⌝;
          ⌜λ2s.isr(Wselect(w;s))⌝]⋅
         THENM (Reduce (-1) THEN Trivial)
         )
         THEN Auto
         )⋅⋅
   ) }

1
1. [A] : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. [B] : A ⟶ Type
4. [P] : W-type(A; a.B[a]) ⟶ ℙ
5. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
6. w : W-type(A; a.B[a])@i
7. s : {s:(a:A ⟶ (B[a]?)) List| ↑isr(Wselect(w;s))} @i
⊢ case Wselect(w;s) of inl(w) => P[w] | inr(z) => True

2
1. [A] : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. [B] : A ⟶ Type
4. [P] : W-type(A; a.B[a]) ⟶ ℙ
5. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
6. w : W-type(A; a.B[a])@i
7. s : {s:(a:A ⟶ (B[a]?)) List| ¬↑isr(Wselect(w;s))} @i
8. ∀t:a:A ⟶ (B[a]?). case Wselect(w;s @ [t]) of inl(w) => P[w] | inr(z) => True
⊢ case Wselect(w;s) of inl(w) => P[w] | inr(z) => True

3
1. A : Type
2. ∀x,y:A.  Dec(x = y ∈ A)
3. B : A ⟶ Type
4. P : W-type(A; a.B[a]) ⟶ ℙ
5. ∀a:A. ∀f:B[a] ⟶ W-type(A; a.B[a]).  ((∀b:B[a]. P[f b]) ⇒ P[W-sup(a;f)])
6. w : W-type(A; a.B[a])@i
7. alpha : ℕ ⟶ a:A ⟶ (B[a]?)@i
⊢ ↓∃n:ℕ. (↑isr(Wselect(w;map(alpha;upto(n)))))

---

Latex:

---

Latex:
\mforall{}[A:Type]
    ((\mforall{}x,y:A.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[P:W-type(A;  a.B[a])  {}\mrightarrow{}  \mBbbP{}].
                ((\mforall{}a:A.  \mforall{}f:B[a]  {}\mrightarrow{}  W-type(A;  a.B[a]).    ((\mforall{}b:B[a].  P[f  b])  {}\mRightarrow{}  P[W-sup(a;f)]))
                {}\mRightarrow{}  (\mforall{}w:W-type(A;  a.B[a]).  P[w]))))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `bool-bar-induction`  [\mkleeneopen{}a:A  {}\mrightarrow{}  (B[a]?)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}s.case  Wselect(w;s)
                                                                                                                      of  inl(w)  =>
                                                                                                                      P[w]
                                                                                                                      |  inr(z)  =>
                                                                                                                      True\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}s.isr(Wselect(w;s))\mkleeneclose{}]\mcdot{}
              THENM  (Reduce  (-1)  THEN  Trivial)
              )
              THEN  Auto
              )\mcdot{}\mcdot{}
  )

---

Home Index