Lines Matching defs:loop
135 (ILOAD 0) ;;; 2 while ; loop: pc=2
145 (GOTO -10) ;;; 12 } ; jump to loop
240 (defun ifact-loop-sched (n)
244 (ifact-loop-sched (- n 1)))))
247 ; at the loop pc = 2: If n is 0, schedule 4 steps, namely the
257 (ifact-loop-sched n)))
766 :rule-classes ((:rewrite :loop-stopper ((i j update-nth)))))
783 ; loop). In particular, define a scheduler function that
789 ; loop.
833 (ILOAD 0) ;;; 2 (while ; loop: pc=2
843 (GOTO -10) ;;; 12 ) ; jump to loop
848 ; [3] Specify how long it takes to execute (starting with the loop).
852 (defun ifact-loop-sched (n)
856 (ifact-loop-sched (- n 1)))))
860 (ifact-loop-sched n)))
889 ; [5] Prove your program does what it does, starting with the loop.
891 (defthm ifact-loop-lemma
894 (equal (run (ifact-loop-sched n)