++++++++++++
-(t is little tau, T is large tau, E is 'in', and + is that other symbol)
+(t is used for types, T is the context, and + is used for in)
[Eq, NEq]
[Assignment]
-T+ i := e:t <= i:t E T & T+ e:t
+T+ i := e:t <= i:t in T & T+ e:t
The assignemnt of e to i returns type t if both i and e have type t.
[EVar]
-T+ i:t <= i:t E T
+T+ i:t <= i:t in T
i has type t if i is defined in the context with type t.
[EPost]
-T+ EPost i:int <= i:int E T
+T+ EPost i:int <= i:int in T
EPost i is of type int if i is defined in T with type int.
[SDecl]
-T+ t i = e => T,i:t <= i!ET & e:t
+T+ t i = e => T,i:t <= i not in T & e:t
if i and e are of the same type and i is not declared in the current scope then i is added with type t to the context.
[SDeclD]
-T+ t i => T,i:t <= i!ET
+T+ t i => T,i:t <= i not in T
if i is not declared in the current scope, then i is added to the context with type t