Nuprl Lemma : mRuleexistsE_wf
∀[hypnum:ℕ]. ∀[var:ℤ].  (existsE on hypnum with var ∈ mFOLRule())
Proof
Definitions occuring in Statement : 
mRuleexistsE: existsE on hypnum with var
, 
mFOLRule: mFOLRule()
, 
nat: ℕ
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
int: ℤ
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
mFOLRule: mFOLRule()
, 
mRuleexistsE: existsE on hypnum with var
, 
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-int, 
istype-nat
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
cut, 
sqequalRule, 
dependent_pairEquality_alt, 
tokenEquality, 
hypothesisEquality, 
inhabitedIsType, 
universeIsType, 
thin, 
instantiate, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
hypothesis, 
universeEquality, 
intEquality, 
productEquality, 
voidEquality
Latex:
\mforall{}[hypnum:\mBbbN{}].  \mforall{}[var:\mBbbZ{}].    (existsE  on  hypnum  with  var  \mmember{}  mFOLRule())
Date html generated:
2020_05_20-AM-09_09_13
Last ObjectModification:
2020_01_22-PM-04_58_49
Theory : minimal-first-order-logic
Home
Index