Lines Matching refs:data2
3121 ``!wpb rpb e tagL dtagL data1 data2 sfb_context sfb_split sfb_imp.
3127 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data2)) sfb_imp)
3132 (data1 = data2)) sfb_imp))``,
3135 Cases_on `data2 = data1` THEN1 (
3165 ``!wpb rpb e tagL dtagL data1 data2 sfb_context sfb_split sfb_imp sr wpb' sfb_restP.
3171 (BAG_INSERT (holfoot_ap_data_tree tagL e (dtagL, data2)) sfb_imp) sfb_restP) =
3176 (data1 = data2)) sfb_imp)) sfb_restP)``,
4236 Q.ABBREV_TAC `data2 = (MAP (\x. (FST x,DROP (SUC n) (SND x))) data)` THEN
4237 `ALL_DISTINCT (tl::MAP FST data1) /\ ALL_DISTINCT (tl::MAP FST data2)` by (
4238 Q.UNABBREV_TAC `data1` THEN Q.UNABBREV_TAC `data2` THEN
4243 EVERY (\x. LENGTH (SND x) = m) data2)` by (
4244 Q.UNABBREV_TAC `data1` THEN Q.UNABBREV_TAC `data2` THEN
4264 (!c. holfoot_ap_data_list_seg_num m tl (var_res_exp_const c) data2 e2 =
4339 (MAP (\x. (FST x,DROP n (TL (SND x)))) data = data2)` by (
4342 Q.UNABBREV_TAC `data2` THEN
4376 MP_TAC (Q.SPECL [`n''`, `tl`, `data2`, `var_res_exp_const c`, `e2`, `(FST (x:holfoot_state), es2)`]
5128 ``!wpb rpb e1 e2 e3 tl data1 data2 sfb_context sfb_split sfb_imp n.
5129 ((LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5130 ALL_DISTINCT (MAP FST data2) /\
5138 (BAG_INSERT (holfoot_ap_data_list_seg_num n tl e1 data2 e3) sfb_imp)
5144 (EVERY (\x. MEM x data1) data2)) sfb_imp)))``,
5203 `data2`, `FST (s:holfoot_state)`, `s1`, `sp1`, `SND (s:holfoot_state)`]
5226 `data2`, `FST (s:holfoot_state)`, `s1`, `s1`, `s1`]
5237 `(FST s,s1) IN holfoot_ap_data_list_seg_num n tl e1 data2 e3 =
5238 (FST s,s1) IN holfoot_ap_data_list_seg_num n tl e1 data2 e2` by (
5254 ``!wpb rpb e1 e2 tl data1 data2 sfb_context sfb_split sfb_imp.
5255 ((LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5256 ALL_DISTINCT (MAP FST data2) /\
5263 (BAG_INSERT (holfoot_ap_data_list_seg tl e1 data2 e2) sfb_imp)
5268 (EVERY (\x. MEM x data1) data2)) sfb_imp))``,
5272 `data1`, `data2`, `sfb_context`, `sfb_split`, `sfb_imp`]
5347 ``!wpb rpb wpb' sr sfb_restP e1 e2 tl data1 data2 sfb_context sfb_split sfb_imp.
5348 ((LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5349 ALL_DISTINCT (MAP FST data2)) /\
5356 (BAG_INSERT (holfoot_ap_data_list_seg tl e1 data2 e2) sfb_imp)
5363 (EVERY (\x. MEM x data1) data2)) sfb_imp) sfb_restP)``,
5379 ``!wpb rpb e2 e3 tl n m e1 data1 data2 sfb_context sfb_split sfb_imp.
5381 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5382 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5390 (BAG_INSERT (holfoot_ap_data_list_seg_num (n+m) tl e1 data2 e3) sfb_imp)
5398 (EVERY (\x. MEM (FST x, TAKE n (SND x)) data1) data2))
5400 (MAP (\x. (FST x, (DROP n (SND x)))) data2) e3) sfb_imp))))``,
5508 Q.SPECL [`n`, `e1`, `e2`, `e1`, `var_res_exp_const c''`, `tl`, `data1`, ` (MAP (\x. (FST x,TAKE n (SND x))) data2)`,
5586 ``!sr sfb_restP wpb rpb wpb' e2 e3 tl n m e1 data1 data2 sfb_context sfb_split sfb_imp.
5588 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5589 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5597 (BAG_INSERT (holfoot_ap_data_list_seg_num (n+m) tl e1 data2 e3) sfb_imp)
5607 (EVERY (\x. MEM (FST x, TAKE n (SND x)) data1) data2))
5609 (MAP (\x. (FST x, (DROP n (SND x)))) data2) e3) sfb_imp)))
5621 ``!wpb rpb e2 e3 tl n m e1 data1 data2 sfb_context sfb_split sfb_imp.
5629 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5630 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5638 (BAG_INSERT (holfoot_ap_data_list_seg_num (n+m) tl e1 data2 e3) sfb_imp)
5643 (EVERY (\x. MEM (FST x, TAKE n (SND x)) data1) data2))
5645 (MAP (\x. (FST x, (DROP n (SND x)))) data2) e3) sfb_imp)))``,
5657 Q.SPECL [`wpb`, `rpb`, `e2`, `e3`, `tl`, `n`, `m`, `e1`, `data1`, `data2`, `sfb_context`, `sfb_split`, `sfb_imp`]
5820 ``!wpb rpb wpb' e2 e3 tl n m e1 data1 data2 sfb_context sfb_split sfb_imp sfb_restP sr.
5825 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5826 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5834 (BAG_INSERT (holfoot_ap_data_list_seg_num (n+m) tl e1 data2 e3) sfb_imp) sfb_restP =
5840 (EVERY (\x. MEM (FST x, TAKE n (SND x)) data1) data2))
5842 (MAP (\x. (FST x, (DROP n (SND x)))) data2) e3) sfb_imp))
5856 ``!wpb rpb wpb' e2 e3 tl n m e1 data1 data2 sfb_context sfb_split sfb_imp sfb_restP sr.
5861 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5862 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5870 (BAG_INSERT (holfoot_ap_data_list_seg_num (n+m) tl e1 data2 e3) sfb_imp) sfb_restP =
5876 (EVERY (\x. MEM (FST x, TAKE n (SND x)) data1) data2))
5878 (MAP (\x. (FST x, (DROP n (SND x)))) data2) e3) sfb_imp))
5893 ``!data1 data2 wpb rpb sfb_context sfb_split sfb_imp e1 e2 e3 tl.
5898 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
5899 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) ==>
5908 (BAG_INSERT (holfoot_ap_data_list_seg tl e1 data2 e3) sfb_imp))
5913 (EVERY (\x. MEM (FST x,TAKE (LENGTH (SND (HD data1))) (SND x)) data1) data2)) (
5916 (MAP (\x. (FST x, (DROP (LENGTH (SND (HD data1))) (SND x)))) data2) e3) sfb_imp)))``,
5949 Tactical.REVERSE (Cases_on `data2 <> [] /\ (LENGTH (SND (HD data1)) <> n)`) THEN1 (
5950 `(EVERY (\x. MEM (FST x,TAKE (LENGTH (SND (HD data1))) (SND x)) data1) data2 =
5951 EVERY (\x. MEM (FST x,TAKE n (SND x)) data1) data2) /\
5952 (MAP (\x. (FST x,DROP (LENGTH (SND (HD data1))) (SND x))) data2 =
5953 MAP (\x. (FST x,DROP n (SND x))) data2)` by (
5954 Cases_on `data2` THEN FULL_SIMP_TAC list_ss []) THEN
5962 Cases_on `data2` THEN FULL_SIMP_TAC list_ss [] THEN
6059 MP_TAC (Q.SPECL [`n'`, `e1`, `e3`, `e1`, `var_res_exp_const c`, `tl`, `data2`,
6104 ``!data1 data2 wpb rpb wpb' sr sfb_restP sfb_context sfb_split sfb_imp e1 e2 e3 tl.
6109 ((LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1)) /\
6110 (ALL_DISTINCT (tl::(MAP FST data1)) ==> ALL_DISTINCT (MAP FST data2)) /\
6118 (BAG_INSERT (holfoot_ap_data_list_seg tl e1 data2 e3) sfb_imp) sfb_restP) =
6124 (EVERY (\x. MEM (FST x,TAKE (LENGTH (SND (HD data1))) (SND x)) data1) data2)) (
6127 (MAP (\x. (FST x, (DROP (LENGTH (SND (HD data1))) (SND x)))) data2) e3) sfb_imp))
6731 ``!e n data1 data2 s.
6732 (s IN holfoot_ap_data_array e n data2 /\ (!x. MEM x data1 ==> MEM x data2) /\
6744 Q.PAT_X_ASSUM `EVERY X data2` (K ALL_TAC) THEN
6747 MAP_EVERY (fn x => Q.SPEC_TAC (x,x)) [`data1`, `data2`, `s`, `e`, `cn`] THEN
6764 Q.EXISTS_TAC `LIST_TO_FMAP (MAP (\tl. (FST tl,var_res_exp_const (HD (SND tl)))) data2)` THEN
6768 `MEM x (MAP FST data2)` by (
6773 `(MAP FST L1 = MAP FST data1) /\ (MAP FST L2 = MAP FST data2)` by (
6785 Q.PAT_X_ASSUM `!e s data2 data1. X ==> Y` MATCH_MP_TAC THEN
6786 Q.EXISTS_TAC `MAP (\tl. (FST tl,TL (SND tl))) data2` THEN
6809 ``!e n data1 data2.
6810 (PERM data1 data2) ==>
6812 holfoot_ap_data_array e n data2)``,
6816 `(!n. (EVERY (\tl. LENGTH (SND tl) = n) data2 =
6818 (ALL_DISTINCT (MAP FST data2) = ALL_DISTINCT (MAP FST data1))` by (
6836 (holfoot_ap_data_array_MAP_LIST e x' data2 =
7166 ``!e n data1 data2 st h1 h2 h.
7170 (st,h2) IN holfoot_ap_data_array (var_res_exp_const e) (var_res_exp_const n) data2 ==>
7171 ((h1 = h2) /\ (!tag dl1 dl2. MEM (tag, dl1) data1 /\ MEM (tag, dl2) data2 ==> (dl1 = dl2)))``,
7213 !tag dl1 dl2. MEM (tag,dl1) data1 /\ MEM (tag,dl2) data2 ==> (HD dl1 = HD dl2)` by (
7232 Q.ABBREV_TAC `L2 = MAP (\tl. (FST tl,(var_res_exp_const (HD (SND tl))):holfoot_a_expression)) data2` THEN
7254 Q.ABBREV_TAC `data2' = (MAP (\tl. (FST tl,TL (SND tl))) data2)` THEN
7256 !tag dl1 dl2. MEM (tag,dl1) data1' /\ MEM (tag,dl2) data2' ==> (dl1 = dl2)` by (
7257 Q.PAT_X_ASSUM `!e data1 data2 st h1 h2 h. X` MATCH_MP_TAC THEN
7266 Q.PAT_X_ASSUM `!e data1 data2 st h1 h2 h. X` (K ALL_TAC) THEN
7277 MAP_EVERY Q.UNABBREV_TAC [`data1'`, `data2'`] THEN
7287 ``!e1 e2 n1 n2 data1 data2 st h1 h2 h.
7295 (st,h2) IN holfoot_ap_data_array e2 n2 data2 /\
7297 ((h1 = h2) /\ (!tag dl1 dl2. MEM (tag, dl1) data1 /\ MEM (tag, dl2) data2 ==> (dl1 = dl2)))``,
7306 (st,h2) IN holfoot_ap_data_array e2 (var_res_exp_const nc) data2` by
7339 (st,h2) IN holfoot_ap_data_array (var_res_exp_const ec) (var_res_exp_const (SUC n)) data2` by
7348 ``!e n data1 data2 wpb rpb sfb_context sfb_split sfb_imp.
7350 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1) /\
7351 ALL_DISTINCT (MAP FST data2)) ==>
7360 (BAG_INSERT (holfoot_ap_data_array e n data2) sfb_imp)
7366 (EVERY (\x. MEM x data1) data2)) sfb_imp)``,
7398 MEM (tag,dl1) data1 /\ MEM (tag,dl2) data2 ==> (dl1 = dl2)` by (
7426 ``!e n data1 data2 sfb_restP wpb wpb' rpb sfb_context sfb_split sfb_imp sr.
7428 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1) /\
7429 ALL_DISTINCT (MAP FST data2) /\
7437 (BAG_INSERT (holfoot_ap_data_array e n data2) sfb_imp) sfb_restP) =
7443 (EVERY (\x. MEM x data1) data2)) sfb_imp)
7637 ``!e n data1 data2.
7638 (PERM data1 data2) ==>
7640 holfoot_ap_data_interval e n data2)``,
7648 ``!e1 e2 data1 data2 sfb_restP wpb wpb' rpb sfb_context sfb_split sfb_imp sr.
7650 (LIST_TO_SET (MAP FST data2) SUBSET LIST_TO_SET (MAP FST data1) /\
7651 ALL_DISTINCT (MAP FST data2) /\
7659 (BAG_INSERT (holfoot_ap_data_interval e1 e2 data2) sfb_imp) sfb_restP) =
7665 (EVERY (\x. MEM x data1) data2)) sfb_imp)