extended all proofs that worked before to the Star case...required a stronger notion of non-problematic values |=

var a = 5;


a =  a + 3;
print a;