--
-- Proof scores template
--

--
-- The proof scores template could be generated from the
-- specification. 
-- (*** We should make a tool that generates proof scores templates
-- from CafeOBJ specifications (semi-)auomatically.***)
-- If you prove that the system has a property, first copy and paste
-- this proof scores template.
-- This example is tiny, and proof scores for each invariant are
-- short.
-- In a middle-sized one, proof socres for each invariant can be about 
-- a few thousand lines or more.
-- In that case, proof scores template is really usefull.
--

-- I) Base case

open INV
  red INVARIANT .
close

-- II) Inductive ceses

--> 1) inc(s)
open ISTEP
-- arbitrary objects
-- assumptions
-- successor state
  eq s' = inc(s) .
-- check if the predicate is true.
  red PREDICATE .
close

--> 2) dec(s)
-- 2.1) c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  -- eq c-dec(s) = treue .
  eq flag(s) = true .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red PREDICATE .
close
--
-- 2.1) not c-dec(s)
open ISTEP
-- arbitrary objects
-- assumptions
  eq c-dec(s) = false .
-- successor state
  eq s' = dec(s) .
-- check if the predicate is true.
  red PREDICATE .
close

--> Q.E.D.