Lines Matching refs:f2
14 `finalForms f = {U f1 f2 | (U f1 f2) ��� tempSubForms f}`;
23 /\ (trans �� (CONJ f1 f2) = d_conj (trans �� f1) (trans �� f2))
24 /\ (trans �� (DISJ f1 f2) = (trans �� f1) ��� (trans �� f2))
26 /\ (trans �� (U f1 f2) = (trans �� f2) ��� (d_conj (trans �� f1) {(��,{U f1 f2})}))
27 /\ (trans �� (R f1 f2) = d_conj (trans �� f2) ((trans �� f1) ��� {(��,{R f1 f2})}))`;
52 rename [���(a1,e1) ��� trans �� f1���, ���a = a1 ��� a2���, ���(a2,e2) ��� trans �� f2���]
61 (e2 = {x | ���s. s ��� t' ��� x ��� s}) ��� e' ��� tempDNF f2 ���
251 ``!a r f f' f1 f2 w l qs.(runForAA (ltl2vwaa_free_alph (POW (props f')) f2) r w
423 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) f2).final`
438 >> `r.V i ��� tempSubForms f2` by fs[validAARunFor_def]
445 ``!a r f f1 f2 w l.(runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w
446 /\ (a,r.E (l,U f1 f2)) ���
447 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})}
451 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2))))
468 >> qabbrev_tac `h' = (\q. if (q = X (U f1 f2)) then {U f1 f2} else h q)`
469 >> qabbrev_tac `e' = e ��� {X (U f1 f2)}`
470 >> `!q. q ��� e' ==> ((h' q = h q) \/ (h' q = {U f1 f2}))`
472 >> `!q. q ��� e' ==> h' q ��� (h q ��� {U f1 f2})`
475 >> `!q. q ��� e ==> h' q ��� h q ��� {U f1 f2}`
477 >> `!q. q ��� e ==> h' q ��� e1 ��� {U f1 f2}` by metis_tac[SUBS_UNION_LEMM2]
478 >> `!q. q ��� e' ==> q ��� e \/ (q = X (U f1 f2))` by metis_tac[IN_UNION, IN_SING]
479 >> `!q. q ��� e' ==> h' q ��� e1 ��� {U f1 f2}` by
485 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) r' (suff w l)
487 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))).final`
490 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).final`
496 validAARunFor (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w
515 >- (`x ��� e \/ (x = (X (U f1 f2)))` by metis_tac[] >> fs[]
522 >> `x ��� tempSubForms (U f1 f2)` by metis_tac[SUBSET_DEF]
528 >> Cases_on `q = X (U f1 f2)`
615 >> `tempSubForms (CONJ f1 (X (U f1 f2)))
616 = {X (U f1 f2)} ��� tempSubForms (U f1 f2)` by
618 >> `U f1' f2' ��� {X (U f1 f2)} ��� tempSubForms (U f1 f2)` by fs[]
619 >> `~(X (U f1 f2) = U f1' f2')` by rw[]
620 >> `U f1' f2' ��� tempSubForms (U f1 f2)` by metis_tac[IN_UNION,IN_SING]
627 ``!a r f f1 f2 w l.(runForAA (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w
628 /\ (a,r.E (l,R f1 f2)) ���
629 d_conj (trans (POW (props f)) f2) {(POW (props f), {R f1 f2})}
633 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2))))
637 (e1 = BIGUNION t) ��� e ��� tempDNF f2 ��� (a1 = BIGINTER a') ���
650 >> qabbrev_tac `h' = (\q. if (q = X (R f1 f2)) then {R f1 f2} else h q)`
651 >> qabbrev_tac `e' = e ��� {X (R f1 f2)}`
652 >> `!q. q ��� e' ==> ((h' q = h q) \/ (h' q = {R f1 f2}))`
654 >> `!q. q ��� e' ==> h' q ��� (h q ��� {R f1 f2})`
657 >> `!q. q ��� e ==> h' q ��� h q ��� {R f1 f2}`
659 >> `!q. q ��� e ==> h' q ��� e1 ��� {R f1 f2}` by metis_tac[SUBS_UNION_LEMM2]
660 >> `!q. q ��� e' ==> q ��� e \/ (q = X (R f1 f2))` by metis_tac[IN_UNION, IN_SING]
661 >> `!q. q ��� e' ==> h' q ��� e1 ��� {R f1 f2}` by
667 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r' (suff w l)
669 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))).final`
672 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)).final`
678 validAARunFor (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w
697 >- (`x ��� e \/ (x = (X (R f1 f2)))` by metis_tac[] >> fs[]
698 >> `e ��� tempSubForms f2` by metis_tac[TEMPDNF_TEMPSUBF]
704 >> `x ��� tempSubForms (R f1 f2)` by metis_tac[SUBSET_DEF]
710 >> Cases_on `q = X (R f1 f2)`
797 >> `tempSubForms (CONJ f2 (X (R f1 f2)))
798 = {X (R f1 f2)} ��� tempSubForms (R f1 f2)` by
800 >> `U f1' f2' ��� {X (R f1 f2)} ��� tempSubForms (R f1 f2)` by fs[]
801 >> `~(X (R f1 f2) = U f1' f2')` by rw[]
802 >> `U f1' f2' ��� tempSubForms (R f1 f2)` by metis_tac[IN_UNION,IN_SING]
809 ``!f1 f2 f w run.
811 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run w
813 ==> runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w``,
822 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w
824 ==> (x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final))`
832 >> `���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[]
833 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[]
845 x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final`
847 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w
849 ==> (x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final))`
857 >> `���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[]
858 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[]
861 >> `b i ��� tempSubForms f2` by metis_tac[SUBSET_DEF]
869 ``!f f1 f2 run w.
870 runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)) run w
872 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run w
876 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (DISJ f1 f2)).final`
885 ���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1) `
900 >- (`(���i. run.V i ��� tempSubForms f2) ���
903 ���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2) `
913 >> `(q',f2) ��� TSF` by metis_tac[TSF_def, IN_DEF]
922 ``!r w f f' f1 f2 a p.
1018 >> `x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f`
1030 ``!f1 f2 f w.
1032 /\ (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r w)
1033 ==> (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r w)``,
1035 >> `?r. validAARunFor (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r w
1037 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)).final)`
1047 >> `r.V i ��� (tempSubForms f1 ��� tempSubForms f2)`
1049 >> `r'.V i ��� (tempSubForms f1 ��� tempSubForms f2)`
1051 >> `r.V i ��� r'.V i ��� (tempSubForms f1 ��� tempSubForms f2)`
1092 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final`
1097 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[]
1099 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f1` by metis_tac[]
1100 >> `U f1' f2' ��� tempSubForms f1` by metis_tac[]
1104 {U f1' f2 | U f1' f2 ��� tempSubForms f1}
1111 >- (`���f1' f2'. x ��� U f1' f2' ��� U f1' f2' ��� tempSubForms f2` by metis_tac[]
1112 >> `U f1' f2' ��� tempSubForms f2` by metis_tac[]
1114 >> `(���i. r'.V i ��� (ALTER_A (tempSubForms f2) (POW (props f))
1116 (initForms f2)
1117 {U f1 f2' | U f1 f2' ��� tempSubForms f2}
1122 >- (`���f1 f2'. x ��� U f1 f2' ��� U f1 f2' ��� tempSubForms f2` by metis_tac[]
1130 ``!f1 f2 f w run.
1131 runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) run w
1133 /\ (?r2. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r2 w
1137 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)).final)`
1148 (validAARunFor (ltl2vwaa_free_alph (POW (props f)) f2) r2 w ���
1150 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) f2).final)) ���
1207 >> `(q,f2) ��� TSF` by metis_tac[TSF_def,IN_DEF,SUBSET_DEF]
1406 ``!x f f1 f2 f3.
1407 (?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (DISJ f2 f3))) r x)
1408 = ((?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r x)
1413 >- (`���r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 f2)) r x`
1419 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f2 f3)) r x`
1424 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (DISJ f2 f3)) r x`
1433 ``!f f1 f2.
1434 (alterA_lang (ltl2vwaa_free_alph (POW (props f)) (U f1 f2))
1436 (DISJ f2 (CONJ f1 (X (U f1 f2))))))``,
1442 (DISJ f2 (CONJ f1 (X (U f1 f2))))) run x) ���
1447 (DISJ f2 (CONJ f1 (X (U f1 f2))))).alphabet`
1451 >> `!a. (a,run.E (0,U f1 f2)) ��� trans (POW (props f)) f2 ��� at x 0 ��� a ���
1452 ���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' x`
1454 >> `!a. (a,run.E (0,U f1 f2)) ���
1455 d_conj (trans (POW (props f)) f1) {(POW (props f),{U f1 f2})}
1458 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) r' x`
1466 >> `(U f1 f2) ��� run.V 0` by simp[]
1467 >> `���a. ((a,run.E (0,U f1 f2)) ��� trans (POW (props f)) (U f1 f2)) ��� (at x 0 ��� a)`
1470 >- (`���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' x`
1476 (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2))))
1486 runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) run x) ���
1489 x' ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).alphabet` suffices_by metis_tac[]
1491 >> `runForAA (ltl2vwaa_free_alph (POW (props f)) f2) run x
1492 \/ runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f1 (X (U f1 f2)))) run x`
1494 >> `{U f1 f2} ��� tempDNF (U f1 f2)` by fs[tempDNF_def]
1495 >- (`?a. (a,run.V 1) ��� trans (POW (props f)) (U f1 f2) ��� at x 0 ��� a`
1497 >> `run.V 0 ��� tempDNF f2 ���
1498 ���a. (a,run.V 1) ��� trans (POW (props f)) f2 ��� at x 0 ��� a`
1502 >> `?a. (a,run.V 1) ��� trans (POW (props f)) f2 /\ (at x 0 ��� a)`
1504 >> `���a. (a,run.V 1) ��� trans (POW (props f)) f2 ��� (at x 0 ��� a)`
1507 >- (`?a. (a,run.V 1) ��� trans (POW (props f)) (U f1 f2) ��� at x 0 ��� a`
1509 >> `run.V 0 ��� tempDNF (CONJ f1 (X (U f1 f2))) ���
1510 ���a. (a,run.V 1) ��� trans (POW (props f)) (CONJ f1 (X (U f1 f2)))
1516 d_conj (trans (POW (props f)) f1) {(POW (props f),{U f1 f2})}
1521 (��s. ���e. (s = (POW (props f),e)) ��� e ��� tempDNF (U f1 f2)) ���
1524 >> `(��s. (s = (POW (props f),{U f1 f2})))
1525 = {(POW (props f), {U f1 f2})}` by
1536 ``!f f1 f2. alterA_lang (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) =
1538 (CONJ f2 (DISJ f1 (X (R f1 f2)))))``,
1544 (CONJ f2 (DISJ f1 (X (R f1 f2))))) run x) ���
1549 (CONJ f2 (DISJ f1 (X (R f1 f2))))).alphabet`
1552 >> `!a qs f1 f2.
1553 (a,qs) ��� trans (POW (props f)) f1 ��� at x 0 ��� a ��� qs ��� run.E (0,f2) ���
1556 >> `!a. (a,run.E (0,R f1 f2)) ���
1557 d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})} ���
1561 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r'
1570 >- (`?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 f1)) r x
1572 (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 (X (R f1 f2)))) r x`
1575 >> `R f1 f2 ��� run.V 0` by metis_tac[IN_SING]
1576 >> `���a. (a,run.E (0,R f1 f2)) ��� trans (POW (props f)) (R f1 f2)
1580 >> `((a,run.E (0,R f1 f2)) ���
1581 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1))
1582 \/ (a,run.E (0,R f1 f2)) ���
1583 d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}`
1589 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff x 0)`
1593 >> `?r. runForAA (ltl2vwaa_free_alph (POW (props f)) (CONJ f2 f1)) r x`
1606 (R f1 f2)) run x) ���
1611 (R f1 f2)).alphabet`
1613 >- (`{R f1 f2} ��� tempDNF (R f1 f2)` by fs[tempDNF_def]
1614 >> `run.V 0 ��� tempDNF (CONJ f2 (DISJ f1 (X (R f1 f2)))) ���
1616 (CONJ f2 (DISJ f1 (X (R f1 f2))))
1618 >> `?a.(a,run.V 1) ��� trans (POW (props f)) (R f1 f2) ��� at x 0 ��� a`
1623 trans (POW (props f)) (CONJ f2 (DISJ f1 (X (R f1 f2))))
1627 >> `(��s. s = (POW (props f),{R f1 f2}))
1628 = {(POW (props f),{R f1 f2})}` suffices_by (rpt strip_tac >> fs[])
1699 >> `x' ��� {U f1 f2 | U f1 f2 ��� tempSubForms (X g)}`
1701 >> `x' ��� {U f1 f2 | U f1 f2 ��� tempSubForms g}` by fs[tempSubForms_def]
1806 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w
1807 ==> (?n a. (a, r.E (n, U f1 f2)) ��� trans (POW (props f)) f2
1811 ��� x ��� (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)).final`
1815 >> `!i. U f1 f2 ��� r.V i` by (
1817 >> `���a. (a,r.E (i,U f1 f2)) ��� trans (POW (props f)) (U f1 f2)
1822 >> `U f1 f2 ��� r.E (i, U f1 f2)` by metis_tac[IN_UNION, IN_SING]
1823 >> `U f1 f2 ��� r.V (i + 1)` by metis_tac[SUBSET_DEF]
1827 >> `!i. U f1 f2 ��� r.E (i, U f1 f2)` by (
1830 >> `(i = 0) ��� ���q'. (U f1 f2) ��� r.E (i ��� 1,q') ��� q' ��� r.V (i ��� 1)`
1833 >> `U f1 f2 ��� r.V 0` by metis_tac[IN_SING]
1834 >> `(1 = 0) ��� ���q'. (U f1 f2) ��� r.E (1 ��� 1,q') ��� q' ��� r.V (1 ��� 1)`
1836 >> `q' = U f1 f2` by metis_tac[IN_SING] >> fs[]
1838 >- (`U f1 f2 ��� r.V i` by fs[]
1839 >> `���a. (a,r.E (i,(U f1 f2))) ��� trans (POW (props f)) (U f1 f2)
1844 >> `U f1 f2 ��� r.E (i, U f1 f2)` by metis_tac[IN_UNION, IN_SING]
1845 >> `U f1 f2 ��� r.V (i + 1)` by metis_tac[SUBSET_DEF]
1850 >> `infBranchOf r (\_. U f1 f2)` by fs[infBranchOf_def]
1851 >> `branchFixP (\_. U f1 f2) (U f1 f2)` by fs[branchFixP_def]
1853 >> `U f1 f2 ��� U f1 f2 ��� U f1 f2 ��� tempSubForms (U f1 f2)`
1860 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w
1861 ==> ?n a. (a, r.E (n, U f1 f2)) ��� trans (POW (props f)) f2
1863 ��� (!i. i < n ==> ?a'. (a', r.E (i, U f1 f2)) ���
1864 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})}
1869 (a,r.E (n,U f1 f2)) ��� trans (POW (props f)) f2 ���
1874 >> `!j. j < N ==> U f1 f2 ��� r.V j` by (
1880 >> `���a'. (a',r.E (j,U f1 f2)) ��� trans (POW (props f)) (U f1 f2) ��� at w j ��� a'`
1888 >> `U f1 f2 ��� r.V i` by fs[]
1890 >> `���a'. (a',r.E (i,(U f1 f2))) ��� trans (POW (props f)) (U f1 f2) ��� at w i ��� a'`
1898 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (U f1 f2)) r w
1899 ==> ?r' n. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff w n)
1902 >> `���n a. (a,r.E (n,U f1 f2)) ��� trans (POW (props f)) f2 ��� at w n ��� a
1903 ��� (!i. i < n ==> ?a'. (a', r.E (i, U f1 f2)) ���
1904 d_conj (trans (POW (props f)) f1) {(POW (props f), {U f1 f2})}
1907 >> `���r'. runForAA (ltl2vwaa_free_alph (POW (props f)) f2) r' (suff w n)`
1912 (a',r.E (i,U f1 f2)) ���
1914 {(POW (props f),{U f1 f2})} ��� at w i ��� a'`
1921 always_run_cond f1 f2 rs s i q =
1923 then (if q = R f1 f2
1924 then {R f1 f2} ��� ((rs i).V 1)
1930 (always_run_V f1 f2 rs 0 = {R f1 f2})
1931 ��� (always_run_V f1 f2 rs (SUC i) =
1932 {R f1 f2} ��� {q | ?q'. q' ��� always_run_V f1 f2 rs i
1933 ��� q ��� always_run_cond f1 f2 rs (always_run_V f1 f2 rs i) i q'}
1937 always_run_E f1 f2 rs (i,q) =
1938 always_run_cond f1 f2 rs (always_run_V f1 f2 rs i) i q`
1941 always_run f1 f2 rs = ALTERA_RUN (always_run_V f1 f2 rs) (always_run_E f1 f2 rs)`
1945 ``���f' f1 f2 w rs.
1946 (!n. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n))
1947 ==> (!i q. q ��� always_run_V f1 f2 rs i /\ ~(q = R f1 f2)
1951 >> Cases_on `q' = R f1 f2`
1952 >- (`q ��� {R f1 f2} ��� (rs i).V 1` by metis_tac[always_run_cond_def]
1989 ``���f' f1 f2 w rs.
1990 (!n .runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n))
1991 ==> (!i q. q ��� always_run_V f1 f2 rs i /\ ~(q = R f1 f2)
1997 >- (rpt strip_tac >> fs[always_run_V_def] >> Cases_on `q' = R f1 f2`
1998 >- (`q ��� {R f1 f2} ��� (rs i).V 1`
2064 ``���f' f1 f2 w rs.
2065 (!n .runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n))
2066 ��� validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) (always_run f1 f2 rs) w
2067 ==> (!b x. infBranchOf (always_run f1 f2 rs) b ��� branchFixP b x
2068 ��� ~(x = R f1 f2)
2073 >> `!m. m >= i ==> x ��� (always_run f1 f2 rs).V m` by metis_tac[]
2083 >> `x ��� (always_run f1 f2 rs).E (k, x)` by (
2146 >> `x ��� always_run_V f1 f2 rs j` by fs[]
2147 >> `x ��� always_run_V f1 f2 rs (a + j)` by fs[]
2152 >> `x ��� always_run_E f1 f2 rs (a + j, x)` by metis_tac[]
2162 >> `validAARunFor (ltl2vwaa_free_alph (POW (props f')) f2) (rs (N j)) (suff w (N j))`
2178 ``!f' f1 f2 w. (word_range w ��� POW (props f')) ���
2179 (!n. ?r. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) r (suff w n))
2180 ==> (?r. runForAA (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)) r w)``,
2182 >> `?rs. !n. runForAA (ltl2vwaa_free_alph (POW (props f')) f2) (rs n) (suff w n)`
2184 >> qexists_tac `always_run f1 f2 rs`
2185 >> `!n. ((rs n).V 0) ��� tempDNF f2
2186 ==> ���a. (a,(rs n).V 1) ��� trans (POW (props f')) f2 ��� at (suff w n) 0 ��� a`
2189 >> `(validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2))
2190 (always_run f1 f2 rs) w)
2191 ��� ((validAARunFor (ltl2vwaa_free_alph (POW (props f')) (R f1 f2))
2192 (always_run f1 f2 rs) w)
2193 ==> acceptingAARun (ltl2vwaa_free_alph (POW (props f')) (R f1 f2))
2194 (always_run f1 f2 rs))` suffices_by metis_tac[]
2204 >> `((q' = R f1 f2) ��� q' ��� tempSubForms f1) ��� q' ��� tempSubForms f2`
2207 >> `x ��� {R f1 f2} ��� (rs i).V 1` by metis_tac[]
2208 >> `x ��� {R f1 f2} \/ x ��� (rs i).V 1`
2212 >> `(rs i).V 0 ��� tempDNF f2`
2219 >- (`~(q' = R f1 f2)` by (
2221 >> `R f1 f2 ��� subForms f1` by metis_tac[TSF_IMPL_SF]
2222 >> `f1 ��� subForms (R f1 f2)`
2224 >> `f1 = R f1 f2` by metis_tac[SF_ANTISYM_LEMM]
2242 >- (`~(q' = R f1 f2)` by (
2244 >> `R f1 f2 ��� subForms f2` by metis_tac[TSF_IMPL_SF]
2245 >> `f2 ��� subForms (R f1 f2)`
2247 >> `f2 = R f1 f2` by metis_tac[SF_ANTISYM_LEMM]
2266 >- (Cases_on `q = R f1 f2`
2272 (a,(rs i).V 1) ��� trans (POW (props f')) f2 ���
2297 >> `x ��� always_run_V f1 f2 rs (SUC i)`
2300 >> Cases_on `x = R f1 f2` >> fs[]
2301 >> Cases_on `q = R f1 f2`
2313 >> `!i. R f1 f2 ��� (always_run f1 f2 rs).V i` by (
2317 >- (qexists_tac `R f1 f2`
2325 >> `���b x. infBranchOf (always_run f1 f2 rs) b ��� branchFixP b x
2326 ��� x ��� (ltl2vwaa_free_alph (POW (props f')) (R f1 f2)).final`
2329 >> Cases_on `x = R f1 f2`
2334 >> `x ��� (ltl2vwaa_free_alph (POW (props f')) f2).final`
2337 >> `U f1' f2' ��� tempSubForms f2` suffices_by metis_tac[]
2338 >> `?i. U f1' f2' ��� (always_run f1 f2 rs).V i`
2340 >> `~(U f1' f2' = R f1 f2)` by simp[]
2342 >> `(U f1' f2') ���
2343 (rs (LEAST j. (U f1' f2') ��� (rs j).V (i' ��� j))).V
2344 (i' ��� LEAST j. (U f1' f2') ��� (rs j).V (i' ��� j))`
2346 >> qabbrev_tac `N = LEAST j. U f1' f2' ��� (rs j).V (i' ��� j)`
2347 >> `(rs N).V (i' - N ) ��� tempSubForms f2`
2356 ``!f f1 f2 r w. runForAA (ltl2vwaa_free_alph (POW (props f)) (R f1 f2)) r w
2357 ==> ((!n. ?a. (a, r.E (n, R f1 f2)) ���
2358 d_conj (trans (POW (props f)) f2) {(POW (props f), {R f1 f2})}
2360 (?n a. (a, r.E (n, R f1 f2)) ��� trans (POW (props f)) (CONJ f1 f2)
2362 rpt strip_tac >> Cases_on `!i. R f1 f2 ��� r.V i`
2365 >> `R f1 f2 ��� r.V n` by metis_tac[]
2366 >> `���a. (a,r.E (n,R f1 f2)) ��� trans (POW (props f)) (R f1 f2) ��� at w n ��� a`
2370 >> `R f1 f2 ��� r.V (n+1)` by metis_tac[]
2371 >> `((n + 1) = 0) ��� ���q'. (R f1 f2) ��� r.E ((n + 1) ��� 1,q') ��� q' ��� r.V ((n + 1) ��� 1)`
2373 >> `q' = R f1 f2` by (
2374 `q' ��� tempSubForms (R f1 f2)` by metis_tac[SUBSET_DEF]
2377 >> `(R f1 f2,q') ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS]
2380 >> `(a,r.E (n,R f1 f2)) ���
2381 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1)
2382 ��� d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}`
2386 >> (`!q. (q ��� e1) ==> (q,f2) ��� TSF` by metis_tac[TRANS_REACHES_SUBFORMS]
2388 >> `R f1 f2 ��� e1 \/ R f1 f2 ��� e2` by metis_tac[IN_UNION]
2389 >- (`R f1 f2 ��� tempSubForms f2` by metis_tac[TSF_def, IN_DEF]
2390 >> `R f1 f2 ��� subForms f2` by metis_tac[TSF_IMPL_SF]
2391 >> `f2 ��� subForms (R f1 f2)` by fs[subForms_def, SUBFORMS_REFL]
2392 >> `R f1 f2 = f2` by metis_tac[SF_ANTISYM_LEMM]
2396 >- (`R f1 f2 ��� tempSubForms f1` by metis_tac[TSF_def, IN_DEF]
2397 >> `R f1 f2 ��� subForms f1` by metis_tac[TSF_IMPL_SF]
2398 >> `f1 ��� subForms (R f1 f2)` by fs[subForms_def, SUBFORMS_REFL]
2399 >> `R f1 f2 = f1` by metis_tac[SF_ANTISYM_LEMM]
2407 >> qabbrev_tac `N = LEAST j. ~(R f1 f2 ��� r.V j)`
2409 >> `R f1 f2 ��� r.V 0`
2411 >> `R f1 f2 ��� r.V (N - 1)` by (
2420 >> `���a. (a,r.E (N-1,(R f1 f2))) ��� trans (POW (props f)) (R f1 f2) ��� at w (N-1) ��� a`
2424 >> `(a,r.E (N -1,R f1 f2)) ���
2425 d_conj (trans (POW (props f)) f2) (trans (POW (props f)) f1)
2426 ��� d_conj (trans (POW (props f)) f2) {(POW (props f),{R f1 f2})}`
2431 >> `r.E (N - 1, R f1 f2) ��� r.V (N - 1 + 1)` by metis_tac[]
2433 >> `~(R f1 f2 ��� r.V N)` by (
2440 >> `R f1 f2 ��� r.V N` by metis_tac[IN_UNION,SUBSET_DEF,IN_SING]