Nuprl Lemma : mk_mFOLSequentRule_wf
∀[s:mFOL-sequent()]. ∀[r:mFOLRule()]. (sBY r ∈ mFOL-sequent() × mFOLRule())
Proof
Definitions occuring in Statement :
mk_mFOLSequentRule: mk_mFOLSequentRule,
mFOL-sequent: mFOL-sequent(),
mFOLRule: mFOLRule(),
uall: ∀[x:A]. B[x],
member: t ∈ T,
product: x:A × B[x]
Lemmas :
mFOLRule_wf,
mFOL-sequent_wf
\mforall{}[s:mFOL-sequent()]. \mforall{}[r:mFOLRule()]. (sBY r \mmember{} mFOL-sequent() \mtimes{} mFOLRule())
Date html generated:
2015_07_17-AM-07_56_48
Last ObjectModification:
2015_01_27-AM-10_05_13
Home
Index