---

Step * of Lemma bbar-recursion_wf

∀[T:Type]. ∀[R:(T List) ⟶ 𝔹]. ∀[A:(T List) ⟶ ℙ]. ∀[b:∀s:{s:T List| ↑R[s]} . A[s]]. ∀[i:∀s:{s:T List| ¬↑R[s]} 
                                                                                          ((∀t:T. A[s @ [t]]) ⇒ A[s])].
∀[s:T List].
  ((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[s @ map(alpha;upto(n))]))) ⇒ (bbar-recursion(R;b;i;s) ∈ A[s]))
BY
{ (Auto
   THEN (Subst ⌜bbar-recursion(R;
                               b;
                               i;
                               s) ∈ A[s] ~ (λx.bbar-recursion(R;b;i;s @ x)) [] ∈ (λx.A[s @ x]) []⌝ 0⋅
         THENA (Reduce 0 THEN RWO "append-nil" 0 THEN Auto)
         )
   ) }

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

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Subst  \mkleeneopen{}bbar-recursion(R;
                                                          b;
                                                          i;
                                                          s)  \mmember{}  A[s]  \msim{}  (\mlambda{}x.bbar-recursion(R;b;i;s  @  x))  []  \mmember{}  (\mlambda{}x.A[s  @  x])  []\mkleeneclose{}  0\mcdot{}
              THENA  (Reduce  0  THEN  RWO  "append-nil"  0  THEN  Auto)
              )
  )

---

Home Index