enrich gen-execute , 
       gen-value , 
       gen-names , 
       gen-command-list
 , 
       gen-secdomain-set
 with
   functions 
      contents : systemstate × name → value;
      comment: Rushby Def. 5;
       
      observe : secdomain → names;
      comment: Rushby Def. 5;
       
      alter : secdomain → names;
      comment: Rushby Def. 5;
       
      run : systemstate × commandlist → systemstate;
      execl : commandlist → systemstate;
      step : systemstate × command → systemstate;
      test : commandlist × command → output;
      ipurge : commandlist × secdomain → commandlist;
      sources : commandlist × secdomain → secdomainset;
   predicates 
       . ⇒ . : secdomain × secdomain;
      comment: security policy, interference relation;
       
      eqd : systemstate × secdomain × systemstate;
      comment: Rushby Reference Monitor Assumption.;
       
      eqds : systemstate × secdomainset × systemstate;
   
   axioms 
      eqd-def :  ⊦ eqd(sys, d, sys0) ↔ (∀ nam. nam ∈ observe(d) → contents(sys, nam) = contents(sys0, nam));
      eqds-def :  ⊦ eqds(sys, ds, sys0) ↔ (∀ d. d ∈ ds → eqd(sys, d, sys0));
      RMA-1 :  ⊦ eqd(sys, cdom(co), sys0) → exec(sys, co) .2 = exec(sys0, co) .2;
      RMA-2
      : ⊦ 
          eqd(sys, cdom(co), sys0) ∧ contents(sys, nam) = contents(sys0, nam) ∧ nam ∈ alter(cdom(co))
        → contents(exec(sys, co) .1, nam) = contents(exec(sys0, co) .1, nam);
      RMA-3 :  ⊦ contents(exec(sys, co) .1, nam) ≠ contents(sys, nam) → nam ∈ alter(cdom(co));
      alter-observe-respects-policy :  ⊦ nam ∈ alter(d) ∧ nam ∈ observe(d0) → d ⇒ d0;
      test :  ⊦ test(cl, co) = exec(execl(cl), co) .2;
      step :  ⊦ step(sys, co) = exec(sys, co) .1;
      run-base :  ⊦ run(sys, []) = sys;
      used for : s, ls;
       
      run-rec :  ⊦ run(sys, co ' + cl) = run(exec(sys, co) .1, cl);
      used for : s, ls;
       
      execl :  ⊦ execl(cl) = run(initialstate, cl);
      sources-base :  ⊦ sources([], d) = ∅ ++ d;
      used for : s, ls;
       
      sources-rec :  ⊦ sources(co ' + cl, d) = (((∃ d0. d0 ∈ sources(cl, d) ∧ cdom(co) ⇒ d0) ⊃ sources(cl, d) ++ cdom(co); sources(cl, d)));
      ipurge-base :  ⊦ ipurge([], d) = [];
      used for : s, ls;
       
      ipurge-rec :  ⊦ ipurge(co ' + cl, d) = ((cdom(co) ∈ sources(co + cl, d) ⊃ co + ipurge(cl, d); ipurge(cl, d)));
end enrich