Nuprl Lemma : le-iff-imax

[a,b:ℤ].  uiff(a ≤ b;imax(a;b) b ∈ ℤ)


Proof




Definitions occuring in Statement :  imax: imax(a;b) uiff: uiff(P;Q) uall: [x:A]. B[x] le: A ≤ B int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T imax: imax(a;b) has-value: (a)↓ uimplies: supposing a all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  prop: le: A ≤ B not: ¬A false: False subtype_rel: A ⊆B bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  value-type-has-value int-value-type le_int_wf bool_wf eqtt_to_assert assert_of_le_int le_wf less_than'_wf equal-wf-base int_subtype_base eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf intformnot_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule callbyvalueReduce extract_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis hypothesisEquality because_Cache lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_pairFormation independent_pairEquality lambdaEquality dependent_functionElimination voidElimination axiomEquality applyEquality dependent_pairFormation promote_hyp instantiate cumulativity independent_functionElimination natural_numberEquality int_eqEquality isect_memberEquality voidEquality computeAll baseApply closedConclusion baseClosed

Latex:
\mforall{}[a,b:\mBbbZ{}].    uiff(a  \mleq{}  b;imax(a;b)  =  b)



Date html generated: 2017_04_14-AM-09_13_31
Last ObjectModification: 2017_02_27-PM-03_50_57

Theory : int_2


Home Index