Nuprl Lemma : less_wf
∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ]. (if (x) < (y) then a else b ∈ T)
Proof
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
member: t ∈ T,
less: if (a) < (b) then c else d,
int: ℤ,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
less_than: a < b,
and: P ∧ Q,
less_than': less_than'(a;b),
true: True,
squash: ↓T,
top: Top,
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ
Lemmas referenced :
top_wf,
less_than_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesisEquality,
lessCases,
equalityTransitivity,
hypothesis,
equalitySymmetry,
independent_pairFormation,
sqequalHypSubstitution,
isectElimination,
thin,
baseClosed,
natural_numberEquality,
sqequalRule,
imageMemberEquality,
axiomSqEquality,
extract_by_obid,
isect_memberEquality,
because_Cache,
promote_hyp,
voidElimination,
voidEquality,
lambdaFormation,
imageElimination,
productElimination,
axiomEquality,
intEquality,
universeEquality
Latex:
\mforall{}[T:Type]. \mforall{}[a,b:T]. \mforall{}[x,y:\mBbbZ{}]. (if (x) < (y) then a else b \mmember{} T)
Date html generated:
2019_06_20-AM-11_18_55
Last ObjectModification:
2018_08_21-AM-11_05_44
Theory : core_2
Home
Index