src/deep_embeddings/ctl_starScript.sml

42             | CTL_STAR_AND        of ctl_star # ctl_star         (* f1 \wedge f2            *)
44             | CTL_STAR_PSUNTIL    of ctl_star # ctl_star         (* f1 U f2                 *)
46             | CTL_STAR_SUNTIL     of ctl_star # ctl_star         (* f1 U f2                 *)
63          [`P`,`\(f1,f2). P f1 /\ P f2`]
71    (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_AND(f1,f2)) p = CTL_STAR_SEM_PATH_TIME t M f1 p /\ CTL_STAR_SEM_PATH_TIME t M f2 p) /\
76    (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_SUNTIL(f1,f2)) p = (?k. k >= t /\ CTL_STAR_SEM_PATH_TIME k M f2 p /\
78    (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_PSUNTIL(f1,f2)) p = (?k. k <= t /\ CTL_STAR_SEM_PATH_TIME k M f2 p /\
92    (CTL_STAR_SEM_STATE M (CTL_STAR_AND(f1,f2)) s = CTL_STAR_SEM_STATE M f1 s /\ CTL_STAR_SEM_STATE M f2 s) /\
106    (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2) /\
110    (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2) /\
111    (IS_CTL_STAR_PATH_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = IS_CTL_STAR_PATH_FORMULA f1 /\ IS_CTL_STAR_PATH_FORMULA f2)`;
118    (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_STATE_FORMULA f1 /\ IS_CTL_STAR_STATE_FORMULA f2) /\
122    (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = F) /\
123    (IS_CTL_STAR_STATE_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = F)`;
130    (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_AND(f1,f2)) = IS_CTL_STAR_PROP_FORMULA f1 /\ IS_CTL_STAR_PROP_FORMULA f2) /\
134    (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_SUNTIL(f1,f2)) = F) /\
135    (IS_CTL_STAR_PROP_FORMULA (CTL_STAR_PSUNTIL(f1,f2)) = F)`;
142    (CTL_STAR_USED_VARS (CTL_STAR_AND(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2) /\
146    (CTL_STAR_USED_VARS (CTL_STAR_SUNTIL(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2) /\
147    (CTL_STAR_USED_VARS (CTL_STAR_PSUNTIL(f1,f2)) = CTL_STAR_USED_VARS f1 UNION CTL_STAR_USED_VARS f2)`;
193    (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_AND(f1,f2)) p = CTL_STAR_SEM_NO_MODEL_PATH_TIME t f1 p /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME t f2 p) /\
196    (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_SUNTIL(f1,f2)) p = (?k. k >= t /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME k f2 p /\
198    (CTL_STAR_SEM_NO_MODEL_PATH_TIME t (CTL_STAR_PSUNTIL(f1,f2)) p = (?k. k <= t /\ CTL_STAR_SEM_NO_MODEL_PATH_TIME k f2 p /\
255 val CTL_STAR_OR_def = Define `CTL_STAR_OR(f1,f2) = CTL_STAR_NOT (CTL_STAR_AND((CTL_STAR_NOT f1),(CTL_STAR_NOT f2)))`;
256 val CTL_STAR_IMPL_def = Define `CTL_STAR_IMPL(f1, f2) = CTL_STAR_OR(CTL_STAR_NOT f1, f2)`;
257 val CTL_STAR_COND_def = Define `CTL_STAR_COND(c, f1, f2) = CTL_STAR_AND(CTL_STAR_IMPL(c, f1), CTL_STAR_IMPL(CTL_STAR_NOT c, f2))`;
261 val CTL_STAR_UNTIL_def = Define `CTL_STAR_UNTIL(f1,f2) = CTL_STAR_OR(CTL_STAR_SUNTIL(f1,f2),CTL_STAR_ALWAYS f1)`;
262 val CTL_STAR_BEFORE_def = Define `CTL_STAR_BEFORE(f1,f2) = CTL_STAR_NOT(CTL_STAR_SUNTIL(CTL_STAR_NOT f1,f2))`;
263 val CTL_STAR_SBEFORE_def = Define `CTL_STAR_SBEFORE(f1,f2) = CTL_STAR_SUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, CTL_STAR_NOT f2))`;
264 val CTL_STAR_WHILE_def = Define `CTL_STAR_WHILE(f1,f2) = CTL_STAR_NOT(CTL_STAR_SUNTIL(CTL_STAR_OR(CTL_STAR_NOT f1, CTL_STAR_NOT f2),CTL_STAR_AND(f2, CTL_STAR_NOT f1)))`;
265 val CTL_STAR_SWHILE_def = Define `CTL_STAR_SWHILE(f1,f2) = CTL_STAR_SUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, f2))`;
268 val CTL_STAR_PUNTIL_def = Define `CTL_STAR_PUNTIL(f1,f2) = CTL_STAR_OR(CTL_STAR_PSUNTIL(f1,f2),CTL_STAR_PALWAYS f1)`;
270 val CTL_STAR_PBEFORE_def = Define `CTL_STAR_PBEFORE(f1,f2) = CTL_STAR_NOT(CTL_STAR_PSUNTIL(CTL_STAR_NOT f1,f2))`;
271 val CTL_STAR_PSBEFORE_def = Define `CTL_STAR_PSBEFORE(f1,f2) = CTL_STAR_PSUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, CTL_STAR_NOT f2))`;
272 val CTL_STAR_PWHILE_def = Define `CTL_STAR_PWHILE(f1,f2) = CTL_STAR_NOT(CTL_STAR_PSUNTIL(CTL_STAR_OR(CTL_STAR_NOT f1, CTL_STAR_NOT f2),CTL_STAR_AND(f2, CTL_STAR_NOT f1)))`;
273 val CTL_STAR_PSWHILE_def = Define `CTL_STAR_PSWHILE(f1,f2) = CTL_STAR_PSUNTIL(CTL_STAR_NOT f2,CTL_STAR_AND(f1, f2))`;
285     prove (``!M f1 f2 p s t.
286       (CTL_STAR_SEM_PATH M (CTL_STAR_OR(f1, f2)) p =
287        (CTL_STAR_SEM_PATH M f1 p \/ CTL_STAR_SEM_PATH M f2 p)) /\
288       (CTL_STAR_SEM_PATH M (CTL_STAR_IMPL(f1, f2)) p =
289        (CTL_STAR_SEM_PATH M f1 p ==> CTL_STAR_SEM_PATH M f2 p)) /\
290       (CTL_STAR_SEM_PATH M (CTL_STAR_EQUIV(f1, f2)) p =
291        (CTL_STAR_SEM_PATH M f1 p = CTL_STAR_SEM_PATH M f2 p)) /\
292       (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_OR(f1, f2)) p =
293        (CTL_STAR_SEM_PATH_TIME t M f1 p \/ CTL_STAR_SEM_PATH_TIME t M f2 p)) /\
294       (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_IMPL(f1, f2)) p =
295        (CTL_STAR_SEM_PATH_TIME t M f1 p ==> CTL_STAR_SEM_PATH_TIME t M f2 p)) /\
296       (CTL_STAR_SEM_PATH_TIME t M (CTL_STAR_EQUIV(f1, f2)) p =
297        (CTL_STAR_SEM_PATH_TIME t M f1 p = CTL_STAR_SEM_PATH_TIME t M f2 p)) /\
298       (CTL_STAR_SEM_STATE M (CTL_STAR_OR(f1, f2)) s =
299        (CTL_STAR_SEM_STATE M f1 s \/ CTL_STAR_SEM_STATE M f2 s)) /\
300       (CTL_STAR_SEM_STATE M (CTL_STAR_IMPL(f1, f2)) s =
301        (CTL_STAR_SEM_STATE M f1 s ==> CTL_STAR_SEM_STATE M f2 s)) /\
302       (CTL_STAR_SEM_STATE M (CTL_STAR_EQUIV(f1, f2)) s =
303        (CTL_STAR_SEM_STATE M f1 s = CTL_STAR_SEM_STATE M f2 s))``,
435    (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
437    (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
439    (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))`;
444     ``!b f c f1 f2.
447    (LTL_TO_CTL_STAR (LTL_AND (f1, f2)) = (CTL_STAR_AND (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
448    (LTL_TO_CTL_STAR (LTL_OR (f1, f2)) = (CTL_STAR_OR (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
449    (LTL_TO_CTL_STAR (LTL_IMPL (f1, f2)) = (CTL_STAR_IMPL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
450    (LTL_TO_CTL_STAR (LTL_COND (c, f1, f2)) = (CTL_STAR_COND (LTL_TO_CTL_STAR c, LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
451    (LTL_TO_CTL_STAR (LTL_EQUIV (f1, f2)) = (CTL_STAR_EQUIV (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
455    (LTL_TO_CTL_STAR (LTL_SUNTIL (f1, f2)) = (CTL_STAR_SUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
456    (LTL_TO_CTL_STAR (LTL_UNTIL (f1, f2)) = (CTL_STAR_UNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
457    (LTL_TO_CTL_STAR (LTL_BEFORE (f1, f2)) = (CTL_STAR_BEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
458    (LTL_TO_CTL_STAR (LTL_SBEFORE (f1, f2)) = (CTL_STAR_SBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
459    (LTL_TO_CTL_STAR (LTL_WHILE (f1, f2)) = (CTL_STAR_WHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
460    (LTL_TO_CTL_STAR (LTL_SWHILE (f1, f2)) = (CTL_STAR_SWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
465    (LTL_TO_CTL_STAR (LTL_PSUNTIL (f1, f2)) = (CTL_STAR_PSUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
466    (LTL_TO_CTL_STAR (LTL_PUNTIL (f1, f2)) = (CTL_STAR_PUNTIL (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
467    (LTL_TO_CTL_STAR (LTL_PBEFORE (f1, f2)) = (CTL_STAR_PBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
468    (LTL_TO_CTL_STAR (LTL_PSBEFORE (f1, f2)) = (CTL_STAR_PSBEFORE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
469    (LTL_TO_CTL_STAR (LTL_PWHILE (f1, f2)) = (CTL_STAR_PWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2))) /\
470    (LTL_TO_CTL_STAR (LTL_PSWHILE (f1, f2)) = (CTL_STAR_PSWHILE (LTL_TO_CTL_STAR f1, LTL_TO_CTL_STAR f2)))``,
529          | FAIR_CTL_AND      of fair_ctl # fair_ctl                              (* f1 \wedge f2            *)
547          [`P`,`\(f1,f2). P f1 /\ P f2`]
556    (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_AND (f1, f2)) = (CTL_STAR_AND (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2))) /\
558    (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_E_SUNTIL FC (f1, f2)) = (CTL_STAR_FAIR_E FC (CTL_STAR_SUNTIL (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2)))) /\
559    (FAIR_CTL_TO_CTL_STAR (FAIR_CTL_E_UNTIL FC (f1, f2)) = (CTL_STAR_FAIR_E FC (CTL_STAR_UNTIL (FAIR_CTL_TO_CTL_STAR f1, FAIR_CTL_TO_CTL_STAR f2))))`;
596 val FAIR_CTL_OR_def = Define `FAIR_CTL_OR(f1,f2) = FAIR_CTL_NOT (FAIR_CTL_AND((FAIR_CTL_NOT f1),(FAIR_CTL_NOT f2)))`;
597 val FAIR_CTL_IMPL_def = Define `FAIR_CTL_IMPL(f1, f2) = FAIR_CTL_OR(FAIR_CTL_NOT f1, f2)`;
598 val FAIR_CTL_COND_def = Define `FAIR_CTL_COND(c, f1, f2) = FAIR_CTL_AND(FAIR_CTL_IMPL(c, f1), FAIR_CTL_IMPL(FAIR_CTL_NOT c, f2))`;
605 val FAIR_CTL_A_UNTIL_def = Define `FAIR_CTL_A_UNTIL FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, (FAIR_CTL_AND(FAIR_CTL_NOT f1, FAIR_CTL_NOT f2))))`;
606 val FAIR_CTL_A_SUNTIL_def = Define `FAIR_CTL_A_SUNTIL FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, (FAIR_CTL_AND(FAIR_CTL_NOT f1, FAIR_CTL_NOT f2))))`;
607 val FAIR_CTL_E_BEFORE_def = Define `FAIR_CTL_E_BEFORE FC (f1,f2) = FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, FAIR_CTL_NOT f2))`;
608 val FAIR_CTL_E_SBEFORE_def = Define `FAIR_CTL_E_SBEFORE FC (f1,f2) = FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, FAIR_CTL_NOT f2))`;
609 val FAIR_CTL_A_BEFORE_def = Define `FAIR_CTL_A_BEFORE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f1, f2))`;
610 val FAIR_CTL_A_SBEFORE_def = Define `FAIR_CTL_A_SBEFORE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f1, f2))`;
611 val FAIR_CTL_E_WHILE_def = Define `FAIR_CTL_E_WHILE FC (f1,f2) = FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, f2))`;
612 val FAIR_CTL_E_SWHILE_def = Define `FAIR_CTL_E_SWHILE FC (f1,f2) = FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(f1, f2))`;
613 val FAIR_CTL_A_WHILE_def = Define `FAIR_CTL_A_WHILE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_SUNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(FAIR_CTL_NOT f1, f2)))`;
614 val FAIR_CTL_A_SWHILE_def = Define `FAIR_CTL_A_SWHILE FC (f1,f2) = FAIR_CTL_NOT(FAIR_CTL_E_UNTIL FC (FAIR_CTL_NOT f2, FAIR_CTL_AND(FAIR_CTL_NOT f1, f2)))`;
619     ``!M b FC f f1 f2 s.
625    (FAIR_CTL_SEM M (FAIR_CTL_AND(f1,f2)) s = FAIR_CTL_SEM M f1 s /\ FAIR_CTL_SEM M f2 s) /\
627    (FAIR_CTL_SEM M (FAIR_CTL_OR(f1,f2)) s = FAIR_CTL_SEM M f1 s \/ FAIR_CTL_SEM M f2 s) /\
629    (FAIR_CTL_SEM M (FAIR_CTL_IMPL(f1,f2)) s = FAIR_CTL_SEM M f1 s ==> FAIR_CTL_SEM M f2 s) /\
634    (FAIR_CTL_SEM M (FAIR_CTL_E_SUNTIL FC (f1, f2)) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\
635       (p 0 = s) /\ (?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))))) /\
637    (FAIR_CTL_SEM M (FAIR_CTL_E_UNTIL FC (f1, f2)) s = (?p. IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\
639       ((?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))) \/
692     ``!M f1 f2 FC s.
693    (FAIR_CTL_SEM M (FAIR_CTL_A_SUNTIL FC (f1, f2)) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\
694       (p 0 = s)) ==> (?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j)))))``,
703     Cases_on `?k. FAIR_CTL_SEM M f2 (p k)` THENL [
739     ``!M f1 f2 FC s.
740    (FAIR_CTL_SEM M (FAIR_CTL_A_UNTIL FC (f1, f2)) s = (!p. (IS_FAIR_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M FC p /\
741       (p 0 = s)) ==> ((?k. FAIR_CTL_SEM M f2 (p k) /\ (!j. j < k ==> FAIR_CTL_SEM M f1 (p j))) \/
815          | CTL_AND      of ctl # ctl         (* f1 \wedge f2            *)
834          [`P`,`\(f1,f2). P f1 /\ P f2`]
843    (CTL_TO_FAIR_CTL fc (CTL_AND (f1, f2)) = (FAIR_CTL_AND (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
845    (CTL_TO_FAIR_CTL fc (CTL_E_SUNTIL (f1, f2)) = (FAIR_CTL_E_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
846    (CTL_TO_FAIR_CTL fc (CTL_E_UNTIL (f1, f2)) = (FAIR_CTL_E_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2)))`;
892 val CTL_OR_def = Define `CTL_OR(f1,f2) = CTL_NOT (CTL_AND((CTL_NOT f1),(CTL_NOT f2)))`;
893 val CTL_IMPL_def = Define `CTL_IMPL(f1, f2) = CTL_OR(CTL_NOT f1, f2)`;
894 val CTL_COND_def = Define `CTL_COND(c, f1, f2) = CTL_AND(CTL_IMPL(c, f1), CTL_IMPL(CTL_NOT c, f2))`;
901 val CTL_A_UNTIL_def = Define `CTL_A_UNTIL(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f2, (CTL_AND(CTL_NOT f1, CTL_NOT f2))))`;
902 val CTL_A_SUNTIL_def = Define `CTL_A_SUNTIL(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f2, (CTL_AND(CTL_NOT f1, CTL_NOT f2))))`;
903 val CTL_E_BEFORE_def = Define `CTL_E_BEFORE(f1,f2) = CTL_E_UNTIL(CTL_NOT f2, CTL_AND(f1, CTL_NOT f2))`;
904 val CTL_E_SBEFORE_def = Define `CTL_E_SBEFORE(f1,f2) = CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(f1, CTL_NOT f2))`;
905 val CTL_A_BEFORE_def = Define `CTL_A_BEFORE(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f1, f2))`;
906 val CTL_A_SBEFORE_def = Define `CTL_A_SBEFORE(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f1, f2))`;
907 val CTL_E_WHILE_def = Define `CTL_E_WHILE(f1,f2) = CTL_E_UNTIL(CTL_NOT f2, CTL_AND(f1, f2))`;
908 val CTL_E_SWHILE_def = Define `CTL_E_SWHILE(f1,f2) = CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(f1, f2))`;
909 val CTL_A_WHILE_def = Define `CTL_A_WHILE(f1,f2) = CTL_NOT(CTL_E_SUNTIL(CTL_NOT f2, CTL_AND(CTL_NOT f1, f2)))`;
910 val CTL_A_SWHILE_def = Define `CTL_A_SWHILE(f1,f2) = CTL_NOT(CTL_E_UNTIL(CTL_NOT f2, CTL_AND(CTL_NOT f1, f2)))`;
916     ``!b f f1 f2 c fc.
919         (CTL_TO_FAIR_CTL fc (CTL_AND (f1, f2)) = (FAIR_CTL_AND (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
920         (CTL_TO_FAIR_CTL fc (CTL_OR (f1, f2)) = (FAIR_CTL_OR (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
921         (CTL_TO_FAIR_CTL fc (CTL_IMPL (f1, f2)) = (FAIR_CTL_IMPL (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
922         (CTL_TO_FAIR_CTL fc (CTL_COND (c, f1, f2)) = (FAIR_CTL_COND (CTL_TO_FAIR_CTL fc c, CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
923         (CTL_TO_FAIR_CTL fc (CTL_EQUIV (f1, f2)) = (FAIR_CTL_EQUIV (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
930         (CTL_TO_FAIR_CTL fc (CTL_E_SUNTIL (f1, f2)) = (FAIR_CTL_E_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
931         (CTL_TO_FAIR_CTL fc (CTL_A_SUNTIL (f1, f2)) = (FAIR_CTL_A_SUNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
932         (CTL_TO_FAIR_CTL fc (CTL_E_UNTIL (f1, f2)) = (FAIR_CTL_E_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
933         (CTL_TO_FAIR_CTL fc (CTL_A_UNTIL (f1, f2)) = (FAIR_CTL_A_UNTIL fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
934         (CTL_TO_FAIR_CTL fc (CTL_E_BEFORE (f1, f2)) = (FAIR_CTL_E_BEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
935         (CTL_TO_FAIR_CTL fc (CTL_A_BEFORE (f1, f2)) = (FAIR_CTL_A_BEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
936         (CTL_TO_FAIR_CTL fc (CTL_E_SBEFORE (f1, f2)) = (FAIR_CTL_E_SBEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
937         (CTL_TO_FAIR_CTL fc (CTL_A_SBEFORE (f1, f2)) = (FAIR_CTL_A_SBEFORE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
938         (CTL_TO_FAIR_CTL fc (CTL_E_WHILE (f1, f2)) = (FAIR_CTL_E_WHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
939         (CTL_TO_FAIR_CTL fc (CTL_A_WHILE (f1, f2)) = (FAIR_CTL_A_WHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
940         (CTL_TO_FAIR_CTL fc (CTL_E_SWHILE (f1, f2)) = (FAIR_CTL_E_SWHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2))) /\
941         (CTL_TO_FAIR_CTL fc (CTL_A_SWHILE (f1, f2)) = (FAIR_CTL_A_SWHILE fc (CTL_TO_FAIR_CTL fc f1, CTL_TO_FAIR_CTL fc f2)))``,
948     ``!M b f f1 f2 s.
956    (CTL_SEM M (CTL_AND(f1,f2)) s = CTL_SEM M f1 s /\ CTL_SEM M f2 s) /\
961    (CTL_SEM M (CTL_E_SUNTIL(f1, f2)) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\
962       (p 0 = s) /\ (?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))))) /\
964    (CTL_SEM M (CTL_E_UNTIL(f1, f2)) s = (?p. IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\
966       ((?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))) \/
982    (CTL_SEM M (CTL_A_SUNTIL(f1, f2)) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\
983       (p 0 = s)) ==> (?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))))) /\
985    (CTL_SEM M (CTL_A_UNTIL(f1, f2)) s = (!p. (IS_PATH_THROUGH_SYMBOLIC_KRIPKE_STRUCTURE M p /\
986       (p 0 = s)) ==> ((?k. CTL_SEM M f2 (p k) /\ (!j. j < k ==> CTL_SEM M f1 (p j))) \/