Nuprl Lemma : order-type-less-transitive-ext
Trans(WFO{i:l}();x,y.order-type-less() x y)
Proof
Definitions occuring in Statement :
WFO: WFO{i:l}(),
order-type-less: order-type-less(),
trans: Trans(T;x,y.E[x; y]),
apply: f a
Definitions unfolded in proof :
member: t ∈ T,
spreadn: spread4,
spreadn: spread3,
compose: f o g,
ot-less-trans: ot-less-trans(),
order-type-less-transitive
Lemmas referenced :
order-type-less-transitive
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
Trans(WFO\{i:l\}();x,y.order-type-less() x y)
Date html generated:
2018_05_21-PM-07_01_51
Last ObjectModification:
2018_05_19-PM-04_43_52
Theory : general
Home
Index