[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 instance
instantiate parameter
   state

< 
   RG2-Theory

with 
   implementation


   
by mapping
      : state → nat × nat; 
      s → n, m; 
      s0 → n0, m0; 
      s1 → n1, m1; 
      s2 → n2, m2; 
      S → N, M
   rename 
      RG-restr → RG-restr; 
      R → R; 
      G → G; 
      R1 → R1; 
      G1 → G1; 
      R2 → R2; 
      G2 → G2; 
      Init → Init; 
      Inv → Inv; 
      Pre → Pre; 
      Pre1 → Pre1; 
      Pre2 → Pre2; 
      Post → Post; 
      Post1 → Post1; 
      Post2 → Post2
end instantiate