src/deep_embeddings/xprop_logicScript.sml

38    (XP_USED_CURRENT_VARS (XP_AND(b1,b2)) =
39       (XP_USED_CURRENT_VARS b1) UNION (XP_USED_CURRENT_VARS b2))`;
46    (XP_USED_X_VARS (XP_AND(b1,b2)) = (XP_USED_X_VARS b1) UNION (XP_USED_X_VARS b2))`;
56    (XP_VAR_RENAMING f (XP_AND(b1,b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2))`;
68    (XP_SEM (XP_AND (b1,b2)) (s1, s2) = ((XP_SEM b1 (s1, s2)) /\ (XP_SEM b2 (s1, s2))))`;
81    `XP_OR(b1, b2) = XP_NOT(XP_AND(XP_NOT b1, XP_NOT b2))`;
84    `XP_IMPL(b1, b2) = XP_OR(XP_NOT b1, b2)`;
90    `XP_EQUIV(b1, b2) = XP_AND(XP_IMPL(b1, b2),XP_IMPL(b2, b1))`;
93    `XPROP_LOGIC_EQUIVALENT b1 b2 = !s1 s2. (XP_SEM b1 (s1, s2)) = (XP_SEM b2 (s1, s2))`;
100    (XP_NEXT (P_AND(b1,b2)) = (XP_AND((XP_NEXT b1),(XP_NEXT b2))))`;
107    (XP_CURRENT (P_AND(b1,b2)) = (XP_AND((XP_CURRENT b1),(XP_CURRENT b2))))`;
150     ((XP_NEXT (P_AND(b1, b2))) = XP_AND (XP_NEXT b1, XP_NEXT b2)) /\
151     ((XP_NEXT (P_OR(b1, b2))) = XP_OR (XP_NEXT b1, XP_NEXT b2)) /\
152     ((XP_NEXT (P_IMPL(b1, b2))) = XP_IMPL (XP_NEXT b1, XP_NEXT b2)) /\
153     ((XP_NEXT (P_EQUIV(b1, b2))) = XP_EQUIV (XP_NEXT b1, XP_NEXT b2)) /\
173     ((XP_CURRENT (P_AND(b1, b2))) = XP_AND (XP_CURRENT b1, XP_CURRENT b2)) /\
174     ((XP_CURRENT (P_OR(b1, b2))) = XP_OR (XP_CURRENT b1, XP_CURRENT b2)) /\
175     ((XP_CURRENT (P_IMPL(b1, b2))) = XP_IMPL (XP_CURRENT b1, XP_CURRENT b2)) /\
176     ((XP_CURRENT (P_EQUIV(b1, b2))) = XP_EQUIV (XP_CURRENT b1, XP_CURRENT b2)) /\
192      ``!s1 s2 b1 b2 b c p.
198        (XP_SEM (XP_AND (b1,b2)) (s1,s2) =
199         (XP_SEM b1 (s1,s2) /\ XP_SEM b2 (s1,s2))) /\
200        (XP_SEM (XP_OR (b1,b2)) (s1,s2) = XP_SEM b1 (s1,s2) \/ XP_SEM b2 (s1,s2)) /\
201        (XP_SEM (XP_IMPL (b1,b2)) (s1,s2) = (~XP_SEM b1 (s1,s2) \/ XP_SEM b2 (s1,s2))) /\
202        (XP_SEM (XP_EQUIV (b1,b2)) (s1,s2) = (XP_SEM b1 (s1,s2) = XP_SEM b2 (s1,s2))) /\
203        (XP_SEM (XP_COND (c, b1, b2)) (s1,s2) = (XP_SEM (XP_AND(c, b1)) (s1,s2) \/ XP_SEM (XP_AND(XP_NOT c, b2)) (s1,s2)))``,
214    ``!p b b1 b2.
219       (XP_USED_VARS (XP_AND(b1,b2)) = ((XP_USED_VARS b1) UNION (XP_USED_VARS b2)))``,
294    ``!p c b b1 b2 P. (
302     (XP_USED_VARS (XP_AND(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\
303     (XP_USED_VARS (XP_OR(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\
304     (XP_USED_VARS (XP_COND(c, b1, b2)) = XP_USED_VARS c UNION XP_USED_VARS b1 UNION XP_USED_VARS b2) /\
305     (XP_USED_VARS (XP_IMPL(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\
306     (XP_USED_VARS (XP_EQUIV(b1, b2)) = XP_USED_VARS b1 UNION XP_USED_VARS b2) /\
314     (XP_USED_CURRENT_VARS (XP_AND(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\
315     (XP_USED_CURRENT_VARS (XP_OR(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\
316     (XP_USED_CURRENT_VARS (XP_COND(c, b1, b2)) = XP_USED_CURRENT_VARS c UNION XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\
317     (XP_USED_CURRENT_VARS (XP_IMPL(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\
318     (XP_USED_CURRENT_VARS (XP_EQUIV(b1, b2)) = XP_USED_CURRENT_VARS b1 UNION XP_USED_CURRENT_VARS b2) /\
326     (XP_USED_X_VARS (XP_AND(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\
327     (XP_USED_X_VARS (XP_OR(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\
328     (XP_USED_X_VARS (XP_COND(c, b1, b2)) = XP_USED_X_VARS c UNION XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\
329     (XP_USED_X_VARS (XP_IMPL(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2) /\
330     (XP_USED_X_VARS (XP_EQUIV(b1, b2)) = XP_USED_X_VARS b1 UNION XP_USED_X_VARS b2)
547   (XP_ASSIGN_TRUE V V' (XP_AND(b1,b2)) = XP_AND (
549         XP_ASSIGN_TRUE V V' b2))`;
557   (XP_ASSIGN_FALSE V V' (XP_AND(b1,b2)) = XP_AND (
559         XP_ASSIGN_FALSE V V' b2))`;
943    ``!p f b b1 b2. (
949     (XP_VAR_RENAMING f (XP_AND(b1, b2)) = XP_AND(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\
950     (XP_VAR_RENAMING f (XP_OR(b1, b2)) = XP_OR(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\
951     (XP_VAR_RENAMING f (XP_IMPL(b1, b2)) = XP_IMPL(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f b2)) /\
952     (XP_VAR_RENAMING f (XP_EQUIV(b1, b2)) = XP_EQUIV(XP_VAR_RENAMING f b1, XP_VAR_RENAMING f  b2))
1060       (XP_ASSIGN_TRUE V V' (XP_AND(b1,b2)) = XP_AND (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\
1061       (XP_ASSIGN_TRUE V V' (XP_OR(b1,b2)) = XP_OR (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\
1062       (XP_ASSIGN_TRUE V V' (XP_IMPL(b1,b2)) = XP_IMPL (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\
1063       (XP_ASSIGN_TRUE V V' (XP_COND(c, b1,b2)) = XP_COND (XP_ASSIGN_TRUE V V' c, XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\
1064       (XP_ASSIGN_TRUE V V' (XP_EQUIV (b1,b2)) = XP_EQUIV (XP_ASSIGN_TRUE V V' b1, XP_ASSIGN_TRUE V V' b2)) /\
1071       (XP_ASSIGN_FALSE V V' (XP_AND(b1,b2)) = XP_AND (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\
1072       (XP_ASSIGN_FALSE V V' (XP_OR(b1,b2)) = XP_OR (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\
1073       (XP_ASSIGN_FALSE V V' (XP_IMPL(b1,b2)) = XP_IMPL (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\
1074       (XP_ASSIGN_FALSE V V' (XP_COND(c, b1,b2)) = XP_COND (XP_ASSIGN_FALSE V V' c, XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2)) /\
1075       (XP_ASSIGN_FALSE V V' (XP_EQUIV(b1,b2)) = XP_EQUIV (XP_ASSIGN_FALSE V V' b1, XP_ASSIGN_FALSE V V' b2))``,