---

Step * 1 1 1 2 of Lemma decidable-bar-rec-equal-spector


1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
     (λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                    then case dec n s of inl(r) => base n s r | inr(x) => ⊥
                                    else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                    fi )) 
          n 
          s)
4. n : ℕ@i
5. s : Base@i
6. ind : Base@i
7. base : Base@i
8. dec : Base@i
9. is-exception(case dec n s
 of inl(r) =>
 base n s r
 | inr(x) =>
 ind n s 
 (λt.(λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
⊢ case dec n s
   of inl(r) =>
   base n s r
   | inr(x) =>
   ind n s 
   (λt.(λdecidable-bar-rec,n,s. case dec n s
                                of inl(r) =>
                                base n s r
                                | inr(x) =>
                                ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ if if dec n s then 0 else n + 1 fi  ≤z n
  then case dec n s of inl(r) => base n s r | inr(x) => ⊥
  else ind n s 
       (λt.(fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                      then case dec n s of inl(r) => base n s r | inr(x) => ⊥
                                      else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                      fi )) 
            (n + 1) 
            s.t@n))
  fi 
BY
{ ExceptionCases (-1) }

1
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
     (λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                    then case dec n s of inl(r) => base n s r | inr(x) => ⊥
                                    else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                    fi )) 
          n 
          s)
4. n : ℕ@i
5. s : Base@i
6. ind : Base@i
7. base : Base@i
8. dec : Base@i
9. is-exception(case dec n s
 of inl(r) =>
 base n s r
 | inr(x) =>
 ind n s 
 (λt.(λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
10. dec n s ∈ Top + Top
⊢ case dec n s
   of inl(r) =>
   base n s r
   | inr(x) =>
   ind n s 
   (λt.(λdecidable-bar-rec,n,s. case dec n s
                                of inl(r) =>
                                base n s r
                                | inr(x) =>
                                ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ if if dec n s then 0 else n + 1 fi  ≤z n
  then case dec n s of inl(r) => base n s r | inr(x) => ⊥
  else ind n s 
       (λt.(fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                      then case dec n s of inl(r) => base n s r | inr(x) => ⊥
                                      else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                      fi )) 
            (n + 1) 
            s.t@n))
  fi 

2
1. j : ℤ
2. 0 < j
3. ∀n:ℕ. ∀s,ind,base,dec:Base.
     (λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      n 
      s ≤ fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                    then case dec n s of inl(r) => base n s r | inr(x) => ⊥
                                    else ind n s (λt.(spector-bar-rec (n + 1) s.t@n))
                                    fi )) 
          n 
          s)
4. n : ℕ@i
5. s : Base@i
6. ind : Base@i
7. base : Base@i
8. dec : Base@i
9. is-exception(case dec n s
 of inl(r) =>
 base n s r
 | inr(x) =>
 ind n s 
 (λt.(λdecidable-bar-rec,n,s. case dec n s
                              of inl(r) =>
                              base n s r
                              | inr(x) =>
                              ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
      ⊥ 
      (n + 1) 
      s.t@n)))
10. is-exception(dec n s)
⊢ case dec n s
   of inl(r) =>
   base n s r
   | inr(x) =>
   ind n s 
   (λt.(λdecidable-bar-rec,n,s. case dec n s
                                of inl(r) =>
                                base n s r
                                | inr(x) =>
                                ind n s (λt.(decidable-bar-rec (n + 1) s.t@n))^j - 1 
        ⊥ 
        (n + 1) 
        s.t@n)) ≤ if if dec n s then 0 else n + 1 fi  ≤z n
  then case dec n s of inl(r) => base n s r | inr(x) => ⊥
  else ind n s 
       (λt.(fix((λspector-bar-rec,n,s. if if dec n s then 0 else n + 1 fi  ≤z n
                                      then case dec n s of inl(r) => base n s r | 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.  j  :  \mBbbZ{}
2.  0  <  j
3.  \mforall{}n:\mBbbN{}.  \mforall{}s,ind,base,dec:Base.
          (\mlambda{}decidable-bar-rec,n,s.  case  dec  n  s
                                                            of  inl(r)  =>
                                                            base  n  s  r
                                                            |  inr(x)  =>
                                                            ind  n  s  (\mlambda{}t.(decidable-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
            \mbot{} 
            n 
            s  \mleq{}  fix((\mlambda{}spector-bar-rec,n,s.  if  if  dec  n  s  then  0  else  n  +  1  fi    \mleq{}z  n
                                                                        then  case  dec  n  s  of  inl(r)  =>  base  n  s  r  |  inr(x)  =>  \mbot{}
                                                                        else  ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))
                                                                        fi  )) 
                    n 
                    s)
4.  n  :  \mBbbN{}@i
5.  s  :  Base@i
6.  ind  :  Base@i
7.  base  :  Base@i
8.  dec  :  Base@i
9.  is-exception(case  dec  n  s
  of  inl(r)  =>
  base  n  s  r
  |  inr(x)  =>
  ind  n  s 
  (\mlambda{}t.(\mlambda{}decidable-bar-rec,n,s.  case  dec  n  s
                                                            of  inl(r)  =>
                                                            base  n  s  r
                                                            |  inr(x)  =>
                                                            ind  n  s  (\mlambda{}t.(decidable-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
            \mbot{} 
            (n  +  1) 
            s.t@n)))
\mvdash{}  case  dec  n  s
      of  inl(r)  =>
      base  n  s  r
      |  inr(x)  =>
      ind  n  s 
      (\mlambda{}t.(\mlambda{}decidable-bar-rec,n,s.  case  dec  n  s
                                                                of  inl(r)  =>
                                                                base  n  s  r
                                                                |  inr(x)  =>
                                                                ind  n  s  (\mlambda{}t.(decidable-bar-rec  (n  +  1)  s.t@n))\^{}j  -  1 
                \mbot{} 
                (n  +  1) 
                s.t@n))  \mleq{}  if  if  dec  n  s  then  0  else  n  +  1  fi    \mleq{}z  n
    then  case  dec  n  s  of  inl(r)  =>  base  n  s  r  |  inr(x)  =>  \mbot{}
    else  ind  n  s 
              (\mlambda{}t.(fix((\mlambda{}spector-bar-rec,n,s.  if  if  dec  n  s  then  0  else  n  +  1  fi    \mleq{}z  n
                                                                            then  case  dec  n  s  of  inl(r)  =>  base  n  s  r  |  inr(x)  =>  \mbot{}
                                                                            else  ind  n  s  (\mlambda{}t.(spector-bar-rec  (n  +  1)  s.t@n))
                                                                            fi  )) 
                        (n  +  1) 
                        s.t@n))
    fi 


By

---

Latex:
ExceptionCases  (-1)

---

Home Index