---

Step * 1 1 1 1 1 1 1 1 of Lemma base-process-class-program_wf


1. Info : Type
2. T : Type
3. loc : Id
4. X : EClass(T)
5. P : Id ─→ hdataflow(Info;T)
6. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(T))
7. ms' : Info List@i
8. v : Info@i
⊢ (snd(P loc*(firstn(||ms' @ [v]|| - 1;ms' @ [v]))(if ||ms' @ [v]|| - 1 <z ||ms' @ [v]||
then ms' @ [v][||ms' @ [v]|| - 1]
else hd(ms' @ [v])
fi )))
= (snd(P loc*(ms')(v)))
∈ bag(T)
BY
{ ((RWO "length-append" 0 THENA Auto) THEN Reduce 0 THEN (RWO "firstn-append" 0 THENA Auto) THEN AutoSplit) }

1
1. Info : Type
2. T : Type
3. loc : Id
4. X : EClass(T)
5. P : Id ─→ hdataflow(Info;T)
6. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(P loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(T))
7. ms' : Info List@i
8. v : Info@i
9. ((||ms'|| + 1) - 1) ≤ ||ms'||
⊢ (snd(P loc*(firstn((||ms'|| + 1) - 1;ms'))(if (||ms'|| + 1) - 1 <z ||ms'|| + 1
then ms' @ [v][(||ms'|| + 1) - 1]
else hd(ms' @ [v])
fi )))
= (snd(P loc*(ms')(v)))
∈ bag(T)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  loc  :  Id
4.  X  :  EClass(T)
5.  P  :  Id  {}\mrightarrow{}  hdataflow(Info;T)
6.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (X(e)  =  (snd(P  loc(e)*(map(\mlambda{}x.info(x);before(e)))(info(e)))))
7.  ms'  :  Info  List@i
8.  v  :  Info@i
\mvdash{}  (snd(P  loc*(firstn(||ms'  @  [v]||  -  1;ms'  @  [v]))(if  ||ms'  @  [v]||  -  1  <z  ||ms'  @  [v]||
then  ms'  @  [v][||ms'  @  [v]||  -  1]
else  hd(ms'  @  [v])
fi  )))
=  (snd(P  loc*(ms')(v)))


By

---

Latex:
((RWO  "length-append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "firstn-append"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index