### Nuprl Lemma : comparison-trans

`∀[T:Type]. ∀cmp:comparison(T). Trans(T;x,y.0 ≤ (cmp x y))`

Proof

Definitions occuring in Statement :  comparison: `comparison(T)` trans: `Trans(T;x,y.E[x; y])` uall: `∀[x:A]. B[x]` le: `A ≤ B` all: `∀x:A. B[x]` apply: `f a` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` trans: `Trans(T;x,y.E[x; y])` implies: `P `` Q` comparison: `comparison(T)` sq_stable: `SqStable(P)` and: `P ∧ Q` squash: `↓T` prop: `ℙ` le: `A ≤ B` not: `¬A` false: `False` guard: `{T}`
Lemmas referenced :  less_than'_wf comparison_wf le_wf sq_stable__le
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination natural_numberEquality applyEquality hypothesisEquality hypothesis independent_functionElimination productElimination sqequalRule imageMemberEquality baseClosed imageElimination dependent_functionElimination lambdaEquality independent_pairEquality voidElimination axiomEquality equalityTransitivity equalitySymmetry because_Cache universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}cmp:comparison(T).  Trans(T;x,y.0  \mleq{}  (cmp  x  y))

Date html generated: 2016_05_14-PM-02_38_08
Last ObjectModification: 2016_01_15-AM-07_42_07

Theory : list_1

Home Index