Nuprl Lemma : exception-name_wf
∀[n:Atom2]. ∀[t:Value() ⋃ Exception(n;Top)]. (exception-name(t;n) ∈ 𝔹)
Proof
Definitions occuring in Statement :
exception-name: exception-name(e;n),
Value: Value(),
Exception: Exception(n;T),
atom: Atom$n,
b-union: A ⋃ B,
bool: 𝔹,
uall: ∀[x:A]. B[x],
top: Top,
member: t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
Exception: Exception(n;T),
prop: ℙ,
exception-name: exception-name(e;n),
Value: Value(),
pi2: snd(t),
ifthenelse: if b then t else f fi ,
unit: Unit,
bool: 𝔹,
tunion: ⋃x:A.B[x],
b-union: A ⋃ B,
has-value: (a)↓,
implies: P ⇒ Q,
all: ∀x:A. B[x],
or: P ∨ Q,
exception-with-name: exception-with-name(n;t),
subtype_rel: A ⊆r B,
mono: mono(T),
cand: A c∧ B,
exists: ∃x:A. B[x],
is-above: is-above(T;a;z)
Lemmas referenced :
top_wf,
Exception_wf,
Value_wf,
b-union_wf,
assert_wf,
band_wf,
has-value-implies-dec-isaxiom-2,
bfalse_wf,
btrue_wf,
has-value-implies-dec-isint-2,
bool-mono,
atom2_subtype_base,
sqle_wf_base,
is-exception_wf,
has-value_wf_base
Rules used in proof :
atomnEquality,
because_Cache,
Error :isect_memberEquality_alt,
hypothesisEquality,
thin,
isectElimination,
extract_by_obid,
Error :universeIsType,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
sqequalRule,
hypothesis,
sqequalHypSubstitution,
cut,
introduction,
Error :isect_memberFormation_alt,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
rename,
setElimination,
equalityElimination,
unionElimination,
productElimination,
imageElimination,
tryReduceValue,
atomn_eqReduceTrueSq,
independent_functionElimination,
dependent_functionElimination,
baseClosed,
isintReduceTrue,
applyEquality,
closedConclusion,
baseApply,
Error :inhabitedIsType,
Error :equalityIsType4,
Error :productIsType,
sqleReflexivity,
sqleRule,
divergentSqle,
independent_pairFormation,
Error :dependent_pairFormation_alt,
natural_numberEquality
Latex:
\mforall{}[n:Atom2]. \mforall{}[t:Value() \mcup{} Exception(n;Top)]. (exception-name(t;n) \mmember{} \mBbbB{})
Date html generated:
2019_06_20-PM-00_28_33
Last ObjectModification:
2018_10_15-PM-10_46_04
Theory : subtype_1
Home
Index