(*The worst case for 8-bit operands *) lemma"#255 $* #255 = #65025" by simp
lemma"#1359 $* #-2468 = #-3354012" by simp
(** Comparisons **)
lemma"(#89) $* #10 ≠ #889" by simp
lemma"(#13) $< #18 $- #4" by simp
lemma"(#-345) $< #-242 $+ #-100" by simp
lemma"(#13557456) $< #18678654" by simp
lemma"(#999999) $≤ (#1000001 $+ #1) $- #2" by simp
lemma"(#1234567) $≤ #1234567" by simp
(*** Quotient and remainder [they could be faster] ***)
lemma"#23 zdiv #3 = #7" by simp
lemma"#23 zmod #3 = #2" by simp
(** negative dividend **)
lemma"#-23 zdiv #3 = #-8" by simp
lemma"#-23 zmod #3 = #1" by simp
(** negative divisor **)
lemma"#23 zdiv #-3 = #-8" by simp
lemma"#23 zmod #-3 = #-1" by simp
(** negative dividend and divisor **)
lemma"#-23 zdiv #-3 = #7" by simp
lemma"#-23 zmod #-3 = #-2" by simp
end
Messung V0.5 in Prozent
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.12Bemerkung:
(vorverarbeitet am 2026-08-21)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
