Nuprl Lemma : no-halt-decider

¬(∃h:partial(ℤ) ⟶ 𝔹(h tt ∧ h ⊥ ff))


Proof




Definitions occuring in Statement :  partial: partial(T) bottom: bfalse: ff btrue: tt bool: 𝔹 exists: x:A. B[x] not: ¬A and: P ∧ Q apply: a function: x:A ⟶ B[x] natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False prop: exists: x:A. B[x] and: P ∧ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt sq_type: SQType(T) guard: {T} ifthenelse: if then else fi  bfalse: ff
Lemmas referenced :  bottom_diverge base-member-partial int-value-type has-value_wf_base not-is-exception-bottom fixpoint-induction-bottom partial_wf int-mono ifthenelse_wf exists_wf bool_wf equal-wf-T-base inclusion-partial subtype_base_sq bool_subtype_base btrue_neq_bfalse equal_wf
Rules used in proof :  cut introduction extract_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin intEquality independent_isectElimination hypothesis baseClosed isect_memberFormation independent_functionElimination voidElimination sqequalRule axiomEquality equalityTransitivity equalitySymmetry lambdaFormation productElimination because_Cache lambdaEquality hypothesisEquality applyEquality functionExtensionality natural_numberEquality functionEquality productEquality unionElimination equalityElimination addLevel instantiate cumulativity dependent_functionElimination levelHypothesis

Latex:
\mneg{}(\mexists{}h:partial(\mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  (h  0  =  tt  \mwedge{}  h  \mbot{}  =  ff))



Date html generated: 2017_04_14-AM-07_40_55
Last ObjectModification: 2017_02_27-PM-03_12_40

Theory : partial_1


Home Index