Nuprl Lemma : FOConnective_wf
∀knd:Atom. (FOConnective(knd) ∈ AbstractFOFormula ─→ AbstractFOFormula ─→ AbstractFOFormula)
Proof
Definitions occuring in Statement :
FOConnective: FOConnective(knd),
AbstractFOFormula: AbstractFOFormula,
all: ∀x:A. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
atom: Atom
Lemmas :
eq_atom_wf,
bool_wf,
uiff_transitivity,
equal-wf-base,
atom_subtype_base,
assert_wf,
eqtt_to_assert,
assert_of_eq_atom,
FOSatWith_wf,
FOAssignment_wf,
FOStruct_wf,
AbstractFOFormula_wf,
iff_transitivity,
bnot_wf,
not_wf,
iff_weakening_uiff,
eqff_to_assert,
assert_of_bnot,
or_wf
\mforall{}knd:Atom. (FOConnective(knd) \mmember{} AbstractFOFormula {}\mrightarrow{} AbstractFOFormula {}\mrightarrow{} AbstractFOFormula)
Date html generated:
2015_07_17-AM-07_53_17
Last ObjectModification:
2015_01_27-AM-10_07_20
Home
Index