Nuprl Lemma : ml_apply-sqle
∀[f,x:Base]. f(x) ≤ f x supposing ¬is-exception(f(x))
Proof
Definitions occuring in Statement :
ml_apply: f(x),
is-exception: is-exception(t),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
not: ¬A,
apply: f a,
base: Base,
sqle: s ≤ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
ml_apply: f(x),
not: ¬A,
implies: P ⇒ Q,
false: False,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
callbyvalueall: callbyvalueall,
has-valueall: has-valueall(a),
has-value: (a)↓
Lemmas referenced :
has-value_wf_base,
is-exception_wf,
not_wf,
base_wf,
has-valueall-if-has-value-callbyvalueall,
evalall-sqequal
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
divergentSqle,
sqequalHypSubstitution,
independent_functionElimination,
thin,
hypothesis,
voidElimination,
extract_by_obid,
isectElimination,
sqequalRule,
baseApply,
closedConclusion,
baseClosed,
hypothesisEquality,
axiomSqleEquality,
isect_memberEquality,
because_Cache,
equalityTransitivity,
equalitySymmetry,
independent_isectElimination,
callbyvalueReduce,
sqleReflexivity
Latex:
\mforall{}[f,x:Base]. f(x) \mleq{} f x supposing \mneg{}is-exception(f(x))
Date html generated:
2017_09_29-PM-05_50_48
Last ObjectModification:
2017_05_22-PM-01_46_39
Theory : ML
Home
Index