### Nuprl Lemma : howard-bar-rec-equal-decidable

`∀[M,mon,base,ind:Top]. ∀[n:ℕ]. ∀[s:Top].`
`  (howard-bar-rec(M;mon;base;ind;n;s) ~ decidable-bar-rec(M;λn,s,r. let k,p = r in base n s (mon n k s p);ind;n;s))`

Proof

Definitions occuring in Statement :  howard-bar-rec: `howard-bar-rec(M;mon;base;ind;n;s)` decidable-bar-rec: `decidable-bar-rec(dec;base;ind;n;s)` nat: `ℕ` uall: `∀[x:A]. B[x]` top: `Top` apply: `f a` lambda: `λx.A[x]` spread: spread def sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` howard-bar-rec: `howard-bar-rec(M;mon;base;ind;n;s)` decidable-bar-rec: `decidable-bar-rec(dec;base;ind;n;s)`
Lemmas referenced :  top_wf nat_wf
Rules used in proof :  hypothesisEquality thin isectElimination isect_memberEquality sqequalHypSubstitution sqequalAxiom introduction isect_memberFormation because_Cache hypothesis lemma_by_obid cut sqequalRule sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[M,mon,base,ind:Top].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:Top].
(howard-bar-rec(M;mon;base;ind;n;s)  \msim{}  decidable-bar-rec(M;\mlambda{}n,s,r.  let  k,p  =  r
in  base  n  s  (mon  n  k  s  p);ind;n;\000Cs))

Date html generated: 2016_05_19-PM-00_08_20
Last ObjectModification: 2016_05_18-PM-02_16_04

Theory : continuity

Home Index