Lines Matching defs:the
7 % This theory identifies the term "((t1 + 1) ... + 1)" with t2 %
8 % for each of the fifteen possible execution cycles from results in %
9 % 'proof1', lemmas about the 'NEXT' relation, and the assumption %
10 % "NEXT (t1,t2) ready". The theorems about each of the the execution %
18 % the memory, program counter, accumulator, and idle status. Other %
19 % results from 'proof1' (eg. the status of 'ready' and the other %
20 % registers) are not required beyond this step in the proof. %