Specification Bubblesort-row-rev

[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,

instantiate parameter
   gen-tord-min-max

< 
   Bubblesort-row
with 
   gen-tord-min-max

   
by mapping
      min → max; 
      max → min; 
      < → λ a, b. b < a; 
   rename 
      sort → sortrev; 
      ins≤ → ins≥; 
      merge → mergerev; 
      ordered≤ → ordered≥; 
      ordered< → ordered>; 
      psortrow# → psortrowrev#; 
end instantiate