---

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

∀[M,mon,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].
  (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
{ ((UnivCD THENA Auto) THEN SqEqualTopToBase THEN SqequalSqle) }

1
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)

2
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. mon : Base
6. M : Base
⊢ 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) ≤ howard-bar-rec(M;mon;base;ind;n;s)

---

Latex:

---

Latex:
\mforall{}[M,mon,base,ind:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:Top].
    (howard-bar-rec(M;mon;base;ind;n;s) 
    \msim{}  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:
((UnivCD  THENA  Auto)  THEN  SqEqualTopToBase  THEN  SqequalSqle)

---

Home Index