Lines Matching refs:to
42 * Set default parsing to natural numbers rather than integers
56 * pureDefine doesn't export definitions to theCompset (for EVAL).
133 ?k :: (0 to LENGTH w).
134 OLD_UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). OLD_UF_SEM (RESTN w j) f1)
137 !j :: (0 to LENGTH w).
141 !j :: (0 to LENGTH w).
144 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
147 !j :: (0 to LENGTH w).
150 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
152 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
159 ?j :: (1 to LENGTH w).
185 ?k :: (0 to LENGTH w).
186 UF_SEM (RESTN w k) f2 /\ !j :: (0 to k). UF_SEM (RESTN w j) f1)
189 !j :: (0 to LENGTH w).
193 !j :: (0 to LENGTH w).
196 ?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
199 !j :: (0 to LENGTH w).
202 ((?k :: (j to LENGTH w). US_SEM (SEL w (j,k)) r2)
204 (!k :: (j to LENGTH w). ?w'. US_SEM (SEL w (j,k) <> w') r2)))
211 ?j :: (1 to LENGTH w).
217 * PATH M p is true iff p is a path with respect to transition relation M.R
237 ?k :: (0 to LENGTH p). O_SEM M f2 (ELEM p k) /\ !j. j < k ==> O_SEM M f1 (ELEM p j))
240 ?p. PATH M p s /\ !j :: (0 to LENGTH p). O_SEM M f (ELEM p j))`;