Nuprl Lemma : fRuleorI_wf
∀[left:𝔹]. (fRuleorI(left) ∈ FOLRule())
Proof
Definitions occuring in Statement : 
fRuleorI: fRuleorI(left)
, 
FOLRule: FOLRule()
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
FOLRule: FOLRule()
, 
fRuleorI: fRuleorI(left)
, 
eq_atom: x =a y
, 
ifthenelse: if b then t else f fi 
, 
bfalse: ff
, 
btrue: tt
Lemmas referenced : 
ifthenelse_wf, 
eq_atom_wf, 
unit_wf2, 
bool_wf, 
nat_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalRule, 
dependent_pairEquality_alt, 
tokenEquality, 
hypothesisEquality, 
universeIsType, 
thin, 
instantiate, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
hypothesis, 
universeEquality, 
intEquality, 
productEquality, 
voidEquality
Latex:
\mforall{}[left:\mBbbB{}].  (fRuleorI(left)  \mmember{}  FOLRule())
Date html generated:
2020_05_20-AM-09_09_35
Last ObjectModification:
2020_01_22-PM-06_29_13
Theory : minimal-first-order-logic
Home
Index