Lines Matching refs:f2
455 ``(!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ==> (((f1 SUBMAP (FUNION f2 f3)) = (f1 SUBMAP f3)))) /\
456 (!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f3 DIFF (FDOM f2)) ==> (((f1 SUBMAP (FUNION f2 f3)) = (f1 SUBMAP f2))))``,
464 ``!f1 f2 f3. (f1 SUBMAP f2) \/ ((DISJOINT (FDOM f1) (FDOM f2) /\ (f1 SUBMAP f3))) ==> (f1 SUBMAP (FUNION f2 f3))``,
471 ``(!f1 f2. (f1 SUBMAP (FUNION f1 f2))) /\
472 (!f1 f2. (DISJOINT (FDOM f1) (FDOM f2)) ==> (f2 SUBMAP (FUNION f1 f2)))``,
485 ``!f1 f2 f3. (DISJOINT (FDOM f1) (FDOM f2) /\
487 (((FUNION f1 f2) = (FUNION f1 f3)) = (f2 = f3))``,
494 ``!f1 f2 f3. (DISJOINT (FDOM f1) (FDOM f2) /\
495 DISJOINT (FDOM f1) (FDOM f3) /\ (f2 = f3)) ==>
496 ((FUNION f1 f2) = (FUNION f1 f3))``,
621 ``!f1 f2 l. (MAP f1 l = MAP f2 l) = (!e. MEM e l ==> (f1 e = f2 e))``,
1748 `DS_ENTAILS f1 f2 =
1749 !s h. (DS_SEM s h f1 ==> DS_SEM s h f2)`
1752 `DS_EQUIV f1 f2 =
1753 !s h. (DS_SEM s h f1 = DS_SEM s h f2)`
1756 ``!f1 f2. DS_EQUIV f1 f2 = (DS_ENTAILS f1 f2 /\ DS_ENTAILS f2 f1)``,
2462 sf_bin_tree (f1, f2) e = sf_tree [f1;f2] dse_nil e`;
2467 ``!s h f1 f2 e.
2468 SF_SEM s h (sf_bin_tree (f1,f2) e) = (
2474 (sf_points_to e [(f1, dse_const c1);(f2, dse_const c2)])
2475 (sf_star (sf_bin_tree (f1,f2) (dse_const c1))
2476 (sf_bin_tree (f1,f2) (dse_const c2)))))
2508 ``!s h f1 f2 e.
2509 SF_SEM s h (sf_bin_tree (f1,f2) e) = (
2514 let c2 = h ' (DS_EXPRESSION_EVAL_VALUE s e) ' f2 in
2516 (sf_points_to e [(f1, dse_const c1);(f2, dse_const c2)])
2517 (sf_star (sf_bin_tree (f1,f2) (dse_const c1))
2518 (sf_bin_tree (f1,f2) (dse_const c2)))))
3452 (!s h f1 f2 sfL pfL e.
3454 (LIST_DS_SEM s h (pfL, (sf_bin_tree (f1,f2) e)::sfL) =
3457 (!s h f1 f2 sfL pfL.
3458 (LIST_DS_SEM s h (pfL, (sf_bin_tree (f1,f2) dse_nil)::sfL) =
3471 (!s h f1 f2 sfL pfL e1 e2.
3473 (LIST_DS_SEM s h (pfL, (sf_bin_tree (f1,f2) e)::sfL) =
3476 let c2 = h ' (DS_EXPRESSION_EVAL_VALUE s e) ' f2 in
3478 (sf_points_to e [(f1, dse_const c1);(f2, dse_const c2)])::
3479 (sf_bin_tree (f1,f2) (dse_const c1))::
3480 (sf_bin_tree (f1,f2) (dse_const c2))::sfL)
3622 (SF_SUBST v e (sf_bin_tree (f1,f2) e1) = sf_bin_tree (f1,f2) (DS_VAR_SUBST v e e1)) /\
3767 MATCH_MP_TAC (prove(``((a1 /\ b1 /\ f1 = a2 /\ b2 /\ f2) /\ (c1 = c2) /\
3770 (a2 /\ b2 /\ c2 /\ d2 /\ e2 /\ f2 /\ g2))``, SIMP_TAC std_ss [] THEN METIS_TAC[])) THEN
6285 `?f1 f2 fL'. fL = f1::f2::fL'` by (
6293 DS_POINTS_TO___RTC s h [f2] e es'` by (
6295 DS_POINTS_TO___RTC s h' [f2] e' es'` by (
6300 `MEM f1 fL /\ MEM f2 fL` by ASM_SIMP_TAC list_ss [] THEN
6323 (SF_SEM___sf_tree_len s h2 fL n es (dse_const (h ' v ' f2)))` by (
6330 `(EL 0 fL = f1) /\ (EL 1 fL = f2)` by ASM_SIMP_TAC list_ss [] THEN
6341 DS_POINTS_TO___RTC s h [f2] (dse_const (h ' v ' f2)) es'` by (
6360 `DS_EXPRESSION_EQUAL s y (dse_const (h ' v ' f2))` by (
6404 Q.EXISTS_TAC `(dse_const (h ' v ' f2))` THEN
6411 Q.EXISTS_TAC `[f2]` THEN
7233 (!f1 f2. MEM f1 fL /\ MEM f2 fL ==> (((h2 ' (DS_EXPRESSION_EVAL_VALUE s e) ' f1) =
7234 (h2 ' (DS_EXPRESSION_EVAL_VALUE s e) ' f2)) =
7235 (f1 = f2))))
7419 Cases_on `f1 = f2` THEN ASM_REWRITE_TAC[] THEN
7421 `?n2. (n2 < LENGTH hL) /\ (EL n2 fL = f2)` by METIS_TAC[MEM_EL] THEN
7429 `(FDOM (EL n2 hL) = {DS_EXPRESSION_EVAL_VALUE s (dse_const (h ' (GET_DSV_VALUE (DS_EXPRESSION_EVAL s e)) ' f2))}) /\
7430 ~IS_DSV_NIL (DS_EXPRESSION_EVAL s (dse_const (h ' (GET_DSV_VALUE (DS_EXPRESSION_EVAL s e)) ' f2)))` by METIS_TAC[BALANCED_SF_SEM___sf_tree_len_1___MODEL_SIZE] THEN
9126 ``!f1 f2 c1 c2 pfL sfL pfL' sfL'.
9128 LIST_DS_ENTAILS (c1,c2) (pfL, (sf_bin_tree (f1,f2) dse_nil)::sfL) (pfL', sfL')``,
9191 ``!f1 f2 c1 c2 pfL sfL pfL' sfL'.
9193 LIST_DS_ENTAILS (c1,c2) (pfL, sfL) (pfL', (sf_bin_tree (f1,f2) dse_nil)::sfL')``,
9426 ``!e f1 f2 f1' f2' c1 c2 pfL sfL pfL' sfL'.
9427 (((f1 = f1') /\ (f2 = f2')) \/ ((f1 = f2') /\ (f2 = f1'))) ==>
9430 LIST_DS_ENTAILS (c1, c2) (pfL, (sf_bin_tree (f1,f2) e)::sfL) (pfL', (sf_bin_tree (f1',f2') e)::sfL'))``,
9610 ``!e e1 e2 f1 f2 a c1 c2 pfL sfL pfL' sfL'.
9611 ((MEM (f1, e1) a) /\ (MEM (f2, e2) a) /\ ~(f1 = f2)) ==>
9612 ((LIST_DS_ENTAILS (c1,c2) (pfL, (sf_points_to e a)::sfL) (pfL', (sf_points_to e a)::(sf_bin_tree (f1,f2) e1)::(sf_bin_tree (f1,f2) e2)::sfL')) =
9613 (LIST_DS_ENTAILS (c1,c2) (pfL, (sf_points_to e a)::sfL) (pfL', (sf_bin_tree (f1,f2) e)::sfL')))``,
9619 Q.SPECL [`e`, `dse_nil`, `c1`, `c2`, `[e1;e2]`, `[f1;f2]`, `a`, `pfL`, `sfL`, `pfL'`, `sfL'`] INFERENCE_NON_EMPTY_TREE
9781 ``!e:('b, 'a) ds_expression f1 f2 pfL sfL pfL' sfL'.
9782 (INFINITE (UNIV:'b set) /\ (~(f1 = f2)) /\
9785 (sf_points_to e [(f1, dse_const x1);(f2, dse_const x2)])::(sf_points_to (dse_const x1) [(f1, dse_nil);(f2, dse_nil)])::(sf_points_to (dse_const x2) [(f1, dse_nil);(f2, dse_nil)])::sfL) (pfL', sfL')))) ==>
9787 LIST_DS_ENTAILS ([],[]) (pfL, (sf_bin_tree (f1,f2) e)::sfL) (pfL', sfL')``,
9804 MP_TAC (Q.SPECL [`s`, `h2`, `[f1;f2]`, `e`, `dse_nil`, `pf`, `sf`, `pf'`, `sf'`] LEMMA_5) THEN
9934 ``!e:('b, 'a) ds_expression f1 f2 c1 c2 pfL sfL pfL' sfL'.
9935 (INFINITE (UNIV:'b set) /\ (~(f1 = f2))) ==>
9940 (sf_points_to e [(f1, dse_const x1);(f2, dse_const x2)])::(sf_points_to (dse_const x1) [(f1, dse_nil);(f2, dse_nil)])::(sf_points_to (dse_const x2) [(f1, dse_nil);(f2, dse_nil)])::sfL) (pfL', sfL'))) =
9942 LIST_DS_ENTAILS (c1,c2) (pfL, (sf_bin_tree (f1,f2) e)::sfL) (pfL', sfL'))``,
10038 ``!e f1 f2 c1 c2 pfL sfL pfL' sfL'.
10040 (LIST_DS_ENTAILS (c1,c2) (pfL, (sf_bin_tree (f1, f2) e)::sfL) (pfL', sfL'))``,