Step
*
1
of Lemma
loop-class-state_wf
.....assertion.....
1. Info : Type
2. B : Type
3. X : EClass(B ─→ B)
4. init : Id ─→ bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. ∀e1:E. ((e1 < e)
⇒ (loop-class-state(X;init) es e1 ∈ bag(B)))
⊢ Prior(loop-class-state(X;init))?init(e) ∈ bag(B)
BY
{ (RepUR ``primed-class-opt class-ap`` 0
THEN (GenConclAtAddr [2;1]
THENA (Try (BLemma `es-local-pred_wf2`)
THEN Reduce 0
THEN Auto
THEN GenConclAtAddrType ⌈bag(B)⌉ [2;1]⋅
THEN Try (BackThruSomeHyp)
THEN Auto)
)
THEN DVar `v'
THEN Reduce 0
THEN Try ((DVar `x' THEN BackThruSomeHyp))
THEN Auto) }
Latex:
Latex:
.....assertion.....
1. Info : Type
2. B : Type
3. X : EClass(B {}\mrightarrow{} B)
4. init : Id {}\mrightarrow{} bag(B)
5. es : EO+(Info)@i'
6. e : E@i
7. \mforall{}e1:E. ((e1 < e) {}\mRightarrow{} (loop-class-state(X;init) es e1 \mmember{} bag(B)))
\mvdash{} Prior(loop-class-state(X;init))?init(e) \mmember{} bag(B)
By
Latex:
(RepUR ``primed-class-opt class-ap`` 0
THEN (GenConclAtAddr [2;1]
THENA (Try (BLemma `es-local-pred\_wf2`)
THEN Reduce 0
THEN Auto
THEN GenConclAtAddrType \mkleeneopen{}bag(B)\mkleeneclose{} [2;1]\mcdot{}
THEN Try (BackThruSomeHyp)
THEN Auto)
)
THEN DVar `v'
THEN Reduce 0
THEN Try ((DVar `x' THEN BackThruSomeHyp))
THEN Auto)
Home
Index