data False = 
data True = true

data Colour = red | green

Phys_State :: Set
           = sig
               sigA :: Colour
               sigB :: Colour

data Control_State = Allred | Agreen | Bgreen

toSigA (s:: Control_State)
       :: Colour
       = case s of
         (Allred)-> red
         (Agreen)-> green
         (Bgreen)-> red


toSigB (s:: Control_State)
       :: Colour
       = case s of
         (Allred)-> red
         (Agreen)-> red
         (Bgreen)-> green

phys_state (s:: Control_State)
           :: Phys_State
           = struct
                sigA = toSigA s
                sigB = toSigB s


CorAux (a,b:: Colour)
       :: Set 
       = case a of
         (red  )-> True
         (green)->
           case b of
           (red  )-> True
           (green)-> False

Cor (s:: Phys_State)
    :: Set
    = CorAux s.sigA s.sigB

cor_proof (s:: Control_State)
          :: Cor(phys_state s)
          = case s of
            (Allred)-> true
            (Agreen)-> true
            (Bgreen)-> true