[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 wlarray
enrich
   wlarray-base, 
   nat-set

with
   

   
   
   functions  free-ecs : wlarray → nat-set;
              used-ecs : wlarray → nat-set;
              free-ecs : wlarray × nat → nat-set;
              used-ecs : wlarray × nat → nat-set;
              below : nat-set × nat → nat-set;
   predicates  same-used : wlarray × wlarray;
   
   
   
   

   

   axioms free-ecs-base :  ⊦ free-ecs(wlar, 0) = ∅;
          used for: s, ls;
          free-ecs-rec :  ⊦ n < # wlar → free-ecs(wlar, n + 1) = (wlar[n].status = free ⊃ free-ecs(wlar, n) ++ wlar[n].ec;free-ecs(wlar, n));
          used for: ls;
          free-ecs :  ⊦ free-ecs(wlar) = free-ecs(wlar, # wlar);
          used for: ls;
          used-ecs-base :  ⊦ used-ecs(wlar, 0) = ∅;
          used for: s, ls;
          used-ecs-rec :  ⊦ n < # wlar → used-ecs(wlar, n + 1) = (wlar[n].status = used ⊃ used-ecs(wlar, n) ++ wlar[n].ec;used-ecs(wlar, n));
          used for: ls;
          used-ecs :  ⊦ used-ecs(wlar) = used-ecs(wlar, # wlar);
          used for: ls;
          below-base :  ⊦ below(∅, m) = ∅;
          used for: s, ls;
          below-rec :  ⊦ below(ns ++ n, m) = (n < m ⊃ below(ns -- n, m) ++ n;below(ns -- n, m));
          used for: ls;
          same-used
          :  ⊦ same-used(wlar0, wlar1) ↔ # wlar0 = # wlar1 ∧ (∀ n. n < # wlar0 → (wlar0[n].status = used ↔ wlar1[n].status = used));
          used for: ls;

   

   
end enrich