---

Step * 1 1 1 1 1 1 1 of Lemma once-class-program_wf


1. Info : Type
2. B : Type
3. X : EClass(B)
4. es : EO+(Info)@i'
5. z : hdataflow(Info;B)@i
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))))
     ⇒ (hdf-once(z)*(map(λx.info(x);before(e1)))
        = hdf-once(if isl(last(λe'.0 <z #(X(e'))) e1) then hdf-halt() else z*(map(λx.info(x);before(e1))) fi )
        ∈ hdataflow(Info;B)))
8. ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B)))@i
9. ¬↑first(e)
10. hdf-once(z)*(map(λx.info(x);before(pred(e))))
= hdf-once(if isl(last(λe'.0 <z #(X(e'))) pred(e)) then hdf-halt() else z*(map(λx.info(x);before(pred(e)))) fi )
∈ hdataflow(Info;B)
⊢ (fst(hdf-once(z)*(map(λx.info(x);before(pred(e))))(info(pred(e)))))
= hdf-once(if isl(if 0 <z #(X(pred(e))) then inl pred(e) else last(λe'.0 <z #(X(e'))) pred(e) fi )
  then hdf-halt()
  else fst(z*(map(λx.info(x);before(pred(e))))(info(pred(e))))
  fi )
∈ hdataflow(Info;B)
BY
{ (HypSubst' (-1) 0 THENA Try (Complete (Auto))) }

1
1. Info : Type
2. B : Type
3. X : EClass(B)
4. es : EO+(Info)@i'
5. z : hdataflow(Info;B)@i
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))))
     ⇒ (hdf-once(z)*(map(λx.info(x);before(e1)))
        = hdf-once(if isl(last(λe'.0 <z #(X(e'))) e1) then hdf-halt() else z*(map(λx.info(x);before(e1))) fi )
        ∈ hdataflow(Info;B)))
8. ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B)))@i
9. ¬↑first(e)
10. hdf-once(z)*(map(λx.info(x);before(pred(e))))
= hdf-once(if isl(last(λe'.0 <z #(X(e'))) pred(e)) then hdf-halt() else z*(map(λx.info(x);before(pred(e)))) fi )
∈ hdataflow(Info;B)
⊢ (fst(hdf-once(if isl(last(λe'.0 <z #(X(e'))) pred(e))
then hdf-halt()
else z*(map(λx.info(x);before(pred(e))))
fi )(info(pred(e)))))
= hdf-once(if isl(if 0 <z #(X(pred(e))) then inl pred(e) else last(λe'.0 <z #(X(e'))) pred(e) fi )
  then hdf-halt()
  else fst(z*(map(λx.info(x);before(pred(e))))(info(pred(e))))
  fi )
∈ hdataflow(Info;B)

2
.....wf..... 
1. Info : Type
2. B : Type
3. X : EClass(B)
4. es : EO+(Info)@i'
5. z : hdataflow(Info;B)@i
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))))
     ⇒ (hdf-once(z)*(map(λx.info(x);before(e1)))
        = hdf-once(if isl(last(λe'.0 <z #(X(e'))) e1) then hdf-halt() else z*(map(λx.info(x);before(e1))) fi )
        ∈ hdataflow(Info;B)))
8. ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B)))@i
9. ¬↑first(e)
10. hdf-once(z)*(map(λx.info(x);before(pred(e))))
= hdf-once(if isl(last(λe'.0 <z #(X(e'))) pred(e)) then hdf-halt() else z*(map(λx.info(x);before(pred(e)))) fi )
∈ hdataflow(Info;B)
11. z1 : hdataflow(Info;B)
⊢ (fst(z1(info(pred(e)))))
  = hdf-once(if isl(if 0 <z #(X(pred(e))) then inl pred(e) else last(λe'.0 <z #(X(e'))) pred(e) fi )
    then hdf-halt()
    else fst(z*(map(λx.info(x);before(pred(e))))(info(pred(e))))
    fi )
  ∈ hdataflow(Info;B) ∈ ℙ

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B)
4.  es  :  EO+(Info)@i'
5.  z  :  hdataflow(Info;B)@i
6.  e  :  E@i
7.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}e':E.  (e'  \mleq{}loc  e1    {}\mRightarrow{}  (X(e')  =  (snd(z*(map(\mlambda{}x.info(x);before(e')))(info(e')))))))
          {}\mRightarrow{}  (hdf-once(z)*(map(\mlambda{}x.info(x);before(e1)))
                =  hdf-once(if  isl(last(\mlambda{}e'.0  <z  \#(X(e')))  e1)
                    then  hdf-halt()
                    else  z*(map(\mlambda{}x.info(x);before(e1)))
                    fi  )))
8.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(z*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
9.  \mneg{}\muparrow{}first(e)
10.  hdf-once(z)*(map(\mlambda{}x.info(x);before(pred(e))))
=  hdf-once(if  isl(last(\mlambda{}e'.0  <z  \#(X(e')))  pred(e))
    then  hdf-halt()
    else  z*(map(\mlambda{}x.info(x);before(pred(e))))
    fi  )
\mvdash{}  (fst(hdf-once(z)*(map(\mlambda{}x.info(x);before(pred(e))))(info(pred(e)))))
=  hdf-once(if  isl(if  0  <z  \#(X(pred(e)))  then  inl  pred(e)  else  last(\mlambda{}e'.0  <z  \#(X(e')))  pred(e)  fi  )
    then  hdf-halt()
    else  fst(z*(map(\mlambda{}x.info(x);before(pred(e))))(info(pred(e))))
    fi  )


By

---

Latex:
(HypSubst'  (-1)  0  THENA  Try  (Complete  (Auto)))

---

Home Index