`∀x,x',y,y':ℕ+ ⟶ ℤ.  (bdd-diff(x;x') `` bdd-diff(y;y') `` bdd-diff(reg-seq-add(x;y);reg-seq-add(x';y')))`

Proof

Definitions occuring in Statement :  reg-seq-add: `reg-seq-add(x;y)` bdd-diff: `bdd-diff(f;g)` nat_plus: `ℕ+` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` and: `P ∧ Q` cand: `A c∧ B` length: `||as||` list_ind: list_ind cons: `[a / b]` nil: `[]` it: `⋅` prop: `ℙ` top: `Top` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` sq_type: `SQType(T)` guard: `{T}` select: `L[n]` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` subtract: `n - m` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` squash: `↓T` reg-seq-add: `reg-seq-add(x;y)` true: `True` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` nat_plus: `ℕ+`
Lemmas referenced :  reg-seq-list-add_functionality_wrt_bdd-diff cons_wf nat_plus_wf nil_wf length_wf int_seg_wf bdd-diff_wf length_of_cons_lemma length_of_nil_lemma decidable__equal_int subtype_base_sq int_subtype_base int_seg_properties int_seg_subtype false_wf int_seg_cases satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf squash_wf true_wf equal_wf reg-seq-list-add-as-l_sum iff_weakening_equal map_cons_lemma map_nil_lemma l_sum_cons_lemma l_sum_nil_lemma nat_plus_properties less_than_wf intformnot_wf intformeq_wf itermAdd_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination functionEquality hypothesis intEquality functionExtensionality applyEquality hypothesisEquality independent_functionElimination sqequalRule independent_pairFormation natural_numberEquality isect_memberEquality voidElimination voidEquality setElimination rename unionElimination instantiate cumulativity independent_isectElimination because_Cache equalityTransitivity equalitySymmetry hypothesis_subsumption addEquality productElimination dependent_pairFormation lambdaEquality int_eqEquality computeAll hyp_replacement imageElimination universeEquality imageMemberEquality baseClosed dependent_set_memberEquality

Latex:
\mforall{}x,x',y,y':\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.