		Search-engine friendly clone of the ACL2 documentation.

Monotonicity-properties-of-ash

Lemmas about (ash a b) versus (ash a c).

These are basic lemmas about:

(< (ASH A B) (ASH A C))
(= (ASH A B) (ASH A C))

BOZO these only address when A is positive and B/C are naturals. We should extend these to negative numbers.

Definitions and Theorems

Theorem: (< (ash a b) (ash a c))

(defthm |(< (ash a b) (ash a c))|
        (implies (and (posp a) (natp b) (natp c))
                 (equal (< (ash a b) (ash a c))
                        (< b c))))

Theorem: (= (ash a b) (ash a c))

(defthm |(= (ash a b) (ash a c))|
        (implies (and (posp a) (natp b) (natp c))
                 (equal (equal (ash a b) (ash a c))
                        (equal b c))))