-- typeConsistencyOfStoreValues.tioga
-- Spreitze, May 9, 1991 1:55 pm PDT

We take a very simple model.
There is a set of variables, V.  There is a configuration, 
We have one operation: Store value u1 into variable v2.  This is successful only if v2 new configuration 
    if v 
    if v = v2 then 

We have a set of types, T.  We have a typing, an assignment of types to the variables, 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, 
We say that a configuration 
    for all v in V, 
Now, we restrict Store to also require:
    Storing u1 into v2 is legal for typing 
        u1 

Now, we attempt to prove that: if succeeds for 

We must prove that 
    if v 
    if v = v2, then 

Now go one step indirect (which a compiler must do, since it doesn't have runtime values in its hands), and introduce the 
operation: Store from v1 through v2, for v1 and v2 in V, which means to store the value successful only if 
    if v 
    if v = 
Store from v1 through v2 is legal exactly when storing u1 into v3 is legal for every u1 legal it produces a 
What do we need to know in order to prove that storing u1 into v3 is legal for every u1 these hypotheses:
H1:  for v 
H2:  
We must prove that u1 
    (1):  u1 
        given;
    (2):  
        by H2;
    (3):  v3 
        given;
    (4):  
        by H1 and (3);
    (5):  u1 
        by (1), (2), and (4).
H2 must be checked when compiling as assignment expression.  H1 is taken to be part of the language definition.
When might case, v will be a t1 variable or a t2 variable; every v 
When might is never utilized in the above proof.