[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 value
enrich term with
comment: structural recursive definition of value predicate.;
   predicates 
      value : term;
   variables 
      t1, t2 : term; 
   
   axioms 
      val-K :  ⊦ value(K);
      used for : s, ls;
       
      val-S :  ⊦ value(S);
      used for : s, ls;
       
      val-K-ap :  ⊦ value(K _ t) ↔ value(t);
      used for : s, ls;
       
      val-S-ap :  ⊦ value(S _ t) ↔ value(t);
      used for : s, ls;
       
      val-other-ap :  ⊦ t1 ≠ K ∧ t1 ≠ S → (value(t1 _ t2) ↔ ¬ ¬ (ap(t1) ∧ t1 .1 = S ∧ value(t2) ∧ value(t1 .2)));
      comment: the double negation indicates that we always unfold the definition in this case.;
      used for : s, ls;
       
end enrich