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 THEN RWO "append-nil" THEN Auto)
         )
   }

1
1. Type
2. (T List) ⟶ 𝔹
3. (T List) ⟶ ℙ
4. : ∀s:{s:T List| ↑R[s]} A[s]
5. : ∀s:{s:T List| ¬↑R[s]} ((∀t:T. A[s [t]])  A[s])
6. 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