Nuprl Lemma : FOQuantifier_wf
∀[isall:𝔹]. (FOQuantifier(isall) ∈ ℤ ─→ AbstractFOFormula ─→ AbstractFOFormula)
Proof
Definitions occuring in Statement :
FOQuantifier: FOQuantifier(isall),
AbstractFOFormula: AbstractFOFormula,
bool: 𝔹,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
int: ℤ
Lemmas :
bool_wf,
eqtt_to_assert,
all_wf,
FOSatWith_wf,
update-assignment_wf,
FOAssignment_wf,
FOStruct_wf,
AbstractFOFormula_wf,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
bnot_wf,
not_wf,
eqff_to_assert,
assert_of_bnot,
exists_wf
\mforall{}[isall:\mBbbB{}]. (FOQuantifier(isall) \mmember{} \mBbbZ{} {}\mrightarrow{} AbstractFOFormula {}\mrightarrow{} AbstractFOFormula)
Date html generated:
2015_07_17-AM-07_53_18
Last ObjectModification:
2015_01_27-AM-10_07_07
Home
Index