Require Import model_structure.


Module sforces_cbn (ks : Kripke_structure).
  Export ks.
  Module ks_monad := (Kripke_structure_monad ks).
  Export ks_monad.

  Fixpoint sforces (w:K)(annot:bool)(A:formula) {struct A} : Type :=
    match A with
      | Atom a => X w annot (Atom a)
                    
      | Bot => X w annot Bot
                 
      | Func A1 A2 =>
        forall w', w <= w' ->
                   forall annot', leb annot annot' ->
                      Kont sforces w' annot' A1 -> Kont sforces w' annot' A2
                                                             
      | Sum A1 A2 => sum (Kont sforces w annot A1) (Kont sforces w annot A2)
    end.

  Lemma sforces_mon : forall A w annot, sforces w annot A ->
                      forall w', w <= w' -> sforces w' annot A.

  Lemma Kont_sforces_mon2' :
    forall w annot A,
      (forall w, sforces w false A -> sforces w true A) ->
      Kont sforces w annot A ->
      forall annot', leb annot annot' -> Kont sforces w annot' A.

  Lemma sforces_mon2 : forall A w, sforces w false A -> sforces w true A.

  Definition Kont_sforces_mon2 :
    forall w annot A,
      Kont sforces w annot A ->
      forall annot', leb annot annot' -> Kont sforces w annot' A :=
    fun w annot A => @Kont_sforces_mon2' w annot A (@sforces_mon2 A).

  Definition run {w annot} :
    Kont sforces w annot Bot -> X w annot Bot.
End sforces_cbn.