Nuprl Lemma : comparison-linear

`∀[T:Type]. ∀cmp:comparison(T). Linorder(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))`

Proof

Definitions occuring in Statement :  cmp-le: `cmp-le(cmp;x;y)` cmp-type: `cmp-type(T;cmp)` comparison: `comparison(T)` linorder: `Linorder(T;x,y.R[x; y])` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` linorder: `Linorder(T;x,y.R[x; y])` and: `P ∧ Q` order: `Order(T;x,y.R[x; y])` connex: `Connex(T;x,y.R[x; y])` member: `t ∈ T` refl: `Refl(T;x,y.E[x; y])` cmp-le: `cmp-le(cmp;x;y)` uimplies: `b supposing a` cmp-type: `cmp-type(T;cmp)` quotient: `x,y:A//B[x; y]` implies: `P `` Q` comparison: `comparison(T)` subtype_rel: `A ⊆r B` sq_type: `SQType(T)` guard: `{T}` le: `A ≤ B` less_than': `less_than'(a;b)` false: `False` not: `¬A` anti_sym: `AntiSym(T;x,y.R[x; y])` prop: `ℙ` trans: `Trans(T;x,y.E[x; y])` true: `True` or: `P ∨ Q` decidable: `Dec(P)` iff: `P `⇐⇒` Q` squash: `↓T` rev_implies: `P `` Q` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)`
Lemmas referenced :  comparison_wf istype-universe cmp-type_wf subtype_base_sq int_subtype_base comparison-reflexive istype-int istype-false cmp-le_wf decidable__cmp-le iff_weakening_equal subtype_rel_self true_wf squash_wf equal_wf comparison-equiv equal-wf-base quotient-member-eq le_wf int_formula_prop_wf int_term_value_minus_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma itermMinus_wf intformle_wf itermConstant_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  Error :lambdaFormation_alt,  independent_pairFormation Error :universeIsType,  cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality hypothesis instantiate isectElimination universeEquality cumulativity intEquality independent_isectElimination pointwiseFunctionalityForEquality sqequalRule pertypeElimination productElimination equalityTransitivity equalitySymmetry Error :inhabitedIsType,  Error :equalityIsType1,  independent_functionElimination Error :productIsType,  Error :equalityIstype,  sqequalBase because_Cache applyEquality setElimination rename baseClosed natural_numberEquality voidElimination unionElimination pointwiseFunctionality imageMemberEquality imageElimination Error :lambdaEquality_alt,  Error :equalityIsType4,  promote_hyp hyp_replacement Error :isect_memberEquality_alt,  int_eqEquality Error :dependent_pairFormation_alt,  approximateComputation Error :inrFormation_alt,  Error :inlFormation_alt,  minusEquality

Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  Linorder(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))

Date html generated: 2019_06_20-PM-01_42_08
Last ObjectModification: 2018_11_22-PM-10_09_55

Theory : list_1

Home Index