Nuprl Rule : exceptionApplyCases
This rule proved as lemma rule_apply_exception_cases_true in file rules/rules_apply_exception_cases_true.v
at https://github.com/vrahli/NuprlInCoq
H
⊢ ↓(exception(⊥; ⊥) ≤ f)
∨ (f ~ λx.(f x))
∨ (⋂x:Base. ⋂z:(x)↓. if x is an integer then True else f x ≤ ⊥) ext islambda(f)
BY exceptionApplyCases a ()
x ≠ z
x,z can not occur free in f
H ⊢ exception(⊥; ⊥) ≤ f a
H ⊢ f ∈ Base
Definitions occuring in rule :
squash: ↓T,
or: P ∨ Q,
sqequal: s ~ t,
lambda: λx.A[x],
isect: ⋂x:A. B[x],
has-value: (a)↓,
isint: isint def,
true: True,
islambda: if z is lambda then a otherwise b,
btrue: tt,
bfalse: ff,
sqle: s ≤ t,
bottom: ⊥,
apply: f a,
member: t ∈ T,
base: Base,
axiom: Ax
Latex:
H
\mvdash{} \mdownarrow{}(exception(\mbot{}; \mbot{}) \mleq{} f)
\mvee{} (f \msim{} \mlambda{}x.(f x))
\mvee{} (\mcap{}x:Base. \mcap{}z:(x)\mdownarrow{}. if x is an integer then True else f x \mleq{} \mbot{}) ext islambda(f)
BY exceptionApplyCases a ()
x \mneq{} z
x,z can not occur free in f
H \mvdash{} exception(\mbot{}; \mbot{}) \mleq{} f a
H \mvdash{} f \mmember{} Base
Date html generated:
2019_06_20-PM-04_12_09
Last ObjectModification:
2016_07_08-PM-03_48_58
Theory : rules
Home
Index