-- 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 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, 
We have one operation: Store from v1 through v2, for v1 and v2 in V.  This is successful only if it produces a new configuration 
    if v 
    if v = 

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, of values:
    for v 
        
        
We say that a configuration 
    for all v in V, 
Now, we restrict Store to also require:
    Store from v1 through v2 is legal for typing 
        

Now, we attempt to prove that: if v1 through v2 succeeds for 

We must prove that 
    if v 
    So, to complete the proof, we need only prove that 
    
        by definition of v3 and the definition of 
    
        by the assumption that 
    
        by the assumption that a store from v1 through v2 is legal for 
    
        This requires several steps.
            
                because 
            v3 
                because v3 = 
            letting t = 
                v3 
                hence 
                    by our assumption about 
            
                from 

    Collecting, we have