Nuprl Lemma : maybe-new-local_wf
∀[me,s:Name]. ∀[avoid:Name List].  (maybe-new-local(me;s;avoid) ∈ Name)
Proof
Definitions occuring in Statement : 
maybe-new-local: maybe-new-local(me;s;avoid)
, 
name: Name
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
maybe-new-local: maybe-new-local(me;s;avoid)
, 
name: Name
, 
subtype_rel: A ⊆r B
, 
prop: ℙ
Latex:
\mforall{}[me,s:Name].  \mforall{}[avoid:Name  List].    (maybe-new-local(me;s;avoid)  \mmember{}  Name)
Date html generated:
2016_05_17-AM-11_30_52
Last ObjectModification:
2015_12_29-PM-06_50_07
Theory : event-logic-applications
Home
Index