---

Step * of Lemma pcw-pp-barred-W-decidable

∀[A:Type]. ∀[B:A ⟶ Type].  ∀n:ℕ. ∀s:ℕn ⟶ cw-step(A;a.B[a]).  (Barred(<n, s>) ∨ (¬Barred(<n, s>)))
BY
{ (Auto
   THEN (InstLemma `decidable__pcw-pp-barred` [⌜Unit⌝;⌜λ2p.A⌝;⌜λ2p a.B[a]⌝;⌜so_lambda(p,a,b.⋅)⌝;⌜<n, s>⌝]⋅ THENA Auto)
   THEN Fold `decidable` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].    \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  cw-step(A;a.B[a]).    (Barred(<n,  s>)  \mvee{}  (\mneg{}Barred(<n,  s>)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `decidable\_\_pcw-pp-barred`
              [\mkleeneopen{}Unit\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p  a.B[a]\mkleeneclose{};\mkleeneopen{}so\_lambda(p,a,b.\mcdot{})\mkleeneclose{};\mkleeneopen{}<n,  s>\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `decidable`  0
  THEN  Trivial)

---

Home Index