[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 context
enrich rawcontext , 
       value with
comment: structural recursive definition of (valid) contexts.;
   predicates 
      context : rawctxt;
   
   axioms 
      context-O :  ⊦ context(O);
      used for : s, ls;
       
       ⊦ context(C _ t) ↔ context(C);
      used for : s, ls;
       
       ⊦ context(t _ C) ↔ ¬ ¬ (context(C) ∧ value(t));
      comment: double negation indicates that we always want to expand the definition.;
      used for : s, ls;
       
end enrich