Nuprl Lemma : fRulefalseE_wf
∀[hypnum:ℕ]. (falseE on hypnum ∈ FOLRule())
Proof
Definitions occuring in Statement : 
fRulefalseE: falseE on hypnum
, 
FOLRule: FOLRule()
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
FOLRule: FOLRule()
, 
fRulefalseE: falseE on hypnum
, 
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, 
istype-nat
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{}[hypnum:\mBbbN{}].  (falseE  on  hypnum  \mmember{}  FOLRule())
Date html generated:
2020_05_20-AM-09_09_58
Last ObjectModification:
2020_01_24-PM-02_32_46
Theory : minimal-first-order-logic
Home
Index