---

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

∀[dec,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].
  (decidable-bar-rec(dec;base;ind;n;s) ~ spector-bar-rec(λn,s. if dec n s then 0 else n + 1 fi ;λn,s. case dec n s
                                                                                                  of inl(r) =>
                                                                                                  base n s r
                                                                                                  | 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. dec : Base
⊢ decidable-bar-rec(dec;base;ind;n;s) ≤ spector-bar-rec(λn,s. if dec n s then 0 else n + 1 fi ;λn,s. case dec n s
                                                                                                 of inl(r) =>
                                                                                                 base n s r
                                                                                                 | inr(x) =>
                                                                                                 ⊥;ind;n;s)

2
1. n : ℕ
2. s : Base
3. ind : Base
4. base : Base
5. dec : Base
⊢ spector-bar-rec(λn,s. if dec n s then 0 else n + 1 fi ;λn,s. case dec n s of inl(r) => base n s r | inr(x) => ⊥;ind;n;\000Cs) 
  ≤ decidable-bar-rec(dec;base;ind;n;s)

---

Latex:

---

Latex:
\mforall{}[dec,base,ind:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:Top].
    (decidable-bar-rec(dec;base;ind;n;s) 
    \msim{}  spector-bar-rec(\mlambda{}n,s.  if  dec  n  s  then  0  else  n  +  1  fi  ;\mlambda{}n,s.  case  dec  n  s
                                                                                                                          of  inl(r)  =>
                                                                                                                          base  n  s  r
                                                                                                                          |  inr(x)  =>
                                                                                                                          \mbot{};ind;n;s))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  SqEqualTopToBase  THEN  SqequalSqle)

---

Home Index