Nuprl Lemma : int-minus-comparison-inc_wf

[T:Type]. ∀[f:T ⟶ ℤ].  (int-minus-comparison-inc(f) ∈ comparison(T))


Proof




Definitions occuring in Statement :  int-minus-comparison-inc: int-minus-comparison-inc(f) comparison: comparison(T) uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] int: universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T int-minus-comparison-inc: int-minus-comparison-inc(f) comparison: comparison(T) and: P ∧ Q cand: c∧ B all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top prop: uiff: uiff(P;Q) le: A ≤ B so_lambda: λ2x.t[x] so_apply: x[s]
Lemmas referenced :  equal-wf-T-base all_wf le_wf int_formula_prop_le_lemma intformle_wf decidable__le equal_wf false_wf int_term_value_constant_lemma int_formula_prop_and_lemma itermConstant_wf intformand_wf subtract-is-int-iff int_formula_prop_wf int_term_value_minus_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma itermMinus_wf itermVar_wf itermSubtract_wf intformeq_wf intformnot_wf satisfiable-full-omega-tt decidable__equal_int subtract_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut dependent_set_memberEquality lambdaEquality lemma_by_obid sqequalHypSubstitution isectElimination thin applyEquality hypothesisEquality hypothesis sqequalRule lambdaFormation dependent_functionElimination because_Cache unionElimination natural_numberEquality independent_isectElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll independent_pairFormation pointwiseFunctionality rename equalityTransitivity equalitySymmetry promote_hyp baseApply closedConclusion baseClosed productElimination productEquality cumulativity minusEquality functionEquality axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}].    (int-minus-comparison-inc(f)  \mmember{}  comparison(T))



Date html generated: 2016_05_14-PM-02_36_34
Last ObjectModification: 2016_01_15-AM-07_43_01

Theory : list_1


Home Index