Step
*
2
1
1
1
of Lemma
hdf-memory-base4-3
1. hdr1 : Name
2. hdr2 : Name
3. hdr3 : Name
4. hdr4 : Name
5. ¬(hdr3 = hdr4 ∈ Name)
6. ¬(hdr2 = hdr4 ∈ Name)
7. ¬(hdr2 = hdr3 ∈ Name)
8. ¬(hdr1 = hdr4 ∈ Name)
9. ¬(hdr1 = hdr3 ∈ Name)
10. ¬(hdr1 = hdr2 ∈ Name)
11. F4 : Base
12. f4 : Base
13. F3 : Base
14. f3 : Base
15. F2 : Base
16. f2 : Base
17. F1 : Base
18. f1 : Base
19. j : ℤ
20. 0 < j
21. ∀s:Base
(λmk-hdf,s. (inl (λa.let v ←─ if name_eq(fst(a);hdr1) then f1[F1[a];s]
if name_eq(fst(a);hdr2) then f2[F2[a];s]
if name_eq(fst(a);hdr3) then f3[F3[a];s]
if name_eq(fst(a);hdr4) then f4[F4[a];s]
else s
fi
in <mk-hdf v, [s]>))^j - 1
⊥
s ≤ fix((λmk-hdf,s. (inl (λa.let v ←─ if name_eq(fst(a);hdr1) then [λs.f1[F1[a];s]] else [] fi
in let v1 ←─ if name_eq(fst(a);hdr2) then [λs.f2[F2[a];s]] else [] fi
in let v2 ←─ if name_eq(fst(a);hdr3) then [λs.f3[F3[a];s]] else [] fi
in let v3 ←─ if name_eq(fst(a);hdr4) then [λs.f4[F4[a];s]] else [] fi
in let v4 ←─ v2 + v3
in let v5 ←─ v1 + v4
in let v6 ←─ v + v5
in let v7 ←─ ∪f∈v6.map(f;s)
in let v8 ←─ if bag-null(v7) then s else v7 fi
in <mk-hdf v8, s>))))
[s])
22. s : Base@i
23. a : Base
24. z : Base@i
25. name_eq(fst(a);hdr1) ~ inr z
26. z1 : Base@i
27. name_eq(fst(a);hdr2) ~ inr z1
28. z2 : Base@i
29. name_eq(fst(a);hdr3) ~ inr z2
⊢ let v ←─ if name_eq(fst(a);hdr4) then f4[F4[a];s] else s fi
in <λmk-hdf,s. (inl (λa.let v ←─ if name_eq(fst(a);hdr1) then f1[F1[a];s]
if name_eq(fst(a);hdr2) then f2[F2[a];s]
if name_eq(fst(a);hdr3) then f3[F3[a];s]
if name_eq(fst(a);hdr4) then f4[F4[a];s]
else s
fi
in <mk-hdf v, [s]>))^j - 1
⊥
v
, [s]
> ≤ let v3 ←─ if name_eq(fst(a);hdr4) then [λs.f4[F4[a];s]] else [] fi
in let v4 ←─ v3
in let v5 ←─ v4
in let v6 ←─ v5
in let v7 ←─ ∪f∈v6.[f s]
in let v8 ←─ if bag-null(v7) then [s] else v7 fi
in <fix((λmk-hdf,s. (inl (λa.let v ←─ if name_eq(fst(a);hdr1) then [λs.f1[F1[a];s]] else [] fi
in let v1 ←─ if name_eq(fst(a);hdr2) then [λs.f2[F2[a];s]] else [] fi
in let v2 ←─ if name_eq(fst(a);hdr3)
then [λs.f3[F3[a];s]]
else []
fi
in let v3 ←─ if name_eq(fst(a);hdr4)
then [λs.f4[F4[a];s]]
else []
fi
in let v4 ←─ v2 + v3
in let v5 ←─ v1 + v4
in let v6 ←─ v + v5
in let v7 ←─ ∪f∈v6.map(f;s)
in let v8 ←─ if bag-null(v7) then s else v7 fi
in <mk-hdf v8, s>))))
v8
, [s]
>
BY
{ HdfStateTransCase⋅ }
Latex:
1. hdr1 : Name
2. hdr2 : Name
3. hdr3 : Name
4. hdr4 : Name
5. \mneg{}(hdr3 = hdr4)
6. \mneg{}(hdr2 = hdr4)
7. \mneg{}(hdr2 = hdr3)
8. \mneg{}(hdr1 = hdr4)
9. \mneg{}(hdr1 = hdr3)
10. \mneg{}(hdr1 = hdr2)
11. F4 : Base
12. f4 : Base
13. F3 : Base
14. f3 : Base
15. F2 : Base
16. f2 : Base
17. F1 : Base
18. f1 : Base
19. j : \mBbbZ{}
20. 0 < j
21. \mforall{}s:Base
(\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) then f1[F1[a];s]
if name\_eq(fst(a);hdr2) then f2[F2[a];s]
if name\_eq(fst(a);hdr3) then f3[F3[a];s]
if name\_eq(fst(a);hdr4) then f4[F4[a];s]
else s
fi
in <mk-hdf v, [s]>))\^{}j - 1
\mbot{}
s \mleq{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1)
then [\mlambda{}s.f1[F1[a];s]]
else []
fi
in let v1 \mleftarrow{}{} if name\_eq(fst(a);hdr2)
then [\mlambda{}s.f2[F2[a];s]]
else []
fi
in let v2 \mleftarrow{}{} if name\_eq(fst(a);hdr3)
then [\mlambda{}s.f3[F3[a];s]]
else []
fi
in let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4)
then [\mlambda{}s.f4[F4[a];s]]
else []
fi
in let v4 \mleftarrow{}{} v2 + v3
in let v5 \mleftarrow{}{} v1 + v4
in let v6 \mleftarrow{}{} v + v5
in let v7 \mleftarrow{}{} \mcup{}f\mmember{}v6.map(f;s)
in let v8 \mleftarrow{}{} if bag-null(v7)
then s
else v7
fi
in <mk-hdf v8, s>))))
[s])
22. s : Base@i
23. a : Base
24. z : Base@i
25. name\_eq(fst(a);hdr1) \msim{} inr z
26. z1 : Base@i
27. name\_eq(fst(a);hdr2) \msim{} inr z1
28. z2 : Base@i
29. name\_eq(fst(a);hdr3) \msim{} inr z2
\mvdash{} let v \mleftarrow{}{} if name\_eq(fst(a);hdr4) then f4[F4[a];s] else s fi
in <\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) then f1[F1[a];s]
if name\_eq(fst(a);hdr2) then f2[F2[a];s]
if name\_eq(fst(a);hdr3) then f3[F3[a];s]
if name\_eq(fst(a);hdr4) then f4[F4[a];s]
else s
fi
in <mk-hdf v, [s]>))\^{}j - 1
\mbot{}
v
, [s]
> \mleq{} let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4) then [\mlambda{}s.f4[F4[a];s]] else [] fi
in let v4 \mleftarrow{}{} v3
in let v5 \mleftarrow{}{} v4
in let v6 \mleftarrow{}{} v5
in let v7 \mleftarrow{}{} \mcup{}f\mmember{}v6.[f s]
in let v8 \mleftarrow{}{} if bag-null(v7) then [s] else v7 fi
in <fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1)
then [\mlambda{}s.f1[F1[a];s]]
else []
fi
in let v1 \mleftarrow{}{} if name\_eq(fst(a);hdr2)
then [\mlambda{}s.f2[F2[a];s]]
else []
fi
in let v2 \mleftarrow{}{} if name\_eq(fst(a);hdr3)
then [\mlambda{}s.f3[F3[a];s]]
else []
fi
in let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4)
then [\mlambda{}s.f4[F4[a];s]]
else []
fi
in let v4 \mleftarrow{}{} v2 + v3
in let v5 \mleftarrow{}{} v1 + v4
in let v6 \mleftarrow{}{} v + v5
in let v7 \mleftarrow{}{} \mcup{}f\mmember{}v6.map(f;s)
in let v8 \mleftarrow{}{} if bag-null(v7)
then s
else v7
fi
in <mk-hdf v8, s>))))
v8
, [s]
>
By
HdfStateTransCase\mcdot{}
Home
Index