Nuprl Lemma : assert-int-deq

`∀[x,y:ℤ].  uiff(↑(IntDeq x y);x = y ∈ ℤ)`

Proof

Definitions occuring in Statement :  int-deq: `IntDeq` assert: `↑b` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` apply: `f a` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` int-deq: `IntDeq` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` prop: `ℙ` subtype_rel: `A ⊆r B` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` deq: `EqDecider(T)`
Lemmas referenced :  equal-wf-base int_subtype_base iff_weakening_uiff assert_wf eq_int_wf assert_of_eq_int assert_witness uiff_wf int-deq_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule independent_pairFormation hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesisEquality applyEquality because_Cache addLevel productElimination independent_isectElimination independent_functionElimination cumulativity instantiate independent_pairEquality isect_memberEquality axiomEquality lambdaEquality setElimination rename equalityTransitivity equalitySymmetry

Latex:
\mforall{}[x,y:\mBbbZ{}].    uiff(\muparrow{}(IntDeq  x  y);x  =  y)

Date html generated: 2019_06_20-PM-00_31_56
Last ObjectModification: 2018_08_24-PM-10_58_42

Theory : equality!deciders

Home Index