Lines Matching defs:modaux
52 (defthm modaux-1a
58 (defthm modaux-1b
63 :hints (("Goal" :use ((:instance modaux-1a
66 (defthm modaux-1c
72 (defthm modaux-2a
79 (defthm modaux-2b
85 :hints (("Goal" :use (modaux-2a))))
93 :hints (("Goal" :use ((:instance modaux-1a
113 (defthm modaux-2c
121 (defthmd modaux-2d
129 ("Subgoal 2'" :use ((:instance modaux-1b
581 :hints (("Subgoal 2" :use ((:instance modaux-1b
601 :hints (("Subgoal 1.2'" :use ((:instance modaux-1b
603 ("Subgoal 1''" :use ((:instance modaux-2d