Specification wellfounded-TL

[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
   wellfounded, 
   nat-basic
with
   variables 
       a : elem;
       A : elem flexible;
       N : nat flexible;
   
   
   theorems 
      not-always-decrease: □ ⟨a := A⟩ (◇ A ≪ a) ⊦ ;
      
      always-noincrease-stable: □ (A'' ≪ A ∨ A'' = A) ⊦ ◇ □ A'' = A;
   
   
end enrich