Nuprl Lemma : imin_ub

[a,b,c:ℤ].  uiff(a ≤ imin(b;c);{(a ≤ b) ∧ (a ≤ c)})


Proof




Definitions occuring in Statement :  imin: imin(a;b) uiff: uiff(P;Q) uall: [x:A]. B[x] guard: {T} le: A ≤ B and: P ∧ Q int:
Definitions unfolded in proof :  guard: {T} imin: imin(a;b) has-value: (a)↓ uall: [x:A]. B[x] member: t ∈ T 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  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top prop: le: A ≤ B bfalse: ff sq_type: SQType(T) bnot: ¬bb assert: b
Lemmas referenced :  value-type-has-value int-value-type le_int_wf bool_wf eqtt_to_assert assert_of_le_int decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf less_than'_wf le_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot ifthenelse_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep callbyvalueReduce cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin intEquality independent_isectElimination hypothesis hypothesisEquality because_Cache lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_pairFormation isect_memberFormation dependent_functionElimination natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality computeAll independent_pairEquality axiomEquality productEquality promote_hyp instantiate cumulativity independent_functionElimination

Latex:
\mforall{}[a,b,c:\mBbbZ{}].    uiff(a  \mleq{}  imin(b;c);\{(a  \mleq{}  b)  \mwedge{}  (a  \mleq{}  c)\})



Date html generated: 2017_04_14-AM-09_14_48
Last ObjectModification: 2017_02_27-PM-03_52_50

Theory : int_2


Home Index