[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 challenge1
enrich nat-array with
   
   functions 
      max : array × nat × nat → nat;
   
   axioms 
      max-in :  ⊦ n < m ∧ m ≤ # ar → (∃ n0. n ≤ n0 ∧ n0 < m ∧ ar[n0] = max(ar, n, m));
      max-gt :  ⊦ n < m ∧ m ≤ # ar → (∀ n0. n ≤ n0 ∧ n0 < m → ar[n0] ≤ max(ar, n, m));
   
end enrich