Step
*
1
1
1
1
1
of Lemma
sequence-class-program_wf
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. x : E@i
11. x ≤loc e @i
12. ↑(bag-null(snd(xpr*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(x)))(info(x))))))
13. ∀e'':E
((e'' <loc x)
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);before(e'')))(info(e''))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(e'')))(info(e''))))))))
14. v : E List@i
15. before(e) = v ∈ (E List)@i
16. before(e) = (before(x) @ v) ∈ (E List)
17. v ∈ E List
⊢ (snd(zpr*(map(λx@0.info(x@0);v))(info(e))))
= (snd(mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);before(x)))*(map(\000Cλx.info(x);v))(info(e))))
∈ bag(A)
BY
{ Assert ⌈mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);before(x)\000C))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);before(x)))
, ypr*(map(λx.info(x);before(x)))
>)
∈ hdataflow(Info;A)⌉⋅ }
1
.....assertion.....
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. x : E@i
11. x ≤loc e @i
12. ↑(bag-null(snd(xpr*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(x)))(info(x))))))
13. ∀e'':E
((e'' <loc x)
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);before(e'')))(info(e''))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(e'')))(info(e''))))))))
14. v : E List@i
15. before(e) = v ∈ (E List)@i
16. before(e) = (before(x) @ v) ∈ (E List)
17. v ∈ E List
⊢ mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);before(x)))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);before(x)))
, ypr*(map(λx.info(x);before(x)))
>)
∈ hdataflow(Info;A)
2
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. x : E@i
11. x ≤loc e @i
12. ↑(bag-null(snd(xpr*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(x)))(info(x))))))
13. ∀e'':E
((e'' <loc x)
⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);before(e'')))(info(e''))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(e'')))(info(e''))))))))
14. v : E List@i
15. before(e) = v ∈ (E List)@i
16. before(e) = (before(x) @ v) ∈ (E List)
17. v ∈ E List
18. mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);before(x)))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr*(map(λx.info(x);before(x)))
, ypr*(map(λx.info(x);before(x)))
>)
∈ hdataflow(Info;A)
⊢ (snd(zpr*(map(λx@0.info(x@0);v))(info(e))))
= (snd(mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);before(x)))*(map(\000Cλx.info(x);v))(info(e))))
∈ bag(A)
Latex:
Latex:
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. x : E@i
11. x \mleq{}loc e @i
12. \muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);before(x)))(info(x))))
\mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);before(x)))(info(x))))))
13. \mforall{}e'':E
((e'' <loc x)
{}\mRightarrow{} (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))
\mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))))))
14. v : E List@i
15. before(e) = v@i
16. before(e) = (before(x) @ v)
17. v \mmember{} E List
\mvdash{} (snd(zpr*(map(\mlambda{}x@0.info(x@0);v))(info(e))))
= (snd(mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(\mlambda{}x.info(\000Cx);before(x)))*(map(\mlambda{}x.info(x);v))(info(e))))
By
Latex:
Assert \mkleeneopen{}mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(\mlambda{}x\000C.info(x);before(x)))
= mk-hdf(S,a.case S
of inl(XY) =>
let X,Y = XY
in let X',bx = X(a)
in let Y',by = Y(a)
in if bag-null(bx) \mwedge{}\msubb{} (\mneg{}\msubb{}bag-null(by))
then let Z',bz = zpr(a)
in <inr Z' , bz>
else <inl <X', Y'>, bx>
fi
| inr(Z) =>
let Z',b = Z(a)
in <inr Z' , b>S.case S
of inl(XY) =>
ff
| inr(Z) =>
hdf-halted(Z);inl <xpr*(map(\mlambda{}x.info(x);before(x))), ypr*(map(\mlambda{}x.info(x);before(x)))>)\mkleeneclose{}\mcdot{}
Home
Index