-- typeConsistencyOfStore.tioga
-- Sturgis, March 21, 1989 10:59:02 am PST
-- Spreitze, May 9, 1991 1:57 pm PDT

[This is Howard's typeConsistencyOfStore.tioga of 21-Mar-89 10:59:02 PST, with the missing parenthesis in the legality requirement for Store added, one of the two D's renamed to D, and formatting changes.  See my typeConsistencyOfStoreValues.tioga for a justification of Howard's legality requirement for Store.  MJS, May 9, 1991]
We take a very simple model.
There is a set of variables, V.  There is a configuration, G: V _ U, where U is the set of values.  V I U.
We have one operation: Store from v1 through v2, for v1 and v2 in V.  This is successful only if G(v2) B V.  When it is successful, it produces a new configuration G(, where G( is defined by: 
if v = G(v2) then G((v) = G(v).
if v = G(v2) then G((v) = G(v1).

We have a set of types, T.  We have a typing, an assignment of types to the variables, D: V _ T.  For the moment, we assume that the typing is fixed.
The types really belong to an algebra.  This algebra has (for the moment) two unary operations: load and store.  That is, for some types t in T, t.load and t.store are defined and also in T.
Given a typing, D, and a type, t, we have a set of values: D(t) I U.  We make only one assumption (for the moment) about this set of values:
for v B V, if v B D(t), then
D(D(v)) I D(t.load), and
D(t.store) I D(D(v)).
We say that a configuration G is consistent with a typing D if and only if
for all v in V, G(v) B D(D(v)).
Now, we restrict Store to also require:
Store from v1 through v2 is legal for typing D only if
D(D(v1)) I D(D(v2).store)

Now, we attempt to prove that: if G is consistent with a typing D, Store from v1 through v2 is legal for typing D, and Store from v1 through v2 succeeds for G, producing G(, then G( is consistent with D.

We must prove that G((v) B D(D(v)), for all v in V.  Let v3 = G(v2).
if v = v3, then G((v) = G(v), and the conclusion follows from the assumption that G is consistent with D.
So, to complete the proof, we need only prove that G((v3) B D(D(v3)).
G((v3) = G(v1)
by definition of v3 and the definition of G(.
G(v1) B D(D(v1))
by the assumption that G is consistent with D.
D(D(v1)) I D(D(v2).store)
by the assumption that a store from v1 through v2 is legal for D.
D(D(v2).store) I D(D(v3))
This requires several steps.
G(v2) B D(D(v2))
because G is consistent with D
v3 B D(D(v2))
because v3 = G(v2)
letting t = D(v2), we have
v3 B D(t)
hence D(t.store) I D(D(v3))
by our assumption about lt.D(t)
D(D(v2).store) I D(D(v3))
from D(t.store) I D(D(v3)) and t = D(v2)

Collecting, we have
G((v3) B D(D(v3)), as desired.

������Ê)��˜�J˜J˜*J˜$J˜�Iblockšœ£ÏgœÏmœ—˜ÊKšœ˜KšœÏiœœŸœžœŸœŸœŸœžœŸœ˜jšœ"ŸÏdœ	Ÿ œŸ œŸ œŸœœŸ œžœŸœ:žœžœ˜ÀIindentšœŸœžœœŸ œžœŸœœŸœ˜LšœŸœœŸ œžœŸœœŸ œ˜ —K˜�KšœŸœ>žœŸœžœŸœ6˜•Kšœ‰ŸœŸœŸœ
ŸœŸœ˜¾š
œžœŸœœŸœžœŸœI˜ŒšœŸœžœŸœŸœžœœŸœ˜LšœžœŸœžœœŸœ˜LšœŸœžœœžœŸœ˜——šœœžœ˜JLšœŸœŸœœŸœžœœžœŸœ˜—˜'š	œŸ œ	Ÿ œžœ˜6LšœžœŸ œžœœžœŸ œ˜——K˜�Kšœ"œžœ
Ÿ œ	Ÿ œžœŸ œ	Ÿ œœžœžœžœ˜ËK˜�šœžœŸœžœœžœŸœŸœŸœŸ œœŸ œ˜DLšœŸœžœŸ œžœŸœœŸœ7œžœ˜iLšœ3žœŸ œžœœžœŸ œ˜EšžœŸ œœŸ œ˜LšœŸ œžœ˜-—šœŸ œžœœžœŸ œ˜Lšœœœ˜.—šœžœŸ œžœœžœŸ œ˜Lš	œ$Ÿ œ	Ÿ œžœ˜A—šœžœŸ œ	žœœžœŸ œ˜˜šœŸ œžœœžœŸ œ˜Lšœœ˜—šŸ œžœœžœŸ œ˜
Lš	œŸ œœŸ œ˜—šœŸœžœŸ œ
˜Lš	Ÿ œžœœŸœ˜	šœœŸœžœœžœŸ œ˜LšœŸœœŸœ˜——šœžœŸ œ	žœœžœŸ œ˜LšœœŸœžœœžœŸ œŸœžœŸ œ˜(———L˜�˜LšžœŸ œžœœžœŸ œ˜—L˜�——�…—����
X��‡��