[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 reflist
actualize
   list-set
with
   genRef
   
by morphism
   :Elem → Ref; 
   :List → Reflist; 
   [] → []; 
    . + .  : (Elem × List → List) →  . + .  : (Ref × Reflist → Reflist); 
   # .  → # . ; 
    . ' →  . '; 
    . + .  : (List × List → List) →  . + .  : (Reflist × Reflist → Reflist); 
    . + .  : (List × Elem → List) →  . + .  : (Reflist × Ref → Reflist); 
    . +2 .  →  . +2 . ; 
    . ++ .  →  . ++ . ; 
   rmdup → rmdup; 
   rev → rev; 
   mklist → mklist; 
   fillfirst → fillfirst; 
    . -l .  →  . -l . ; 
    . -1l .  →  . -1l . ; 
    . -p .  →  . -p . ; 
   pos → pos; 
   frome → frome; 
    . ∪ .  →  . ∪ . ; 
    . \ .  →  . \ . ; 
   filter → filter; 
    . < .  : (List × List → Bool) →  . < .  : (Reflist × Reflist → Bool); 
    . ∈ .  →  . ∈ . ; 
   dups → dups; 
   disj → disj; 
    . ⊑ .  →  . ⊑ . ; 
    . ⊒ .  →  . ⊒ . ; 
    . ⊆ .  →  . ⊆ . ; 
    . head → hd . ; 
    . tail → tl . ; 
    . last →  . last; 
    . butlast →  . butlast; 
   butlastn → butlastn; 
    . ( . )  →  . ( . ) ; 
    . (. := .)  →  . (. := .) ; 
   firstn → firstn; 
   restn → restn; 
   lastn → lastn; 
   sublist → sublist; 
end actualize