Nuprl Lemma : rec-combined-loc-class-2-classrel
∀[B,F,X,Y,es,e,v:Top]. (v ∈ F|Loc, X, Y, Prior(self)|(e) ~ v ∈ F|Loc, X, Y, Prior(F|Loc, X, Y, Prior(self)|)|(e))
Proof
Definitions occuring in Statement :
simple-loc-comb-3: F|Loc, X, Y, Z|,
rec-combined-loc-class-2: F|Loc, X, Y, Prior(self)|,
primed-class: Prior(X),
classrel: v ∈ X(e),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Definitions unfolded in proof :
rec-combined-loc-class-2: F|Loc, X, Y, Prior(self)|,
simple-loc-comb-3: F|Loc, X, Y, Z|,
classrel: v ∈ X(e),
simple-loc-comb: F|Loc; Xs|,
select: L[n],
cons: [a / b],
subtract: n - m,
rec-combined-loc-class: f|Loc, X, Prior(self)|,
member: t ∈ T,
uall: ∀[x:A]. B[x]
Latex:
\mforall{}[B,F,X,Y,es,e,v:Top].
(v \mmember{} F|Loc, X, Y, Prior(self)|(e) \msim{} v \mmember{} F|Loc, X, Y, Prior(F|Loc, X, Y, Prior(self)|)|(e))
Date html generated:
2016_05_17-AM-09_27_34
Last ObjectModification:
2015_12_29-PM-04_03_16
Theory : classrel!lemmas
Home
Index