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