Nuprl Lemma : subtract-wf-partial

[x,y:partial(Base)].  (x y ∈ partial(ℤ))


Proof




Definitions occuring in Statement :  partial: partial(T) uall: [x:A]. B[x] member: t ∈ T subtract: m int: base: Base
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a subtype_rel: A ⊆B subtract: m has-value: (a)↓ and: P ∧ Q uiff: uiff(P;Q) prop: not: ¬A implies:  Q false: False squash: T
Lemmas referenced :  partial-not-exception base_wf partial_wf is-exception_wf minus-is-int-iff subtract_wf int-value-type base-member-partial partial-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination sqequalRule baseApply closedConclusion baseClosed hypothesisEquality applyEquality because_Cache callbyvalueAdd productElimination axiomEquality equalityTransitivity equalitySymmetry lambdaFormation isect_memberEquality addExceptionCases minusExceptionCases independent_functionElimination voidElimination imageElimination imageMemberEquality

Latex:
\mforall{}[x,y:partial(Base)].    (x  -  y  \mmember{}  partial(\mBbbZ{}))



Date html generated: 2016_05_14-AM-06_10_27
Last ObjectModification: 2016_01_14-PM-07_50_16

Theory : partial_1


Home Index