[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification RG-I-n-Instance
instantiate parameter
   state+param
< 
   RG-I-2-Theory

with 
   CSPAWN+Preds

   
by mapping
      : param → nat; 
      : state → (nat → bool) × cstate; 
      pm → n2; 
      s → act, cs
   rename 
      RG-restr → RG-restr; 
      s0 → act4, cs4; 
      s1 → act5, cs5; 
      S → Act4, CS4; 
      I → IV; 
      Pre → Pre; 
      Pre1 → Pre1; 
      Pre2 → Pre2; 
      R → R; 
      G → G; 
      R1 → R1; 
      G1 → G1; 
      R2 → R2; 
      G2 → G2; 
      Post → Post; 
      Post1 → Post1; 
      Post2 → Post2
end instantiate