Nuprl Lemma : fix_strict_diverge

f:StrictFun. (fix(f) ~ ⊥)


Proof




Definitions occuring in Statement :  strict-fun: StrictFun bottom: all: x:A. B[x] fix: fix(F) sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T strict-fun: StrictFun
Lemmas referenced :  fix-diverges strict-fun_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin sqequalRule hypothesisEquality hypothesis

Latex:
\mforall{}f:StrictFun.  (fix(f)  \msim{}  \mbot{})



Date html generated: 2016_05_15-PM-10_04_50
Last ObjectModification: 2015_12_27-PM-05_16_42

Theory : bar!type


Home Index