Nuprl Lemma : natrec-unroll

[g,n:Top].  (letrec f(n)=g[n;f] in g[n;letrec f(n)=g[n;f] in f])


Proof




Definitions occuring in Statement :  natrec: natrec uall: [x:A]. B[x] top: Top so_apply: x[s1;s2] apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T natrec: natrec genrec: genrec
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesis sqequalAxiom lemma_by_obid sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality because_Cache

Latex:
\mforall{}[g,n:Top].    (letrec  f(n)=g[n;f]  in  f  n  \msim{}  g[n;letrec  f(n)=g[n;f]  in  f])



Date html generated: 2016_05_13-PM-04_03_16
Last ObjectModification: 2015_12_26-AM-10_56_04

Theory : int_1


Home Index