open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  eq (g(s) = up and c(s) = state1) = false .
  eq (g(s) = lowering and c(s) = state2) = false .
  eq (g(s) = down and c(s) = state2) = false .
-- check
  red inv8(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = up and c(s) = state1) = true .
  eq g(s) = up .
  eq c(s) = state1 .
  --
  -- eq now(s) <= cu(s) = true .
  eq now(s) <= cl(s) = true .
  eq cu(s) = cl(s) .
  eq tl(s) + d2 = cl(s) + d1 .
-- facts
  ceq cl(s) < tl(s) = true if tl(s) + d2 = cl(s) + d1 and d2 < d1 .
  ceq now(s) < tl(s) = true if now(s) <= cl(s) and cl(s) < tl(s) .
-- check
  red inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = up and c(s) = state1) = true .
  eq g(s) = up .
  eq c(s) = state1 .
  --
  -- eq now(s) <= cu(s) = true .
  eq now(s) <= cl(s) = true .
  eq cu(s) = cl(s) .
  eq (tl(s) + d2 = cl(s) + d1) = false .
-- check
  red inv4(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = up and c(s) = state1) = true .
  eq g(s) = up .
  eq c(s) = state1 .
  --
  eq now(s) <= cu(s) = true .
  eq (cu(s) = cl(s)) = false .
-- check
  red inv4(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = up and c(s) = state1) = true .
  eq g(s) = up .
  eq c(s) = state1 .
  --
  eq now(s) <= cu(s) = false .
-- check
  red inv5(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = lowering and c(s) = state2) = true .
  eq g(s) = lowering .
  eq c(s) = state2 .
  --
  eq now(s) <= gu(s) = true .
  eq gu(s) + d1 = tl(s) + d2 + d3 .
-- facts
  ceq gu(s) < tl(s) = true if gu(s) + d1 = tl(s) + d2 + d3 and d2 + d3 < d1 .
  ceq now(s) < tl(s) = true if now(s) <= gu(s) and gu(s) < tl(s) .
-- check
  red inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = lowering and c(s) = state2) = true .
  eq g(s) = lowering .
  eq c(s) = state2 .
  --
  eq now(s) <= gu(s) = true .
  eq (gu(s) + d1 = tl(s) + d2 + d3) = false .
-- check
  red inv6(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = lowering and c(s) = state2) = true .
  eq g(s) = lowering .
  eq c(s) = state2 .
  --
  eq now(s) <= gu(s) = false .
-- check
  red inv7(s) implies inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq t(s) = sect1 .
  --
  -- eq (g(s) = down and c(s) = state2) = true .
  eq g(s) = down .
  eq c(s) = state2 .
-- check
  red inv9(s) .  
close
--
open INV
-- arbitrary objects
  op s : -> Sys .
-- assumptions
  eq (t(s) = sect1) = false .
-- check
  red inv9(s) .  
close

--> Q.E.D.