--> Base case
open INV
  red inv4(init) .
close

--> Inductive cases
--> 1 approach(s)
-- 1.1 c-approach(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-approach(s) = true .
  eq t(s) = sect0 .
  eq c(s) = state0 .
-- successor state
  eq s' = approach(s) .
-- check 
  red istep4 .
close
--
-- 1.2 not c-approach(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-approach(s) = false .
-- successor state
  eq s' = approach(s) .
-- check 
  red istep4 .
close

--> 2 in(s)
-- 2.1 c-in(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-in(s) = true .
  eq t(s) = sect1 .
  eq tl(s) <= now(s) = 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) .
-- facts
  -- ceq (X:Real+) <= (T:Timeval) = true if X <= now(s) and now(s) <= T .
  eq tl(s) <= cl(s) = true .
-- successor state
  eq s' = in(s) .
-- check 
  red istep4 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-in(s) = true .
  eq t(s) = sect1 .
  eq tl(s) <= now(s) = true .
  --
  eq g(s) = up .
  eq c(s) = state1 .
  eq now(s) <= cu(s) = true .
  eq (cu(s) = cl(s)) = false .
-- successor state
  eq s' = in(s) .
-- check 
  red istep4 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-in(s) = true .
  eq t(s) = sect1 .
  eq tl(s) <= now(s) = true .
  --
  eq g(s) = up .
  eq c(s) = state1 .
  eq now(s) <= cu(s) = false .
-- successor state
  eq s' = in(s) .
-- check 
  red inv5(s) implies istep4 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-in(s) = true .
  eq t(s) = sect1 .
  eq tl(s) <= now(s) = true .
  --
  eq g(s) = up .
  eq (c(s) = state1) = false .
-- successor state
  eq s' = in(s) .
-- check 
  red istep4 .
close
--
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-in(s) = true .
  eq t(s) = sect1 .
  eq tl(s) <= now(s) = true .
  --
  eq (g(s) = up) = false .
-- successor state
  eq s' = in(s) .
-- check 
  red istep4 .
close
--
-- 2.2 not c-in(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-in(s) = false .
-- successor state
  eq s' = in(s) .
-- check 
  red istep4 .
close

--> 3 out(s)
-- 3.1 c-out(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-out(s) = true .
  eq t(s) = crossing .
-- successor state
  eq s' = out(s) .
-- check 
  red istep4 .
close
--
-- 3.2 not c-out(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-out(s) = false .
-- successor state
  eq s' = out(s) .
-- check 
  red istep4 .
close

--> 4 exit(s)
-- 4.1 c-exit(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-exit(s) = true .
  eq t(s) = sect2 .
  eq c(s) = state2 .
-- successor state
  eq s' = exit(s) .
-- check 
  red istep4 .
close
--
-- 4.2 not c-exit(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-exit(s) = false .
-- successor state
  eq s' = exit(s) .
-- check 
  red istep4 .
close

--> 5 down(s)
-- 5.1 c-down(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-down(s) = true .
  eq g(s) = lowering .
-- successor state
  eq s' = down(s) .
-- check 
  red istep4 .
close
--
-- 5.2 not c-down(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-down(s) = false .
-- successor state
  eq s' = down(s) .
-- check 
  red istep4 .
close

--> 6 up(s)
-- 6.1 c-up(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-up(s) = true .
  eq g(S) = raising .
-- successor state
  eq s' = up(s) .
-- check 
  red istep4 .
close
--
-- 6.2 not c-up(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-up(s) = false .
-- successor state
  eq s' = up(s) .
-- check 
  red istep4 .
close

--> 7 lower(s)
-- 7.1 c-lower(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-lower(s) = true .
  eq g(s) = up .
  eq c(s) = state1 .
  eq cl(s) <= now(s) = true .
-- successor state
  eq s' = lower(s) .
-- check 
  red istep4 .
close
--
-- 7.2 not c-lower(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-lower(s) = false .
-- successor state
  eq s' = lower(s) .
-- check 
  red istep4 .
close

--> 8 raise(s)
-- 8.1 c-raise(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-raise(s) = true .
  eq g(s) = down .
  eq c(s) = state3 .
-- successor state
  eq s' = raise(s) .
-- check 
  red istep4 .
close
--
-- 8.2 not c-raise(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-raise(s) = false .
-- successor state
  eq s' = raise(s) .
-- check 
  red istep4 .
close

--> 9 tick(s,d)
-- 9.1 c-tick(s,d)
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq c-tick(s,d) = true .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep4 .
close
--
-- 9.2 not c-tick(s,d)
open ISTEP
-- arbitrary objects
  op d : -> Real+ .
-- assumptions
  eq c-tick(s,d) = false .
-- successor state
  eq s' = tick(s,d) .
-- check 
  red istep4 .
close


--> Q.E.D.