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