Nuprl Lemma : primed-class-opt-cases2
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[b:Top]. ∀[e:E].
(Prior(X)?b(e) ~ if first(e) then b loc(e)
if 0 <z #(X(pred(e))) then X(pred(e))
else Prior(X)?b(pred(e))
fi )
Proof
Definitions occuring in Statement :
primed-class-opt: Prior(X)?b,
class-ap: X(e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-first: first(e),
es-pred: pred(e),
es-loc: loc(e),
es-E: E,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
natural_number: $n,
universe: Type,
sqequal: s ~ t,
bag-size: #(bs)
Lemmas :
primed-class-opt-cases
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(Top)]. \mforall{}[b:Top]. \mforall{}[e:E].
(Prior(X)?b(e) \msim{} if first(e) then b loc(e)
if 0 <z \#(X(pred(e))) then X(pred(e))
else Prior(X)?b(pred(e))
fi )
Date html generated:
2015_07_21-PM-02_30_28
Last ObjectModification:
2015_01_27-PM-09_46_31
Home
Index