Specification string-append

[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,

enrich
   string-data
with
   

   
   
   functions  . + . : string × string → string;
              . ' : char → string;
   
   
   variables  stringvar : string;
              stringvar0 : string;
   
   

   

   axioms chartostring :  ⊦ char ' = char + "";
          append-base :  ⊦ "" + str = str;
          append-rec :  ⊦ (char + str) + str0 = char + (str + str0);

   

   
end enrich