Nuprl Lemma : fix-not-exception

[G,g:Base].  ¬is-exception(G fix(g)) supposing ∀j:ℕis-exception(G (g^j ⊥)))


Proof




Definitions occuring in Statement :  fun_exp: f^n nat: bottom: is-exception: is-exception(t) uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A apply: a fix: fix(F) base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False is-exception: is-exception(t) all: x:A. B[x] prop: so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: so_apply: x[s]
Lemmas referenced :  base_wf int_subtype_base le_wf set_subtype_base not_wf nat_wf all_wf is-exception_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation thin sqequalHypSubstitution sqequalRule hypothesis exceptionCompactness dependent_functionElimination hypothesisEquality independent_functionElimination voidElimination because_Cache lemma_by_obid isectElimination baseApply closedConclusion baseClosed lambdaEquality applyEquality intEquality natural_numberEquality independent_isectElimination isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[G,g:Base].    \mneg{}is-exception(G  fix(g))  supposing  \mforall{}j:\mBbbN{}.  (\mneg{}is-exception(G  (g\^{}j  \mbot{})))



Date html generated: 2016_05_14-AM-06_09_55
Last ObjectModification: 2016_01_14-PM-07_50_08

Theory : partial_1


Home Index