---

Step * of Lemma bar_recursion_wf

∀[T:Type]. ∀[R,A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ]. ∀[d:∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R[n;s])].
∀[b:∀n:ℕ. ∀s:ℕn ⟶ T.  (R[n;s] ⇒ A[n;s])]. ∀[i:∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])].
∀[n:ℕ]. ∀[s:ℕn ⟶ T].
  ((∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[n + m;seq-append(n;m;s;alpha)]))
  ⇒ (bar_recursion(d;
                    b;
                    i;
                    n;seq-normalize(n;s)) ∈ A[n;seq-normalize(n;s)]))
BY
{ TACTIC:(Auto
          THEN (Subst ⌜bar_recursion(d;
                                     b;
                                     i;
                                     n;seq-normalize(n;s)) ∈ A[n;seq-normalize(n;s)] ~ (λk,u. bar_recursion(d;
                                                                                              b;
                                                                                              i;
                                                                                              n + k;seq-normalize(n
                                                                                              + k;seq-append(n;k;s;u))))\000C 
                                                                         0 
                                                                         ⊥ ∈ (λk,u. A[n + k;seq-normalize(n
                                                                                    + k;seq-append(n;k;s;u))]) 
                                                                             0 
                                                                             ⊥⌝ 0⋅
                THENA (Reduce 0 THEN RWW "seq-append0 seq-normalize-normalize" 0 THEN Auto THEN AutoSplit)
                )
          ) }

1
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. d : ∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R[n;s])
5. b : ∀n:ℕ. ∀s:ℕn ⟶ T.  (R[n;s] ⇒ A[n;s])
6. i : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. A[n + 1;seq-append(n;1;s;λi.t)]) ⇒ A[n;s])
7. n : ℕ
8. s : ℕn ⟶ T
9. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. R[n + m;seq-append(n;m;s;alpha)])
⊢ (λk,u. bar_recursion(d;b;i;n + k;seq-normalize(n + k;seq-append(n;k;s;u)))) 0 ⊥
  ∈ (λk,u. A[n + k;seq-normalize(n + k;seq-append(n;k;s;u))]) 0 ⊥

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    Dec(R[n;s])].  \mforall{}[b:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
                                                                                                                                                                        (R[n;s]
                                                                                                                                                                        {}\mRightarrow{}  A[n;s])].
\mforall{}[i:\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.    ((\mforall{}t:T.  A[n  +  1;seq-append(n;1;s;\mlambda{}i.t)])  {}\mRightarrow{}  A[n;s])].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  T].
    ((\mforall{}alpha:\mBbbN{}  {}\mrightarrow{}  T.  (\mdownarrow{}\mexists{}m:\mBbbN{}.  R[n  +  m;seq-append(n;m;s;alpha)]))
    {}\mRightarrow{}  (bar\_recursion(d;
                                        b;
                                        i;
                                        n;seq-normalize(n;s))  \mmember{}  A[n;seq-normalize(n;s)]))


By

---

Latex:
TACTIC:(Auto
                THEN  (Subst  \mkleeneopen{}bar\_recursion(d;
                                                                      b;
                                                                      i;
                                                                      n;seq-normalize(n;s))  \mmember{}  A[n;seq-normalize(n;s)] 
                                          \msim{}  (\mlambda{}k,u.  bar\_recursion(d;b;i;n  +  k;seq-normalize(n  +  k;seq-append(n;k;s;u))))  0\000C  \mbot{}
                                              \mmember{}  (\mlambda{}k,u.  A[n  +  k;seq-normalize(n  +  k;seq-append(n;k;s;u))])  0  \mbot{}\mkleeneclose{}  0\mcdot{}
                            THENA  (Reduce  0
                                          THEN  RWW  "seq-append0  seq-normalize-normalize"  0
                                          THEN  Auto
                                          THEN  AutoSplit)
                            )
                )

---

Home Index