---

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


1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
     (λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ 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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. is-exception(case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                       of inl() =>
                       ff
                       | inr() =>
                       tt
 of inl() =>
 case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
 | inr() =>
 ind n s 
 (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
11. is-exception(case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
 of inl() =>
 ff
 | inr() =>
 tt)
12. is-exception(if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff)
⊢ case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff of inl() => ff | inr() => tt
   of inl() =>
   case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
   | inr() =>
   ind n s 
   (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                    of inl() =>
                                    ff
                                    | inr() =>
                                    tt
                              of inl() =>
                              case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                              | inr() =>
                              ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ 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.(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 + 1) 
        s.t@n))
BY
{ ExceptionCases (-1) }

1
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
     (λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ 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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. is-exception(case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                       of inl() =>
                       ff
                       | inr() =>
                       tt
 of inl() =>
 case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
 | inr() =>
 ind n s 
 (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
11. is-exception(case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
 of inl() =>
 ff
 | inr() =>
 tt)
12. is-exception(if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff)
13. n ∈ ℤ
14. case M n s of inl() => 0 | inr() => n + 1 ∈ ℤ
⊢ case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff of inl() => ff | inr() => tt
   of inl() =>
   case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
   | inr() =>
   ind n s 
   (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                    of inl() =>
                                    ff
                                    | inr() =>
                                    tt
                              of inl() =>
                              case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                              | inr() =>
                              ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ 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.(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 + 1) 
        s.t@n))

2
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
     (λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ 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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. is-exception(case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                       of inl() =>
                       ff
                       | inr() =>
                       tt
 of inl() =>
 case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
 | inr() =>
 ind n s 
 (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
11. is-exception(case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
 of inl() =>
 ff
 | inr() =>
 tt)
12. is-exception(if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff)
13. n ∈ ℤ
14. is-exception(case M n s of inl() => 0 | inr() => n + 1)
⊢ case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff of inl() => ff | inr() => tt
   of inl() =>
   case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
   | inr() =>
   ind n s 
   (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                    of inl() =>
                                    ff
                                    | inr() =>
                                    tt
                              of inl() =>
                              case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                              | inr() =>
                              ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ 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.(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 + 1) 
        s.t@n))

3
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,mon,M:Base.
     (λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ 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)
4. n : ℕ
5. s : Base
6. ind : Base
7. base : Base
8. mon : Base
9. M : Base
10. is-exception(case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                       of inl() =>
                       ff
                       | inr() =>
                       tt
 of inl() =>
 case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
 | inr() =>
 ind n s 
 (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                  of inl() =>
                                  ff
                                  | inr() =>
                                  tt
                            of inl() =>
                            case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                            | inr() =>
                            ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
11. is-exception(case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
 of inl() =>
 ff
 | inr() =>
 tt)
12. is-exception(if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff)
13. is-exception(n)
⊢ case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff of inl() => ff | inr() => tt
   of inl() =>
   case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
   | inr() =>
   ind n s 
   (λt.(λspector-bar-rec,n,s. case case if (n) < (case M n s of inl() => 0 | inr() => n + 1)  then tt  else ff
                                    of inl() =>
                                    ff
                                    | inr() =>
                                    tt
                              of inl() =>
                              case M n s of inl(x) => let k,p = x in base n s (mon n k s p) | inr(x) => ⊥
                              | inr() =>
                              ind n s (λt.(spector-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ 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.(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 + 1) 
        s.t@n))

---

Latex:

---

Latex:

1.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}n:\mBbbN{}.  \mforall{}s,ind,base,mon,M:Base.
          (\mlambda{}spector-bar-rec,n,s.  case  case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)
                                                                                  then  tt
                                                                                  else  ff
                                                                    of  inl()  =>
                                                                    ff
                                                                    |  inr()  =>
                                                                    tt
                                                        of  inl()  =>
                                                        case  M  n  s
                                                          of  inl(x)  =>
                                                          let  k,p  =  x 
                                                          in  base  n  s  (mon  n  k  s  p)
                                                          |  inr(x)  =>
                                                          \mbot{}
                                                        |  inr()  =>
                                                        ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
            \mbot{} 
            n 
            s  \mleq{}  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)
4.  n  :  \mBbbN{}
5.  s  :  Base
6.  ind  :  Base
7.  base  :  Base
8.  mon  :  Base
9.  M  :  Base
10.  is-exception(case  case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)    then  tt    else  ff
                                              of  inl()  =>
                                              ff
                                              |  inr()  =>
                                              tt
  of  inl()  =>
  case  M  n  s  of  inl(x)  =>  let  k,p  =  x  in  base  n  s  (mon  n  k  s  p)  |  inr(x)  =>  \mbot{}
  |  inr()  =>
  ind  n  s 
  (\mlambda{}t.(\mlambda{}spector-bar-rec,n,s.  case  case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)
                                                                                  then  tt
                                                                                  else  ff
                                                                    of  inl()  =>
                                                                    ff
                                                                    |  inr()  =>
                                                                    tt
                                                        of  inl()  =>
                                                        case  M  n  s
                                                          of  inl(x)  =>
                                                          let  k,p  =  x 
                                                          in  base  n  s  (mon  n  k  s  p)
                                                          |  inr(x)  =>
                                                          \mbot{}
                                                        |  inr()  =>
                                                        ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
            \mbot{} 
            (n  +  1) 
            s.t@n)))
11.  is-exception(case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)    then  tt    else  ff
  of  inl()  =>
  ff
  |  inr()  =>
  tt)
12.  is-exception(if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)    then  tt    else  ff)
\mvdash{}  case  case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)    then  tt    else  ff
                of  inl()  =>
                ff
                |  inr()  =>
                tt
      of  inl()  =>
      case  M  n  s  of  inl(x)  =>  let  k,p  =  x  in  base  n  s  (mon  n  k  s  p)  |  inr(x)  =>  \mbot{}
      |  inr()  =>
      ind  n  s 
      (\mlambda{}t.(\mlambda{}spector-bar-rec,n,s.  case  case  if  (n)  <  (case  M  n  s  of  inl()  =>  0  |  inr()  =>  n  +  1)
                                                                                      then  tt
                                                                                      else  ff
                                                                        of  inl()  =>
                                                                        ff
                                                                        |  inr()  =>
                                                                        tt
                                                            of  inl()  =>
                                                            case  M  n  s
                                                              of  inl(x)  =>
                                                              let  k,p  =  x 
                                                              in  base  n  s  (mon  n  k  s  p)
                                                              |  inr(x)  =>
                                                              \mbot{}
                                                            |  inr()  =>
                                                            ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
                \mbot{} 
                (n  +  1) 
                s.t@n))  \mleq{}  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.(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  +  1) 
                s.t@n))


By

---

Latex:
ExceptionCases  (-1)

---

Home Index