Step
*
1
of Lemma
hdf-state-base4-2
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. C4 : Base
14. F3 : Base
15. f3 : Base
16. C3 : Base
17. F2 : Base
18. f2 : Base
19. C2 : Base
20. F1 : Base
21. f1 : Base
22. C1 : Base
23. j : ℤ
24. 0 < j
25. ∀s:Base
(λmk-hdf,s. (inl (λa.let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a] then [λs.f1[F1[a];s]] else [] fi
in let v1 ⟵ if name_eq(fst(a);hdr2) ∧b C2[a] then [λs.f2[F2[a];s]] else [] fi
in let v2 ⟵ if name_eq(fst(a);hdr3) ∧b C3[a] then [λs.f3[F3[a];s]] else [] fi
in let v3 ⟵ if name_eq(fst(a);hdr4) ∧b C4[a] 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, v8>))^j - 1
⊥
[s] ≤ fix((λmk-hdf,s. (inl (λa.let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
if name_eq(fst(a);hdr4) ∧b C4[a] then f4[F4[a];s]
else s
fi
in <mk-hdf v, [v]>))))
s)
26. s : Base@i
27. a : Base
⊢ let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a] then [λs.f1[F1[a];s]] else [] fi
in let v1 ⟵ if name_eq(fst(a);hdr2) ∧b C2[a] then [λs.f2[F2[a];s]] else [] fi
in let v2 ⟵ if name_eq(fst(a);hdr3) ∧b C3[a] then [λs.f3[F3[a];s]] else [] fi
in let v3 ⟵ if name_eq(fst(a);hdr4) ∧b C4[a] 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.[f s]
in let v8 ⟵ if bag-null(v7) then [s] else v7 fi
in <λmk-hdf,s. (inl (λa.let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a]
then [λs.f1[F1[a];s]]
else []
fi
in let v1 ⟵ if name_eq(fst(a);hdr2) ∧b C2[a]
then [λs.f2[F2[a];s]]
else []
fi
in let v2 ⟵ if name_eq(fst(a);hdr3) ∧b C3[a]
then [λs.f3[F3[a];s]]
else []
fi
in let v3 ⟵ if name_eq(fst(a);hdr4) ∧b C4[a]
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, v8>))^j - 1
⊥
v8
, v8
> ≤ let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
if name_eq(fst(a);hdr4) ∧b C4[a] then f4[F4[a];s]
else s
fi
in <fix((λmk-hdf,s. (inl (λa.let v ⟵ if name_eq(fst(a);hdr1) ∧b C1[a] then f1[F1[a];s]
if name_eq(fst(a);hdr2) ∧b C2[a] then f2[F2[a];s]
if name_eq(fst(a);hdr3) ∧b C3[a] then f3[F3[a];s]
if name_eq(fst(a);hdr4) ∧b C4[a] then f4[F4[a];s]
else s
fi
in <mk-hdf v, [v]>))))
v
, [v]
>
BY
{ RepeatFor 4 (HdfStateTransCase⋅) }
Latex:
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. C4 : Base
14. F3 : Base
15. f3 : Base
16. C3 : Base
17. F2 : Base
18. f2 : Base
19. C2 : Base
20. F1 : Base
21. f1 : Base
22. C1 : Base
23. j : \mBbbZ{}
24. 0 < j
25. \mforall{}s:Base
(\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a]
then [\mlambda{}s.f1[F1[a];s]]
else []
fi
in let v1 \mleftarrow{}{} if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a]
then [\mlambda{}s.f2[F2[a];s]]
else []
fi
in let v2 \mleftarrow{}{} if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a]
then [\mlambda{}s.f3[F3[a];s]]
else []
fi
in let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4) \mwedge{}\msubb{} C4[a]
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, v8>))\^{}j - 1
\mbot{}
[s] \mleq{} fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a] then f1[F1[a];s]
if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a] then f2[F2[a];s]
if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a] then f3[F3[a];s]
if name\_eq(fst(a);hdr4) \mwedge{}\msubb{} C4[a] then f4[F4[a];s]
else s
fi
in <mk-hdf v, [v]>))))
s)
26. s : Base@i
27. a : Base
\mvdash{} let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a] then [\mlambda{}s.f1[F1[a];s]] else [] fi
in let v1 \mleftarrow{}{} if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a] then [\mlambda{}s.f2[F2[a];s]] else [] fi
in let v2 \mleftarrow{}{} if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a] then [\mlambda{}s.f3[F3[a];s]] else [] fi
in let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4) \mwedge{}\msubb{} C4[a] 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.[f s]
in let v8 \mleftarrow{}{} if bag-null(v7) then [s] else v7 fi
in <\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a]
then [\mlambda{}s.f1[F1[a];s]]
else []
fi
in let v1 \mleftarrow{}{} if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a]
then [\mlambda{}s.f2[F2[a];s]]
else []
fi
in let v2 \mleftarrow{}{} if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a]
then [\mlambda{}s.f3[F3[a];s]]
else []
fi
in let v3 \mleftarrow{}{} if name\_eq(fst(a);hdr4)
\mwedge{}\msubb{} C4[a]
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, v8>))\^{}j - 1\000C
\mbot{}
v8
, v8
> \mleq{} let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a] then f1[F1[a];s]
if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a] then f2[F2[a];s]
if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a] then f3[F3[a];s]
if name\_eq(fst(a);hdr4) \mwedge{}\msubb{} C4[a] then f4[F4[a];s]
else s
fi
in <fix((\mlambda{}mk-hdf,s. (inl (\mlambda{}a.let v \mleftarrow{}{} if name\_eq(fst(a);hdr1) \mwedge{}\msubb{} C1[a]
then f1[F1[a];s]
if name\_eq(fst(a);hdr2) \mwedge{}\msubb{} C2[a]
then f2[F2[a];s]
if name\_eq(fst(a);hdr3) \mwedge{}\msubb{} C3[a]
then f3[F3[a];s]
if name\_eq(fst(a);hdr4) \mwedge{}\msubb{} C4[a]
then f4[F4[a];s]
else s
fi
in <mk-hdf v, [v]>))))
v
, [v]
>
By
Latex:
RepeatFor 4 (HdfStateTransCase\mcdot{})
Home
Index