---

Step * 1 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
⊢ 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
BY
{ ProveSqFixpointsLe }

1
.....failed on: 16..... 
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
     (λ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))^j - 1 
      ⊥ 
      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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
⊢ 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,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))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ 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.(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 + 1) 
            s.t@n))
  fi 

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  s  :  Base
3.  ind  :  Base
4.  base  :  Base
5.  mon  :  Base
6.  M  :  Base
\mvdash{}  fix((\mlambda{}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  (\mlambda{}t.(howard-bar-rec  (n  +  1)  s.t@n)))) 
    n 
    s  \mleq{}  fix((\mlambda{}spector-bar-rec,n,s.  if  if  M  n  s  then  0  else  n  +  1  fi    \mleq{}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)  =>
                                                                            \mbot{}
                                                                else  ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))
                                                                fi  )) 
            n 
            s


By

---

Latex:
ProveSqFixpointsLe

---

Home Index