open LTO
-- check if the property holds
  red (inv8(s,i) /\ lto17(s,i)) => lto18(s,i) .
close