Nuprl Lemma : nat-deq_wf

NatDeq ∈ EqDecider(ℕ)


Proof




Definitions occuring in Statement :  nat-deq: NatDeq deq: EqDecider(T) nat: member: t ∈ T
Definitions unfolded in proof :  deq: EqDecider(T) nat-deq: NatDeq member: t ∈ T uall: [x:A]. B[x] nat: all: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q implies:  Q squash: T le: A ≤ B prop: rev_implies:  Q uiff: uiff(P;Q) uimplies: supposing a so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  iff_wf all_wf assert_wf assert_of_eq_int le_wf equal_wf nat_wf eq_int_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule dependent_set_memberEquality lambdaEquality cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis lambdaFormation independent_pairFormation applyEquality imageMemberEquality baseClosed equalityUniverse levelHypothesis introduction productElimination natural_numberEquality intEquality addLevel allFunctionality impliesFunctionality equalityTransitivity equalitySymmetry independent_isectElimination

Latex:
NatDeq  \mmember{}  EqDecider(\mBbbN{})



Date html generated: 2016_05_14-AM-06_07_00
Last ObjectModification: 2016_01_14-PM-07_31_53

Theory : equality!deciders


Home Index