enrich
   RGI-Conds
with
   

   
   
   
   predicates  CRely : nat × (nat → bool) × cstate × (nat → bool) × cstate;
               CGuar : nat × (nat → bool) × cstate × (nat → bool) × cstate;
               CInit : nat × (nat → bool) × cstate;
               CRelyto : nat × (nat → bool) × cstate × (nat → bool) × cstate;
               CGuarto : nat × (nat → bool) × cstate × (nat → bool) × cstate;
               CInitto : nat × (nat → bool) × cstate;
               CInv : nat × (nat → bool) × cstate;
   procedures CSPAWN nat : (nat → bool) × (nat → input) × cstate × (nat → output) nonfunctional nondeterministic;
              CSEQ nat : (nat → bool) × (nat → input) × cstate × (nat → output) nonfunctional nondeterministic;
   variables  Act : nat → bool flexible;
              act : nat → bool;
              act0 : nat → bool;
              act1 : nat → bool;
              act2 : nat → bool;
              act3 : nat → bool;
              cs0 : cstate;
              cs1 : cstate;
              cs2 : cstate;
              Rfun : (nat → bool) × cstate × (nat → bool) × cstate → bool;
              Invfun : (nat → bool) × cstate → bool;
   
   

   

   axioms CGuar-def
          : ⊦   CGuar(m, act, cs, act0, cs0)
              ↔   Guar(m, cs, cs0) ∧ ((¬ act(m) → Idle(m, cs)) → ¬ act0(m) → Idle(m, cs0))
                ∧ (∀ m0. m0 ≠ m → (act0(m0) ↔ act(m0)) ∧ (Idle(m0, cs) ↔ Idle(m0, cs0)));
          CRely-def :  ⊦ CRely(m, act1, cs1, act2, cs2) ↔ Rely(m, cs1, cs2) ∧ (Idle(m, cs1) ↔ Idle(m, cs2)) ∧ (act2(m) ↔ act1(m));
          CInit-def :  ⊦ CInit(m, act1, cs1) ↔ Idle(m, cs1) ∧ ¬ act1(m);
          CInv-def :  ⊦ CInv(m, act, cs) ↔ Inv(cs) ∧ (∀ m0. m < m0 → Idle(m0, cs) ∧ ¬ act(m0));
          CInitto-def :  ⊦ CInitto(m, act1, cs1) ↔ (∀ m0. m0 ≤ m → CInit(m0, act1, cs1));
          CRrelyto-def :  ⊦ CRelyto(m, act, cs, act0, cs0) ↔ (∀ m0. m0 ≤ m → CRely(m0, act, cs, act0, cs0));
          CGuarto-def :  ⊦ CGuarto(m, act, cs, act0, cs0) ↔ (∃ m0. m0 ≤ m ∧ CGuar(m0, act, cs, act0, cs0));

   

   declaration CSEQ-def : CSEQ(m; Act, Inp, CS, Outp){{skip or {Act(m) := true; COP(m, Inp; CS, Outp); Act(m) := false}} star};
               CSPAWN-def
               : CSPAWN(n; Act, Inp, CS, Outp)
                 {if* n = 0 then CSEQ(n; Act, Inp, CS, Outp) else CSEQ(n; Act, Inp, CS, Outp) ∥ CSPAWN(n - 1; Act, Inp, CS, Outp)}
               ;
end enrich