kleene logic implications/equalities proved
model generation written
reworked 3VL logic details; verifying |- and <: