Specification rawcontext

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

data specification 
   comment: Definition of raw contexts as a free data type.
Instead of □ (reserved for temporal logic) we use O.
Cf and Ca test whether function/argument is the context;
   using nat , 
         term
   rawctxt = O |  . _ . (.c : rawctxt;  . .t : term) prio 9 left  with Cf |  . _ . ( . .t : term; .c : rawctxt) prio 9 left  with Ca;
   variables 
      C : rawctxt; 
   size functions # : rawctxt → nat;
end data specification