Step
*
of Lemma
prior-val-pred
∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[e:E].
(X)' es e ~ if pred(e) ∈b X then {X(pred(e))} else (X)' es pred(e) fi supposing ¬↑first(e)
BY
{ (InstLemma `prior-val-cases` []
THEN RepeatFor 4 (ParallelLast')
THEN (D 0 THENA Auto)
THEN SplitOnHypITE -2
THEN Auto) }
Latex:
Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(Top)]. \mforall{}[e:E].
(X)' es e \msim{} if pred(e) \mmember{}\msubb{} X then \{X(pred(e))\} else (X)' es pred(e) fi supposing \mneg{}\muparrow{}first(e)
By
Latex:
(InstLemma `prior-val-cases` []
THEN RepeatFor 4 (ParallelLast')
THEN (D 0 THENA Auto)
THEN SplitOnHypITE -2
THEN Auto)
Home
Index