---

Step * 1 of Lemma howard-bar-rec-equal-spector


1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
⊢ howard-bar-rec(M;mon;base;ind;n;s) ≤ spector-bar-rec(λn,s. if M n s then 0 else n + 1 fi ;λn,s. case M n s
                                                                                              of inl(x) =>
                                                                                              let k,p = x 
                                                                                              in base n s (mon n k s p)
                                                                                              | inr(x) =>
                                                                                              ⊥;ind;n;s)
BY
{ RepUR ``howard-bar-rec spector-bar-rec`` 0 }

1
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
⊢ fix((λhoward-bar-rec,n,s. case M n s
                            of inl(x) =>
                            let k,p = x 
                            in base n s (mon n k s p)
                            | inr(x) =>
                            ind n s (λt.(howard-bar-rec (n + 1) s.t@n)))) 
  n 
  s ≤ fix((λspector-bar-rec,n,s. if if M n s then 0 else n + 1 fi  ≤z n
                                then case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                                else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                fi )) 
      n 
      s

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  s  :  Base
3.  ind  :  Base
4.  base  :  Base
5.  mon  :  Base
6.  M  :  Base
\mvdash{}  howard-bar-rec(M;mon;base;ind;n;s) 
    \mleq{}  spector-bar-rec(\mlambda{}n,s.  if  M  n  s  then  0  else  n  +  1  fi  ;\mlambda{}n,s.  case  M  n  s
                                                                                                                      of  inl(x)  =>
                                                                                                                      let  k,p  =  x 
                                                                                                                      in  base  n  s  (mon  n  k  s  p)
                                                                                                                      |  inr(x)  =>
                                                                                                                      \mbot{};ind;n;s)


By

---

Latex:
RepUR  ``howard-bar-rec  spector-bar-rec``  0

---

Home Index