Lines Matching refs:prefix
27 |- !E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))
31 ``!E E'. OBS_CONGR (sum E (prefix tau (sum E' E))) (prefix tau (sum E' E))``,
89 ``!p q. (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q) \/
90 OBS_CONGR (prefix tau p) q) ==> WEAK_EQUIV p q``,
107 ``!p q. WEAK_EQUIV p q ==> (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q)
108 \/ OBS_CONGR (prefix tau p) q)``,
122 take [`prefix tau q`, `q`] \\
150 take [`prefix tau p`, `p`] \\
162 ``!p q. WEAK_EQUIV p q = (OBS_CONGR p q \/ OBS_CONGR p (prefix tau q)
163 \/ OBS_CONGR (prefix tau p) q)``,
231 ASSUME_TAC (Q.SPEC `prefix (label a) nil`
234 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) nil`)) \\
239 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil))
240 (sum q (prefix (label a) nil))``)) \\
251 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau u``
263 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a) nil))
264 (sum q (prefix (label a) nil))``)) \\
268 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau E'``
277 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) (label L) E'``
291 ASSUME_TAC (Q.SPEC `prefix (label a') nil`
294 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a') nil`)) \\
299 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil))
300 (sum q (prefix (label a') nil))``)) \\
311 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau u``
323 (ASSUME ``WEAK_EQUIV (sum p (prefix (label a') nil))
324 (sum q (prefix (label a') nil))``)) \\
328 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau E'``
337 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) (label L) E'``
377 (ASSUME_TAC o (Q.SPEC `prefix (label a) k`))
382 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\
383 PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum q (prefix (label a) k))``
388 PAT_X_ASSUM ``EPS (sum q (prefix (label a) k)) E2``
398 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau u``
413 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'``
421 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label a) E'``
435 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E'``
443 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label x) E'``
452 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\
453 PAT_X_ASSUM ``WEAK_EQUIV (sum p (prefix (label a) k)) (sum h (prefix (label a) k))``
458 PAT_X_ASSUM ``EPS (sum p (prefix (label a) k)) E1``
469 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau u``
484 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'``
492 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label a) E'``
506 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'``
514 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label x) E'``
528 (KLOP a (SUC n) = sum (KLOP a n) (prefix (label a) (KLOP a n))) `;
855 KLOP_INF X a = rec X (sum (var X) (prefix (label a) (var X)))`;