### Nuprl Lemma : bdd-diff_weakening

`∀a,b:ℕ+ ⟶ ℤ.  ((a = b ∈ (ℕ+ ⟶ ℤ)) `` bdd-diff(a;b))`

Proof

Definitions occuring in Statement :  bdd-diff: `bdd-diff(f;g)` nat_plus: `ℕ+` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` guard: `{T}` equiv_rel: `EquivRel(T;x,y.E[x; y])` and: `P ∧ Q` refl: `Refl(T;x,y.E[x; y])`
Lemmas referenced :  bdd-diff-equiv equal_wf nat_plus_wf and_wf bdd-diff_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution isectElimination thin functionEquality hypothesis intEquality functionExtensionality applyEquality hypothesisEquality productElimination dependent_functionElimination hyp_replacement equalitySymmetry sqequalRule dependent_set_memberEquality independent_pairFormation lambdaEquality setElimination rename setEquality

Latex:
\mforall{}a,b:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    ((a  =  b)  {}\mRightarrow{}  bdd-diff(a;b))

Date html generated: 2016_10_26-AM-09_02_40
Last ObjectModification: 2016_07_12-AM-08_12_39

Theory : reals

Home Index