Nuprl Lemma : subtract-wf-bar-int

`∀[x,y:bar(ℤ)].  (x - y ∈ bar(ℤ))`

Proof

Definitions occuring in Statement :  bar: `bar(T)` uall: `∀[x:A]. B[x]` member: `t ∈ T` subtract: `n - m` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` guard: `{T}` or: `P ∨ Q` subtype_rel: `A ⊆r B` all: `∀x:A. B[x]` implies: `P `` Q`
Lemmas referenced :  subtype_bar2 base_wf int_subtype_base value-type_wf subtype_rel_self bar-base subtract-wf-bar subtype_barSqtype_base int-value-type
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin intEquality hypothesis independent_isectElimination independent_pairFormation sqequalRule inrFormation because_Cache hypothesisEquality applyEquality dependent_functionElimination independent_functionElimination axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality

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

Date html generated: 2016_07_08-PM-05_18_53
Last ObjectModification: 2015_12_27-PM-05_17_11

Theory : bar!type

Home Index