(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Chapter: Local Fan *) (* Author: Hoang Le Truong *) (* Date: 2012-04-01 *) (* ========================================================================= *) (* remaining conclusions from appendix to Local Fan chapter *) module Yxionxl2 = struct open Polyhedron;; open Sphere;; open Topology;; open Fan_misc;; open Planarity;; open Conforming;; open Hypermap;; open Fan;; open Topology;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Collect_geom;; open Dih2k_hypermap;; open Wjscpro;; open Tecoxbm;; open Hdplygy;; open Nkezbfc_local;; open Flyspeck_constants;; open Gbycpxs;; open Pcrttid;; open Local_lemmas1;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Hypermap;; open Fan;; open Wrgcvdr_cizmrrh;; open Local_lemmas;; open Flyspeck_constants;; open Pack_defs;; open Hales_tactic;; open Appendix;; open Zithlqn;; open Xwitccn;; open Ayqjtmd;; open Jkqewgv;; open Mtuwlun;; open Uxckfpe;; open Sgtrnaf;; open Yxionxl;; open Qknvmlb;; open Odxlstcv2;; let IN_SYM_0=prove(`a IN A ==> (-- a) IN IMAGE (\x:real^N. -- x) A`, REWRITE_TAC[IMAGE;IN_ELIM_THM;VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN SET_TAC[]);; let SUBSET_SYM_0=prove(`A SUBSET B ==> IMAGE (\x. -- x) A SUBSET IMAGE (\x:real^N. -- x) B`, REWRITE_TAC[SUBSET;IMAGE;IN_ELIM_THM;VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN ASM_TAC THEN SET_TAC[]);; let SET_EQ_SYM_0=prove(`A = B ==> IMAGE (\x. -- x) A = IMAGE (\x:real^N. -- x) B`, REWRITE_TAC[EXTENSION] THEN REPEAT RESA_TAC THEN EQ_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN ASM_TAC THEN SET_TAC[]);; let IMAGE_V_SYM_0=prove(`IMAGE (\i. --(vv:num->real^N) i) (:num)= IMAGE (\x. -- x) (IMAGE vv (:num))`, REWRITE_TAC[IMAGE;EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ EXISTS_TAC`(vv:num->real^N) x'` THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`x'':num` THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]]);; let UNIONS_IMAGE_FAN_SYM_0=prove_by_refinement(`UNIONS (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)) = IMAGE (\x:real^N. -- x) (UNIONS (IMAGE (\i. {vv i, vv (SUC i)}) (:num)))`, [REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[UNIONS;IMAGE;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,c} <=> a=b\/ a=c`] THEN RESA_TAC; EXISTS_TAC`(vv:num->real^N) x'` THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN EXISTS_TAC`{(vv:num->real^N) x', vv (SUC x')}` THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`(vv:num->real^N) (SUC x')` THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN EXISTS_TAC`{(vv:num->real^N) x', vv (SUC x')}` THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,a}`] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,c} <=> a=b\/ a=c`] THEN RESA_TAC; EXISTS_TAC`{--(vv:num->real^N) x', --vv (SUC x')}` THEN ASM_REWRITE_TAC[SET_RULE`a IN {a,b}`] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`{--(vv:num->real^N) x', --vv (SUC x')}` THEN ASM_REWRITE_TAC[SET_RULE`a IN {b,a}`] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]]);; let FINITE_SYM_0=prove(`FINITE A ==> FINITE (IMAGE (\x:real^N. -- x) A)`, SIMP_TAC[FINITE_IMAGE]);; let CARD_SYM_0=prove(`FINITE A ==> CARD (IMAGE (\x:real^N. -- x) A)= CARD A`, STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`]);; let ELEMENT2_SYM_0=prove(`{--a, --b}= IMAGE (\x:real^N. --x) {a,b}`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;SET_RULE`a IN{b,c} <=> a=b\/ a=c`] THEN GEN_TAC THEN EQ_TAC THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`] THEN SET_TAC[]);; let GRAPH_SYM_0=prove(`graph (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num)) ==> graph (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))`, REWRITE_TAC[GRAPH;HAS_SIZE;IMAGE;IN_ELIM_THM] THEN STRIP_TAC THEN GEN_TAC THEN RESA_TAC THEN SUBGOAL_THEN `(?x'. x' IN (:num) /\ {(vv:num->real^N) x, vv (SUC x)} = {vv x', vv (SUC x')})`ASSUME_TAC THENL[ EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th1-> REPEAT DISCH_TAC THEN MRESA_TAC th1[`{(vv:num->real^N) x, vv (SUC x)}`]) THEN ASM_SIMP_TAC[ELEMENT2_SYM_0;FINITE_SYM_0;CARD_SYM_0]]);; let NOT_SUBSET_EMPTY_SYM_0=prove(`~(A SUBSET {}) ==> ~(IMAGE (\x:real^N. --x) A SUBSET {})`, REWRITE_TAC[SET_RULE`~(A SUBSET {}) <=> ?a. a IN A`] THEN RESA_TAC THEN EXISTS_TAC`-- a:real^N` THEN ASM_SIMP_TAC[IN_SYM_0]);; let NOT_EMPTY_SYM_0=prove(`~(A ={}) ==> ~(IMAGE (\x:real^N. --x) A = {})`, REWRITE_TAC[SET_RULE`~(A = {}) <=> ?a. a IN A`] THEN RESA_TAC THEN EXISTS_TAC`-- a:real^N` THEN ASM_SIMP_TAC[IN_SYM_0]);; let REFL_SYM_0=prove(`IMAGE (\x:real^N. --x) (IMAGE (\x. --x) A) =A`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`] THEN EXISTS_TAC`--x:real^N` THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`] THEN EXISTS_TAC`x:real^N` THEN ASM_REWRITE_TAC[]);; let IMAGE_E_SYM_0=prove(`e IN IMAGE (\i. {--vv i, --vv (SUC i)}) (:num) ==> IMAGE (\x:real^N. --x) e IN IMAGE (\i. {vv i, vv (SUC i)}) (:num)`, REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[EXTENSION;IN_ELIM_THM;SET_RULE`a IN {b,c} <=> a=b\/ a=c`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`] THENL[ EXISTS_TAC`-- (vv:num->real^N) x` THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`]; EXISTS_TAC`-- (vv:num->real^N) (SUC x)` THEN ASM_SIMP_TAC[VECTOR_ARITH`(-- --a=a:real^N)`]]);; let COLLINEAR_SYM_0=prove(`(collinear e) ==> (collinear (IMAGE (\x:real^N. --x) e))`, REWRITE_TAC[collinear;IMAGE;IN_ELIM_THM] THEN RESA_TAC THEN EXISTS_TAC`--u:real^N` THEN REPEAT RESA_TAC THEN ASM_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x':real^N`;`x'':real^N`]) THEN EXISTS_TAC`c:real` THEN ASM_REWRITE_TAC[VECTOR_ARITH`c % --u = --(c % u)/\ -- a - -- b= --(a-b:real^N)`]);; let UNION_SYM_0=prove(`IMAGE (\x:real^N. --x) (s UNION e) = (IMAGE (\x:real^N. --x) s) UNION (IMAGE (\x:real^N. --x) e)`, SIMP_TAC[IMAGE_UNION]);; let VEC0_SYM_0=prove(`IMAGE (\x:real^N. --x) {vec 0}= {vec 0}`, REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION] THEN EXISTS_TAC`vec 0:real^N` THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;IN_SING;VECTOR_ARITH`-- vec 0=vec 0`;EXTENSION]);; let VEC0_UNION_SYM_0=prove(`IMAGE (\x:real^N. --x) ({vec 0} UNION e) = {vec 0} UNION (IMAGE (\x:real^N. --x) e)`, ASM_SIMP_TAC[UNION_SYM_0;VEC0_SYM_0]);; let NOT_COLLINEAR_SYM_0=prove(`~(collinear e) ==> ~(collinear (IMAGE (\x:real^N. --x) e))`, REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_SYM_0)[`IMAGE (\x:real^N. --x) (e:real^N->bool)`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[REFL_SYM_0]);; let VEC0_NOT_COLLINEAR_SYM_0=prove(`~(collinear ({vec 0} UNION e)) ==> ~(collinear ({vec 0} UNION (IMAGE (\x:real^N. --x) e)))`, REPEAT STRIP_TAC THEN MRESAL_TAC(GEN_ALL NOT_COLLINEAR_SYM_0)[`{vec 0} UNION (e:real^N->bool)`] [VEC0_UNION_SYM_0]);; let IMAGE_E_UNION_V_SYM_0=prove(`e IN IMAGE (\i. {--vv i, --vv (SUC i)}) (:num) UNION {{v} | v IN IMAGE (\i. --vv i) (:num)} ==> IMAGE (\x:real^N. --x) e IN IMAGE (\i. {vv i, vv (SUC i)}) (:num) UNION {{v} | v IN IMAGE vv (:num)}`, REWRITE_TAC[UNION;IN_ELIM_THM] THEN MATCH_MP_TAC(SET_RULE`(A==>A1)/\ (B==>B1)==> (A\/B==> A1\/B1)`) THEN ASM_SIMP_TAC[IMAGE_E_SYM_0] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN RESA_TAC THEN REWRITE_TAC[IN_SING] THEN EXISTS_TAC`(vv:num->real^N) x` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL[ EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[]; REWRITE_TAC[EXTENSION;IN_ELIM_THM;IN_SING] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`] THEN EXISTS_TAC`-- (vv:num->real^N) x` THEN ASM_SIMP_TAC[VECTOR_ARITH`-- -- A=A:real^N`]]);; let LINAER_SYM_0=prove(`linear (\x:real^N. --x)`, ASM_SIMP_TAC[VECTOR_ARITH`--(x+y)= -- x+ -- y:real^N`;linear] THEN VECTOR_ARITH_TAC);; let AFF_GE_COMMUTATIVE_SYM_0=prove(`aff_ge (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_ge e1 e)`, MATCH_MP_TAC AFF_GE_INJECTIVE_LINEAR_IMAGE THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);; let AFF_GE_VEC0_SYM_0=prove(`aff_ge {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_ge {vec 0} e)`, GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0] THEN ASM_SIMP_TAC[AFF_GE_COMMUTATIVE_SYM_0]);; let AFF_GT_COMMUTATIVE_SYM_0=prove(`aff_gt (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_gt e1 e)`, MATCH_MP_TAC AFF_GT_INJECTIVE_LINEAR_IMAGE THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);; let AFF_GT_VEC0_SYM_0=prove(`aff_gt {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_gt {vec 0} e)`, GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0] THEN ASM_SIMP_TAC[AFF_GT_COMMUTATIVE_SYM_0]);; let AFF_LE_COMMUTATIVE_SYM_0=prove(`aff_le (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_le e1 e)`, MATCH_MP_TAC AFF_LE_INJECTIVE_LINEAR_IMAGE THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);; let AFF_LE_VEC0_SYM_0=prove(`aff_le {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_le {vec 0} e)`, GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0] THEN ASM_SIMP_TAC[AFF_LE_COMMUTATIVE_SYM_0]);; let AFF_LT_COMMUTATIVE_SYM_0=prove(`aff_lt (IMAGE (\x. --x) e1) (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_lt e1 e)`, MATCH_MP_TAC AFF_LT_INJECTIVE_LINEAR_IMAGE THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- x= -- y==> x=y:real^N`;LINAER_SYM_0]);; let AFF_LT_VEC0_SYM_0=prove(`aff_lt {vec 0} (IMAGE (\x. --x) e) = IMAGE (\x:real^N. --x) (aff_lt {vec 0} e)`, GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[GSYM VEC0_SYM_0] THEN ASM_SIMP_TAC[AFF_LT_COMMUTATIVE_SYM_0]);; let INTER_SYM_0=prove(`IMAGE (\x:real^N. --x) (e1 INTER e2) =IMAGE (\x. --x) e1 INTER IMAGE (\x. --x) e2`, MATCH_MP_TAC IMAGE_INTER_INJ THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC);; let FAN_SYM_0=prove_by_refinement(`FAN (vec 0, IMAGE (vv:num->real^3) (:num), IMAGE (\i. {vv i, vv (SUC i)}) (:num)) ==> FAN (vec 0, IMAGE (\i. -- vv i) (:num), IMAGE (\i. {-- vv i, -- vv (SUC i)}) (:num))`, [REWRITE_TAC[FAN;fan1;fan2;fan6;fan7] THEN REPEAT RESA_TAC; ASM_SIMP_TAC[UNIONS_IMAGE_FAN_SYM_0;IMAGE_V_SYM_0;SUBSET_SYM_0]; ASM_SIMP_TAC[GRAPH_SYM_0]; ASM_SIMP_TAC[IMAGE_V_SYM_0;FINITE_SYM_0]; POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[IMAGE_V_SYM_0;SUBSET_SYM_0;NOT_SUBSET_EMPTY_SYM_0]; POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[IMAGE_V_SYM_0;SUBSET_SYM_0;NOT_SUBSET_EMPTY_SYM_0] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL IN_SYM_0)[`vec 0:real^3`;`IMAGE (\x:real^3. --x) (IMAGE (vv:num->real^3) (:num))`][VECTOR_ARITH`-- vec 0= vec 0`;REFL_SYM_0]; POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL IMAGE_E_SYM_0)[`e:real^3->bool`;`vv:num->real^3`] THEN REPLICATE_TAC (10-7)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC th[`IMAGE (\x:real^3. --x) e`]) THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`IMAGE (\x:real^3. --x) e`][REFL_SYM_0]; MRESA_TAC (GEN_ALL IMAGE_E_UNION_V_SYM_0)[`e1:real^3->bool`;`vv:num->real^3`] THEN MRESA_TAC (GEN_ALL IMAGE_E_UNION_V_SYM_0)[`e2:real^3->bool`;`vv:num->real^3`] THEN REPLICATE_TAC (12-8)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MRESAL_TAC th[`IMAGE (\x:real^3. --x) e1`;`IMAGE (\x:real^3. --x) e2`][]) THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[AFF_GE_VEC0_SYM_0;GSYM INTER_SYM_0] THEN MRESAL_TAC(GEN_ALL SET_EQ_SYM_0)[`IMAGE (\x:real^3. --x) (aff_ge {vec 0} e1 INTER aff_ge {vec 0} e2)`;`IMAGE (\x:real^3. --x) (aff_ge {vec 0} (e1 INTER e2))`][REFL_SYM_0]]);; let OPP_SUC_MOD=prove(`~(k=0)==>k - SUC ((k - SUC (x MOD k)) MOD k) = x MOD k` , RESA_TAC THEN MRESA_TAC DIVISION[`k- SUC(x MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`x:num`;`k:num`] THEN MP_TAC(ARITH_RULE`x MOD k < k ==> k- SUC(x MOD k) (k - SUC ((k - SUC (x MOD k)) MOD k) = x MOD k) <=> k -SUC( x MOD k) = (k - SUC (x MOD k)) MOD k`) THEN RESA_TAC);; let OPP_IMAGE_V_EQ=prove(`periodic vv k/\ ~(k=0) ==> IMAGE (\i. vv (k - SUC (i MOD k))) (:num)= IMAGE vv (:num)`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`k - SUC (x' MOD k)` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; RESA_TAC THEN EXISTS_TAC`k- SUC(x' MOD k)` THEN ASM_SIMP_TAC[OPP_SUC_MOD;SET_RULE`(a:num)IN (:num)`;PERIODIC_PROPERTY]]);; let MOD_SUC_MOD=prove(`1 SUC (x MOD k) MOD k= SUC x MOD k`, STRIP_TAC THEN REWRITE_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_ADD_MOD[`x:num`;`1:num`;`k:num`]);; let SUC_MOD_EQ_MOD_SUC=prove(`1(k - SUC (x MOD k)) MOD k =(k - SUC x MOD k) MOD k`, STRIP_TAC THEN REWRITE_TAC[ADD1] THEN MP_TAC(ARITH_RULE`1 ~(k=0)/\ k - (k - 1 + 1)=0/\ k - 1 + 1=k/\ k-k=0/\ 0 REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESA_TAC MOD_LT[`0`;`k:num`] THEN MRESA_TAC DIVISION[`x:num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`0:num`][ARITH_RULE`1*k+0=k`] THEN MP_TAC(ARITH_RULE`x MOD k< k/\ 1 x MOD k= k-1\/ x MOD k +1< k`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`x MOD k +1`;`k:num`]);; let OPP_IMAGE_E_EQ=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. {vv (k - SUC (i MOD k)), vv (k - SUC (SUC i MOD k))}) (:num) =IMAGE (\i. {vv i, vv (SUC i)}) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let OPP_IMAGE_F_EQ=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. vv (k - SUC (SUC i MOD k)),vv (k - SUC (i MOD k))) (:num) =IMAGE (\i. vv i, vv (SUC i)) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let OPP_IMAGE_F_EQ2=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. vv (k - SUC (i MOD k)),vv (k - SUC (SUC i MOD k))) (:num) =IMAGE (\i. vv (SUC i),vv i ) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let BALL_ANNULUS_SYM_0=prove(`-- v IN ball_annulus <=> v IN ball_annulus`, ASM_SIMP_TAC[ball_annulus;IN_ELIM_THM;DIFF;cball;ball;dist;VECTOR_ARITH`vec 0- A= -- A/\ -- --A=A`;NORM_NEG]);; let DIST_SYM_0=prove(`dist(-- a, -- b)= dist(a,b:real^N)`, ASM_SIMP_TAC[dist;VECTOR_ARITH`--a - --b= --(a-b):real^N`;NORM_NEG]);; let OPP_FAN_SYM_0=prove(` 3<=k /\ periodic vv k /\ FAN (vec 0, IMAGE (vv:num->real^3) (:num), IMAGE (\i. {vv i, vv (SUC i)}) (:num)) ==> FAN (vec 0,IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num))`, STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`] THEN MRESA_TAC(GEN_ALL OPP_IMAGE_V_EQ)[`k:num`;`vv:num->real^3`] THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[FAN_SYM_0]);; let ORD_PAIRS_E_VV=prove(`ord_pairs (IMAGE (\i. {vv i, vv (SUC i)}) (:num)) =IMAGE (\i. vv i, vv (SUC i)) (:num) UNION IMAGE (\i. vv (SUC i),vv i) (:num) `, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[ord_pairs;IMAGE;IN_ELIM_THM;UNION;SET_RULE`{a,b}={c,d}<=> (a=c/\ b=d)\/ (a=d/\ b=c)`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN SET_TAC[]);; let SELF_PAIR_EMPTY_VV=prove(`self_pairs (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num)) (IMAGE vv (:num))={}`, REWRITE_TAC[SET_RULE`A={}<=> ~(?a. a IN A)`;self_pairs;IN_ELIM_THM;EE;IMAGE] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN POP_ASSUM (fun th-> STRIP_TAC THEN MP_TAC th THEN ASM_REWRITE_TAC[]) THEN EXISTS_TAC`(vv:num->real^N) (SUC x)` THEN EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[]);; let DART_OF_HYP_VV=prove(`darts_of_hyp (IMAGE (\i. {(vv:num->real^N) i, vv (SUC i)}) (:num)) (IMAGE vv (:num)) = IMAGE (\i. vv i, vv (SUC i)) (:num) UNION IMAGE (\i. vv (SUC i),vv i) (:num)`, ASM_SIMP_TAC[darts_of_hyp;SELF_PAIR_EMPTY_VV;ORD_PAIRS_E_VV] THEN SET_TAC[]);; let PAIR_FUN_SYM_0=prove(`IMAGE (\i. -- vv1 i, -- vv2 i) (:num) = IMAGE(\(x:real^N,y:real^N). --x, --y) (IMAGE (\i. vv1 i, vv2 i) (:num))`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ EXISTS_TAC` (vv1 :num->real^N) x', (vv2 :num->real^N) x'` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`x'':num` THEN ASM_REWRITE_TAC[]]);; let IN_PAIR_SYM_0=prove(`a IN A==> (\(x:real^N,y:real^N). --x, --y) a IN IMAGE(\(x:real^N,y:real^N). --x, --y) A`, ASM_SIMP_TAC[FUN_IN_IMAGE]);; let ID_SYM_0_PRIME=prove(`(\(x:real^N,y). --x,--y) ((\(x,y). --x,--y) (a:real^N,b:real^N)) = (a,b)` , ASM_REWRITE_TAC[VECTOR_ARITH`-- -- a= a:real^N`]);; let ID_SYM_0=prove(`(\(x:real^N,y). --x,--y) ((\(x,y). --x,--y) x) = (x:real^N#real^N)`, MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN ASM_REWRITE_TAC[VECTOR_ARITH`-- -- a= a:real^N`]);; let ID_PAIR_SYM_0=prove(`IMAGE (\(x,y):real^N#real^N. --x,--y) (IMAGE (\(x,y). --x,--y) A)=A`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THEN ASM_SIMP_TAC[ID_SYM_0] THEN EXISTS_TAC`(\(x,y):real^N#real^N. --x,--y) x` THEN ASM_SIMP_TAC[ID_SYM_0] THEN EXISTS_TAC`x:real^N#real^N` THEN ASM_REWRITE_TAC[]);; let IN_EQ_PAIR_SYM_0=prove(` (\(x:real^N,y:real^N). --x, --y) a IN IMAGE(\(x:real^N,y:real^N). --x, --y) A<=> a IN A`, EQ_TAC THENL[ STRIP_TAC THEN MRESAL_TAC (GEN_ALL IN_PAIR_SYM_0)[`(\(x:real^N,y:real^N). --x,--y) a`;`IMAGE(\(x:real^N,y:real^N). --x, --y) A`][ID_PAIR_SYM_0;ID_SYM_0]; ASM_SIMP_TAC[FUN_IN_IMAGE];]);; let FST_SND_PAIR_SYM_0=prove(`FST ((\(x,y):real^N#real^N. --x,--y) x)= -- FST x /\ SND ((\(x,y):real^N#real^N. --x,--y) x)= -- SND x`, MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[]);; let EQ_SET_PAIR_SYM_0=prove(`IMAGE (\(x,y):real^N#real^N. --x,--y) A =IMAGE (\(x,y). --x,--y) B <=> A=B`, EQ_TAC THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN SIMP_TAC[EXTENSION;IN_EQ_PAIR_SYM_0] THEN REPEAT STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[` (\(x,y):real^N#real^N. --x,--y) x:real^N#real^N`][IN_EQ_PAIR_SYM_0]));; let EE_SYM_0=prove_by_refinement(`EE (--a) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)) = IMAGE(\x:real^N. --x)(EE (a) (IMAGE (\i. {vv i, vv (SUC i)}) (:num)) )`, [REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[EE;IMAGE;IN_ELIM_THM;SET_RULE`{a,b}={c,d}<=> (a=c/\b=d)\/ (a=d/\ b=c)`;VECTOR_ARITH`--a= --b<=> a=b:real^N`] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC; EXISTS_TAC`(vv:num->real^N) (SUC x')` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`(vv:num->real^N) (x')` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`(x'':num)` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`(x'':num)` THEN ASM_REWRITE_TAC[]]);; let EMPTY_EQ_SYM_0=prove(` (IMAGE (\x:real^N. --x) A = {}) <=> (A ={})`, EQ_TAC THENL[ ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN ASM_SIMP_TAC[NOT_EMPTY_SYM_0]; ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN MRESAL_TAC (GEN_ALL NOT_EMPTY_SYM_0)[`IMAGE (\x. --x) (A:real^N->bool)`][REFL_SYM_0];]);; let EE_EXPAND_BB_VV=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> EE (vv i) E= {vv (SUC i),vv (i+k-1)}`, [ REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF] THEN STRIP_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[convex_local_fan] THEN STRIP_TAC THEN SUBGOAL_THEN`(vv:num->real^3) i IN V` ASSUME_TAC; EXPAND_TAC"V" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`]; MRESA_TAC (GEN_ALL Local_lemmas1.LOFA_IMP_EE_TWO_ELMS_INS_ND)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) i`] THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3 MRESA_TAC th[`(vv:num->real^3) i`]) THEN MRESAL_TAC(GEN_ALL VV_SUC_EQ_RHO_NODE_PRIME)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`k:num`;`s:scs_v39`;`FF:real^3#real^3->bool`;`(vv:num->real^3) i:real^3`;`vv:num->real^3`;`i:num`] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan] THEN POP_ASSUM(fun th-> MRESAL_TAC th[`SUC 0`][ITER;ARITH_RULE`SUC 0 +i= SUC i`] THEN MRESA_TAC th[`k-1`]) THEN REWRITE_TAC[ARITH_RULE`k-1+i= i+k-1`]]);; let AZIM_CYCLE1_SYM_0=prove(` scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> azim_cycle (IMAGE (\x. --x) (EE (vv i) E)) (vec 0) (--vv i) (--vv (SUC i)) = --azim_cycle (EE (vv i) E) (vec 0) (vv i) (vv (SUC i))`, RESA_TAC THEN MP_TAC EE_EXPAND_BB_VV THEN RESA_TAC THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]);; let AZIM_CYCLE2_SYM_0=prove(` scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> azim_cycle (IMAGE (\x. --x) (EE (vv i) E)) (vec 0) (--vv i) (--vv (i + k-1)) = --azim_cycle (EE (vv i) E) (vec 0) (vv i) (vv (i+k-1))`, RESA_TAC THEN MP_TAC EE_EXPAND_BB_VV THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]);; let IVS_AZIM_CYCLE_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv /\ x IN darts_of_hyp E V ==> ivs_azim_cycle (EE (--SND x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (vec 0) (--SND x) (--FST x) = -- ivs_azim_cycle (EE (SND x) E) (vec 0) (SND x) (FST x)`, [ RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN EXPAND_TAC"FF" THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE] THEN REWRITE_TAC[IN_ELIM_THM] THEN RESA_TAC; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC; MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic] THEN REPEAT RESA_TAC; ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN ASM_SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]]);; let ff_FUN_COMMUTATIVE_SYM_0=prove(` scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!x. ff_of_hyp (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) (ff_of_hyp (vec 0,V,E) x)) `, RESA_TAC THEN GEN_TAC THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0] THEN MP_TAC(SET_RULE`x IN darts_of_hyp (E:(real^3->bool)->bool) V \/ ~(x IN darts_of_hyp E V)`) THEN RESA_TAC THENL[ POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN RESA_TAC THEN MP_TAC IVS_AZIM_CYCLE_SYM_0 THEN RESA_TAC; POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN RESA_TAC]);; let FUN_COMMUTATIVE=prove(`(!x. f(g x)= g(f1 x)) ==> !n x. (f POWER n) (g x) = g((f1 POWER n) x)`, STRIP_TAC THEN INDUCT_TAC THENL[ ASM_REWRITE_TAC[POWER;I_DEF]; ASM_REWRITE_TAC[POWER;o_DEF]]);; let ff_POWER_COMMUTATIVE_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> !n x. (ff_of_hyp (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)) POWER n) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) ( (ff_of_hyp (vec 0,IMAGE vv (:num),IMAGE (\i. {vv i, vv (SUC i)}) (:num)) POWER n) x) `, RESA_TAC THEN MATCH_MP_TAC FUN_COMMUTATIVE THEN MATCH_MP_TAC ff_FUN_COMMUTATIVE_SYM_0 THEN ASM_REWRITE_TAC[]);; let FACE_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> face (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) ((\(x,y). --x,--y) x) = IMAGE (\(x,y). --x,--y) (face (hypermap (HYP (vec 0,V,E))) x)`, STRIP_TAC THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;] THEN REPEAT RESA_TAC THEN MP_TAC FAN_SYM_0 THEN RESA_TAC THEN REWRITE_TAC[face] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[IMAGE] THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ EXISTS_TAC`(ff_of_hyp (vec 0,V,E) POWER n) x` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[]]);; let OPP_IMAGE_V_EQ_NEG=prove(`periodic vv k/\ ~(k=0) ==> IMAGE (\i. -- (vv:num->real^3) (k - SUC (i MOD k))) (:num)= IMAGE (\i. -- vv i) (:num)`, REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`k - SUC (x' MOD k)` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; RESA_TAC THEN EXISTS_TAC`k- SUC(x' MOD k)` THEN ASM_SIMP_TAC[OPP_SUC_MOD;SET_RULE`(a:num)IN (:num)`;PERIODIC_PROPERTY]]);; let OPP_IMAGE_E_EQ_NEG=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num) =IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let OPP_IMAGE_F_EQ_NEG=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--vv (k - SUC (i MOD k))) (:num) =IMAGE (\i. --vv i, --vv (SUC i)) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let OPP_IMAGE_F_EQ2_NEG=prove(`periodic (vv:num->real^3) k/\ 1 IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num) =IMAGE (\i. --vv (SUC i),--vv i ) (:num)`, ONCE_REWRITE_TAC[EXTENSION] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;] THEN REPEAT STRIP_TAC THEN EQ_TAC THENL[ RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN(:num)`;MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC DIVISION[`SUC x'`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x' MOD k< k==> SUC (k - SUC (SUC x' MOD k)) =k - SUC x' MOD k`) THEN RESA_TAC THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (x' MOD k)`] THEN MRESA_TAC th[`k - SUC x' MOD k`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[SUC_MOD_EQ_MOD_SUC]; RESA_TAC THEN MP_TAC(ARITH_RULE`1 ~(k=0)`) THEN RESA_TAC THEN EXISTS_TAC`(k - SUC(SUC(x' MOD k)MOD k))` THEN ASM_SIMP_TAC[SET_RULE`(a:num)IN (:num)`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`SUC(x' MOD k)`;`k:num`] THEN MRESA_TAC DIVISION[`SUC(x' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC(x' MOD k) MOD k SUC (k - SUC (SUC (x' MOD k) MOD k))= k-(SUC(x' MOD k) MOD k)`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL MOD_SUC_MOD)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`SUC (k - SUC(SUC (x' MOD k)MOD k))`;`k:num`] THEN MRESA_TAC (GEN_ALL SUC_MOD_EQ_MOD_SUC)[`x':num`;`k:num`] THEN MRESA_TAC (GEN_ALL OPP_SUC_MOD)[`x':num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num`] THEN MRESA_TAC th[`SUC x'`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[]]);; let CARD_PAIR_SYM_0=prove(`FINITE s ==> CARD (IMAGE (\(x,y):real^N#real^N. --x,--y) s) =CARD s`, STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ THEN RESA_TAC THEN RESA_TAC THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ] THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN MP_TAC(SET_RULE`y=(FST (y:real^N#real^N),SND (y:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ] THEN ASM_REWRITE_TAC[GSYM PAIR_EQ] THEN RESA_TAC);; let FACE_ALL_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!x. face (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) ((\(x,y). --x,--y) x) = IMAGE (\(x,y). --x,--y) (face (hypermap (HYP (vec 0,V,E))) x))`, REPEAT STRIP_TAC THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;] THEN REPEAT RESA_TAC THEN MP_TAC FAN_SYM_0 THEN RESA_TAC THEN REWRITE_TAC[face] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN GEN_REWRITE_TAC(RAND_CONV o ONCE_DEPTH_CONV)[IMAGE] THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ EXISTS_TAC`(ff_of_hyp (vec 0,V,E) POWER n) x` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`n:num` THEN ASM_REWRITE_TAC[]]);; let AZIM_CYCLE_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv /\ x IN darts_of_hyp E V ==> azim_cycle (EE (--SND x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (vec 0) (--SND x) (--FST x) = -- azim_cycle (EE (SND x) E) (vec 0) (SND x) (FST x)`, [RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN EXPAND_TAC"FF" THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE] THEN REWRITE_TAC[IN_ELIM_THM] THEN RESA_TAC; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC; MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic] THEN REPEAT RESA_TAC; ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0] ]);; let FST_SND_EQ_PAIR_SYM_0=prove(`(\(x,y):real^N#real^N. --x,--y)x= --FST x,--SND x`, MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[]);; let SYM_AZIM_CYCLE_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv /\ x IN darts_of_hyp E V ==> azim_cycle (EE (--FST x) (IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (vec 0) (--FST x) (--SND x) = -- azim_cycle (EE (FST x) E) (vec 0) (FST x) (SND x)`, [RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN EXPAND_TAC"FF" THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM;IMAGE] THEN REWRITE_TAC[IN_ELIM_THM] THEN RESA_TAC; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`x':num`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]; MRESA_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`] THEN ASM_SIMP_TAC[EE_SYM_0] THEN SUBGOAL_THEN`vv (SUC x' + k - 1) = (vv:num->real^3) x'`ASSUME_TAC; MP_TAC(ARITH_RULE`~(k<=3)==> SUC x' + k - 1= x' +k`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;periodic] THEN REPEAT RESA_TAC; ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0]; ]);; let NODE_MAP_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!x. (node_map (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) (node_map (hypermap (HYP (vec 0,V,E))) x))`, STRIP_TAC THEN GEN_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC th THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;] THEN REPEAT RESA_TAC ) THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC FAN_SYM_0 THEN RESA_TAC THEN ASM_SIMP_TAC[Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;FUN_EQ_THM] THEN MP_TAC(SET_RULE`x=(FST (x:real^3#real^3),SND (x:real^3#real^3))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN ASM_SIMP_TAC[nn_of_hyp;] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0;Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP] THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN ASM_SIMP_TAC[GSYM FST_SND_EQ_PAIR_SYM_0;IN_EQ_PAIR_SYM_0] THEN MP_TAC(SET_RULE`x IN FF UNION IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) \/ ~(x IN FF UNION IMAGE (\i. vv (SUC i),vv i) (:num))`) THEN RESA_TAC THEN MP_TAC SYM_AZIM_CYCLE_SYM_0 THEN RESA_TAC);; let IMAGE_NODE_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!A. IMAGE (node_map (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (IMAGE (\(x,y). --x,--y) A) = IMAGE (\(x,y). --x,--y) (IMAGE (node_map (hypermap (HYP (vec 0,V,E)))) A))`, RESA_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[EXTENSION;IN_ELIM_THM] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN MP_TAC NODE_MAP_SYM_0 THEN RESA_TAC THEN EXISTS_TAC`node_map (hypermap (HYP (vec 0,V,E))) x''` THEN ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE] THEN EXISTS_TAC`x'':real^3#real^3` THEN ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN MP_TAC NODE_MAP_SYM_0 THEN RESA_TAC THEN EXISTS_TAC`(\(x,y):real^3#real^3. --x,--y) x''` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[IN_ELIM_THM;IMAGE] THEN EXISTS_TAC`x'':real^3#real^3` THEN ASM_REWRITE_TAC[]]);; let COMMUTATIVE_POINT_PAIR_0=prove(`(\(x,y):real^N#real^N. --x,--y) a= b <=> a= (\(x,y). --x,--y) b `, EQ_TAC THENL[ STRIP_TAC THEN MRESA_TAC(GEN_ALL ID_SYM_0)[`a:real^N#real^N`]; STRIP_TAC THEN MRESA_TAC(GEN_ALL ID_SYM_0)[`b:real^N#real^N`]]);; let EDGE_MAP_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!x. (edge_map (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) (edge_map (hypermap (HYP (vec 0,V,E))) x))`, STRIP_TAC THEN GEN_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN ASSUME_TAC th THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;local_fan;] THEN REPEAT RESA_TAC ) THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC FAN_SYM_0 THEN RESA_TAC THEN ASM_SIMP_TAC[Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP;FUN_EQ_THM] THEN MP_TAC(SET_RULE`x=(FST (x:real^3#real^3),SND (x:real^3#real^3))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN ASM_SIMP_TAC[ee_of_hyp;] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN STRIP_TAC THEN ASM_SIMP_TAC[ff_of_hyp2;DART_OF_HYP_VV;PAIR_FUN_SYM_0;IN_EQ_PAIR_SYM_0;GSYM IMAGE_UNION;FST_SND_PAIR_SYM_0;Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP] THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN ASM_SIMP_TAC[GSYM FST_SND_EQ_PAIR_SYM_0;IN_EQ_PAIR_SYM_0] THEN MP_TAC(SET_RULE`x IN FF UNION IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) \/ ~(x IN FF UNION IMAGE (\i. vv (SUC i),vv i) (:num))`) THEN RESA_TAC);; let EDGE_POWER_MAP_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!n x. (edge_map (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) POWER n) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) ((edge_map (hypermap (HYP (vec 0,V,E))) POWER n) x))`, RESA_TAC THEN MATCH_MP_TAC FUN_COMMUTATIVE THEN MATCH_MP_TAC EDGE_MAP_SYM_0 THEN ASM_REWRITE_TAC[]);; let NODE_POWER_MAP_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> (!n x. (node_map (hypermap (HYP (vec 0,IMAGE (\i. --vv i) (:num),IMAGE (\i. {--vv i, --vv (SUC i)}) (:num)))) POWER n) ((\(x,y). --x,--y) x) = (\(x,y). --x,--y) ((node_map (hypermap (HYP (vec 0,V,E))) POWER n) x))`, RESA_TAC THEN MATCH_MP_TAC FUN_COMMUTATIVE THEN MATCH_MP_TAC NODE_MAP_SYM_0 THEN ASM_REWRITE_TAC[]);; let LOCAL_FAN_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> local_fan (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num), IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--vv (k - SUC (i MOD k))) (:num))`, [ STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1 REPEAT STRIP_TAC THEN MP_TAC th) THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC (SYM th)) THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN MP_TAC OPP_FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2] THEN GEN_REWRITE_TAC(RAND_CONV o LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN EXISTS_TAC`(\(x:real^3,y:real^3). --x,--y) x` THEN ASM_SIMP_TAC[UNION;IN_ELIM_THM;IN_PAIR_SYM_0;] THEN MP_TAC FACE_SYM_0 THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG] ; REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC (SYM th)) THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV] THEN MP_TAC OPP_FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2] THEN GEN_REWRITE_TAC(RAND_CONV o LAND_CONV o DEPTH_CONV)[UNION;IN_ELIM_THM] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[dih2k] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN REPEAT STRIP_TAC; MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`] THEN REPLICATE_TAC (28-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SYM th]); ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;] THEN REPEAT RESA_TAC THEN MP_TAC FACE_ALL_SYM_0 THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0]) THEN MP_TAC IMAGE_NODE_SYM_0 THEN RESA_TAC THEN ASM_SIMP_TAC[GSYM IMAGE_UNION] THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num) UNION IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k))) (:num)`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`] THEN STRIP_TAC THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`] ) THEN SET_TAC[] ; REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (ff_of_hyp (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (x) = (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; MP_TAC FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][] THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (39-14)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC EDGE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (edge_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC NODE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (node_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); (*******) MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`] THEN REPLICATE_TAC (28-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SYM th]); ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;] THEN REPEAT RESA_TAC THEN MP_TAC FACE_ALL_SYM_0 THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0]) THEN MP_TAC IMAGE_NODE_SYM_0 THEN RESA_TAC THEN ASM_SIMP_TAC[GSYM IMAGE_UNION] THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num) UNION IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k))) (:num)`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`] THEN STRIP_TAC THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`] ) THEN SET_TAC[] ; REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (ff_of_hyp (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (x) = (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; MP_TAC FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][] THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (39-14)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC EDGE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (edge_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC NODE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (node_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); ]);; let POINT_IN_AFF_LT_SYM_0=prove(` DISJOINT {vec 0,v1} {w2} ==> -- w2 IN aff_lt {vec 0,v1} {w2}`, STRIP_TAC THEN ASM_SIMP_TAC[AFF_LT_2_1;IN_ELIM_THM] THEN EXISTS_TAC`&2` THEN EXISTS_TAC`&0` THEN EXISTS_TAC`-- &1` THEN REWRITE_TAC[REAL_ARITH`-- &1< &0/\ &2 + &0 + -- &1 = &1`] THEN VECTOR_ARITH_TAC);; let COLLINEAR_POINT_SYM_0=prove(`~collinear {vec 0, v1, w1} ==> ~collinear {vec 0, v1, --w1}`, REWRITE_TAC[COLLINEAR_LEMMA;IMAGE;IN_ELIM_THM;VECTOR_ARITH`-- a= vec 0<=> a= vec 0`] THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> STRIP_TAC THEN MP_TAC th THEN ASM_REWRITE_TAC[]) THEN MATCH_MP_TAC(SET_RULE`A==> B\/C\/A`) THEN EXISTS_TAC`--c:real` THEN POP_ASSUM MP_TAC THEN VECTOR_ARITH_TAC);; let AZIM_EQ_PI_POINT_SYM_0=prove(`~collinear {vec 0, v1, w1:real^3} ==> azim (vec 0) v1 w1 (--w1) = pi`, STRIP_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN ASM_SIMP_TAC[AZIM_EQ_PI] THEN MRESAL_TAC (GEN_ALL POINT_IN_AFF_LT_SYM_0)[`v1:real^3`;`-- w1:real^3`][VECTOR_ARITH`-- --A=A:real^3`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[Fan.th3a]);; let SUM_AZIM_SYM_0=prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2} /\ azim (vec 0) v1 w1 w2<= pi ==> azim (vec 0) v1 w1 w2 + azim (vec 0) v1 w2 (--w1) = pi `, REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN MRESA_TAC(GEN_ALL AZIM_EQ_PI_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`;`--w1:real^3`]);; let SUM_AZIM_SYM_0=prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2} /\ azim (vec 0) v1 w1 w2<= pi ==> azim (vec 0) v1 w1 w2 + azim (vec 0) v1 w2 (--w1) = pi `, REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN MRESA_TAC(GEN_ALL AZIM_EQ_PI_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`;`--w1:real^3`]);; let AZIM_EQ_LE_SYM_0=prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2} /\ azim (vec 0) v1 w1 w2<= pi ==> azim (vec 0) v1 (--w1) (--w2)=azim (vec 0) v1 w1 w2 `, STRIP_TAC THEN MP_TAC SUM_AZIM_SYM_0 THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) v1 w1 w2/\ azim (vec 0) v1 w1 w2 + azim (vec 0) v1 w2 (--w1) = pi ==> azim (vec 0) v1 w2 (--w1) <= pi`) THEN ASM_SIMP_TAC[azim] THEN RESA_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`v1:real^3`;`w1:real^3`] THEN MRESA_TAC (GEN_ALL SUM_AZIM_SYM_0)[`v1:real^3`;`--w1:real^3`;`w2:real^3`] THEN ASM_TAC THEN REAL_ARITH_TAC);; let AZIM_LE_PI_SYM_0=prove(`~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2} /\ azim (vec 0) v1 w1 w2<= pi ==> azim (vec 0) v1 (--w1) (--w2) <= pi`, REPEAT STRIP_TAC THEN MP_TAC AZIM_EQ_LE_SYM_0 THEN RESA_TAC);; let EQUI_FF_SYM_0=prove(`!(x:real^N#real^N). (SND x, FST x)IN IMAGE (\i. vv (SUC i),vv i) (:num) <=> x IN IMAGE (\i. vv i,vv (SUC i)) (:num)`, REWRITE_TAC[IMAGE;IN_ELIM_THM;PAIR_EQ] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ EXISTS_TAC`x':num` THEN ASM_SIMP_TAC[] THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[PAIR_EQ] THEN ASM_SIMP_TAC[]; POP_ASSUM MP_TAC THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[PAIR_EQ] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`x':num` THEN ASM_SIMP_TAC[]]);; let CARD_EQUI_FF_SYM_0=prove(`FINITE (IMAGE (\i. vv i,vv (SUC i)) (:num)) ==> CARD (IMAGE (\i. (vv:num->real^N) (SUC i),vv i) (:num))= CARD (IMAGE (\i. vv i,vv (SUC i)) (:num))`, STRIP_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN EXISTS_TAC`(\(x:real^N#real^N). (SND x, FST x))` THEN ASM_REWRITE_TAC[EQUI_FF_SYM_0;EXISTS_UNIQUE] THEN REPEAT STRIP_TAC THEN EXISTS_TAC`SND (y:real^N#real^N),FST (y:real^N#real^N)` THEN MRESA_TAC( GEN_ALL EQUI_FF_SYM_0)[`vv:num->real^N`;`SND (y:real^N#real^N),FST (y:real^N#real^N)`] THEN REPEAT RESA_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]));; let FF_OF_HYP_ITER_VV=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> !n. (ITER n (ff_of_hyp (vec 0,V,E)) ) (vv (SUC i),vv i)= vv (SUC(n*(k-1)+i)),vv (n*(k-1)+i)`, STRIP_TAC THEN INDUCT_TAC THENL[ REWRITE_TAC[ITER;I_DEF;ARITH_RULE`0 *B+A=A`]; ASM_REWRITE_TAC[ITER] THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;ff_of_hyp;] THEN REPEAT RESA_TAC THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN SUBGOAL_THEN`vv (SUC (n *(k-1)+ i)),(vv:num->real^3) (n *(k-1)+ i) IN FF UNION IMAGE (\i. vv (SUC i),vv i) (:num)`ASSUME_TAC THENL[ REWRITE_TAC[UNION;IN_ELIM_THM] THEN MATCH_MP_TAC(SET_RULE`A==> B\/A`) THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`n *(k-1)+i:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC (SUC n * (k - 1) + i) =(n*(k-1)+i) +k /\ (n * (k - 1) + i) + k - 1 =SUC n * (k - 1) + i`) THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`(n * (k - 1) + i)`;`k:num`] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;ff_of_hyp;] THEN SIMP_TAC[Polar_fan.IVS_AZIM_CYCLE_TWO_POINT_SET] THEN ASM_TAC THEN REWRITE_TAC[periodic] THEN REPEAT RESA_TAC]]);; let DUAL_EXISTS_MOD0=prove(` ~(k=0) ==> ?n. (n*(k-1)) MOD k= b MOD k `, STRIP_TAC THEN EXISTS_TAC`k- b MOD k` THEN MRESA_TAC DIVISION[`b:num`;`k:num`] THEN MP_TAC(ARITH_RULE`~(k=0)/\ b MOD k b MOD k<=k/\ 1 <= k- b MOD k /\ 0 (k * (k - b MOD k) + b MOD k) - k = k * (k - b MOD k) - k *1+ b MOD k`) THEN RESA_TAC THEN ASM_REWRITE_TAC[GSYM LEFT_SUB_DISTRIB] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN MRESA_TAC MOD_MULT_ADD[`k-b MOD k-1`;`k:num`;`b MOD k`] THEN ASM_SIMP_TAC[MOD_MOD_REFL]);; let DUAL_EXISTS_MOD_LE=prove(` ~(k=0)/\ a MOD k<= b MOD k ==> ?n. (n*(k-1) +a) MOD k= b MOD k `, REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL DUAL_EXISTS_MOD0)[`b MOD k- a MOD k`;`k:num`] THEN EXISTS_TAC`n:num` THEN MRESA_TAC DIVISION[`b:num`;`k:num`] THEN MP_TAC(ARITH_RULE`a MOD k<= b MOD k /\ b MOD k b MOD k - a MOD k< k/\ (b MOD k- a MOD k) + a MOD k= b MOD k `) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`b MOD k- a MOD k`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`n*(k-1)`;`a:num`;`k:num`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[MOD_MOD_REFL]);; let DUAL_EXISTS_MOD_GE=prove(` ~(k=0)/\ b MOD k<= a MOD k ==> ?n. (n*(k-1) +a) MOD k= b MOD k `, REPEAT STRIP_TAC THEN MRESA_TAC(GEN_ALL DUAL_EXISTS_MOD0)[`b MOD k +k- a MOD k`;`k:num`] THEN EXISTS_TAC`n:num` THEN MRESA_TAC DIVISION[`a:num`;`k:num`] THEN MRESA_TAC MOD_LT[`a MOD k`;`k:num`] THEN MP_TAC(ARITH_RULE`a MOD k(b MOD k + k - a MOD k) + a MOD k= 1* k+ b MOD k`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1:num`;`k:num`;`b MOD k`] THEN MRESA_TAC MOD_ADD_MOD[`b MOD k + k - a MOD k`;`a MOD k:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`n*(k-1)`;`a:num`;`k:num`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[MOD_MOD_REFL]);; let DUAL_EXISTS_MOD=prove(` ~(k=0) ==> ?n. (n*(k-1) +a) MOD k= b MOD k `, STRIP_TAC THEN MP_TAC(ARITH_RULE`a MOD k<= b MOD k\/ b MOD k<= a MOD k`) THEN RESA_TAC THEN ASM_SIMP_TAC[DUAL_EXISTS_MOD_GE;DUAL_EXISTS_MOD_LE]);; let FACE_DUAL_SYM_0=prove(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ x IN FF /\ SND x,FST x = v1 /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> IMAGE (\i. vv (SUC i),vv i) (:num) = face (hypermap (HYP (vec 0,V,E))) v1`, STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1bool`;`E:(real^3->bool)->bool`] THEN ASM_TAC THEN REPLICATE_TAC (16-12)(STRIP_TAC) THEN EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION;Wrgcvdr_cizmrrh.POWER_TO_ITER;] THEN REPEAT RESA_TAC THEN EQ_TAC THENL[ REPEAT STRIP_TAC THEN EXPAND_TAC"v1" THEN MRESA_TAC(GEN_ALL FF_OF_HYP_ITER_VV) [`FF:real^3#real^3->bool`;`s:scs_v39`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`k:num`;`x'':num`;] THEN MRESA_TAC (GEN_ALL DUAL_EXISTS_MOD)[`x'':num`;`x'''':num`;`k:num`] THEN EXISTS_TAC`n:num` THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x'''':num`] THEN MRESA_TAC th[`n *(k-1) + x''`] THEN MRESA_TAC th[`SUC x'''':num`] THEN MRESA_TAC th[`SUC(n *(k-1) + x'')`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;ADD1]) THEN MRESA_TAC MOD_LT[`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`(n * (k - 1) + x'')`;`1`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`(x''''):num`;`1`;`k:num`] THEN ARITH_TAC; RESA_TAC THEN EXPAND_TAC"v1" THEN MRESA_TAC(GEN_ALL FF_OF_HYP_ITER_VV) [`FF:real^3#real^3->bool`;`s:scs_v39`;`V:real^3->bool`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`k:num`;`x'':num`;] THEN EXISTS_TAC`n * (k - 1) + x'':num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`]]);; let LOCAL_FAN_DUAL_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> local_fan (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num), IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num))`, [STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1 REPEAT STRIP_TAC THEN MP_TAC th) THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC (SYM th)) THEN REPEAT STRIP_TAC THEN MRESA_TAC face_refl[`hypermap (HYP (vec 0,(V:real^3->bool),(E:(real^3->bool)->bool)))`;`x:real^3#real^3`] THEN ABBREV_TAC`v1=(SND (x:real^3#real^3),FST (x:real^3#real^3))` THEN MP_TAC OPP_FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] THEN POP_ASSUM (fun th-> REWRITE_TAC[th]) THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2] THEN REPEAT RESA_TAC ; EXISTS_TAC`(\(x:real^3,y:real^3). --x,--y) v1` THEN ASM_SIMP_TAC[UNION;IN_ELIM_THM;IN_PAIR_SYM_0; IN_EQ_PAIR_SYM_0] THEN MP_TAC FACE_SYM_0 THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;] ; MATCH_MP_TAC(SET_RULE`A==> A\/B`) THEN EXPAND_TAC"v1" THEN SIMP_TAC[EQUI_FF_SYM_0] THEN ASM_SIMP_TAC[]; MP_TAC FACE_ALL_SYM_0 THEN ASM_REWRITE_TAC[] THEN RESA_TAC THEN ASM_SIMP_TAC[EQ_SET_PAIR_SYM_0;] THEN MP_TAC FACE_DUAL_SYM_0 THEN RESA_TAC ; REPLICATE_TAC (16-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MP_TAC th) THEN REPLICATE_TAC (15-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC (SYM th)) THEN REPEAT STRIP_TAC THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`][DART_OF_HYP_VV] THEN MP_TAC OPP_FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL Lvducxu.FAN_DART_DARTS)[`vec 0:real^3`;`IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`][DART_OF_HYP_VV] THEN ASM_SIMP_TAC[IN_ELIM_THM;PAIR_FUN_SYM_0;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2] THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[dih2k] THEN REPEAT RESA_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN REPEAT STRIP_TAC; MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`] THEN MRESA_TAC (GEN_ALL CARD_EQUI_FF_SYM_0)[`vv:num->real^3`] THEN REPLICATE_TAC (31-12)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[SYM th]); ASM_TAC THEN REWRITE_TAC[LET_DEF;LET_END_DEF;] THEN REPEAT RESA_TAC THEN MP_TAC FACE_ALL_SYM_0 THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y):real^3#real^3. --x,--y) x'`][ID_SYM_0]) THEN MP_TAC IMAGE_NODE_SYM_0 THEN RESA_TAC THEN ASM_SIMP_TAC[GSYM IMAGE_UNION] THEN MRESA_TAC (GEN_ALL IN_EQ_PAIR_SYM_0)[`x':real^3#real^3`;`IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num) UNION IMAGE (\i. --vv (k - SUC (SUC i MOD k)),--(vv:num->real^3) (k - SUC (i MOD k))) (:num)`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;ID_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B= B UNION A`] THEN STRIP_TAC THEN REPLICATE_TAC (28-13)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`((\(x,y):real^3#real^3. --x,--y) x')`] ) THEN SET_TAC[] ; REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC ff_POWER_COMMUTATIVE_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (ff_of_hyp (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))) (x) = (\(x,y). --x,--y) (ITER n (ff_of_hyp (vec 0,V,E)) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; SUBGOAL_THEN`CARD (IMAGE (\(x,y). --x,--y) (IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num))) = CARD (FF:real^3#real^3->bool)`ASSUME_TAC ; MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`A UNION B=B UNION A`] THEN MRESA_TAC (GEN_ALL CARD_EQUI_FF_SYM_0)[`vv:num->real^3`] ; MP_TAC FAN_SYM_0 THEN RESA_TAC THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (\i. --(vv:num->real^3) i) (:num)`;`IMAGE (\i. {--(vv:num->real^3) i, --vv (SUC i)}) (:num)`][orbit_map;IN_ELIM_THM;] THEN MRESAL_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`][] THEN MRESA_TAC Hypermap.node_map_and_darts[`hypermap (HYP (vec 0, IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_F_EQ2_NEG;dih2k;PAIR_FUN_SYM_0;GSYM IMAGE_UNION;OPP_IMAGE_E_EQ;OPP_IMAGE_V_EQ;OPP_IMAGE_F_EQ;OPP_IMAGE_F_EQ2;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL FINITE_IMAGE)[`(\(x,y):real^3#real^3. --x,--y)`;`IMAGE (\(x,y):real^3#real^3. --x,--y)(IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF)`][ID_PAIR_SYM_0] THEN MP_TAC(SET_RULE`FF SUBSET IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num) UNION FF`) THEN RESA_TAC THEN MRESA_TAC(FINITE_SUBSET)[`FF:real^3#real^3->bool`;`IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num) UNION FF`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (40-14)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (43-39)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC EDGE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (edge_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (edge_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-15)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN MP_TAC NODE_POWER_MAP_SYM_0 THEN REWRITE_TAC[Wrgcvdr_cizmrrh.POWER_TO_ITER] THEN RESA_TAC THEN SUBGOAL_THEN `!n x. ITER n (node_map (hypermap (HYP (vec 0, IMAGE (\i. --vv i) (:num), IMAGE (\i. {--vv i, --vv (SUC i)}) (:num))))) (x) = (\(x,y). --x,--y) (ITER n (node_map (hypermap (HYP (vec 0,V,E)))) ((\(x,y). --x,--y) x))` ASSUME_TAC; REPEAT GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`n:num`;`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]) ; ASM_SIMP_TAC[CARD_PAIR_SYM_0;COMMUTATIVE_POINT_PAIR_0] THEN REPLICATE_TAC (26-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN REWRITE_TAC[Wrgcvdr_cizmrrh.has_orders;FUN_EQ_THM;I_DEF] THEN REPEAT RESA_TAC; REPLICATE_TAC (30-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC(ISPEC `i:num` th)) THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`(\(x,y). --x,--y) x':real^3#real^3`][ID_SYM_0]); ]);; let AZIM_NEG_FIRST_PI=prove_by_refinement( `~collinear {vec 0, v1, w1} /\ ~collinear {vec 0, v1, w2} /\ &0 azim (vec 0) (--v1) w1 w2 = &2 *pi- azim (vec 0) v1 w1 w2`, [STRIP_TAC THEN MATCH_MP_TAC AZIM_UNIQUE THEN MRESA_TAC Fan.properties_coordinate[`vec 0:real^3`;`v1:real^3`;`w1:real^3`] THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`] THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`] THEN POP_ASSUM (fun th-> MRESA_TAC th[`e1_fan (vec 0:real^3) v1 w1`;`e2_fan (vec 0:real^3) v1 w1`;`e3_fan (vec 0:real^3) v1 w1`]) THEN EXISTS_TAC`--h1:real` THEN EXISTS_TAC`--h2:real` THEN EXISTS_TAC`r1:real` THEN EXISTS_TAC`r2:real` THEN EXISTS_TAC`e1_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`--e2_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`-- e3_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`&2 * pi- psi` THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`;REAL_ARITH`A-B< A<=> &0 a<=b`) THEN ASM_REWRITE_TAC[]; STRIP_TAC; ASM_TAC THEN REWRITE_TAC[orthonormal] THEN REPEAT DISCH_TAC THEN ASM_REWRITE_TAC[DOT_RNEG;DOT_LNEG;REAL_ARITH`-- -- A=A/\ -- &0= &0`;CROSS_RNEG] THEN ONCE_REWRITE_TAC[DOT_SYM] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[DOT_SYM]; ASM_REWRITE_TAC[VECTOR_ARITH`(-- A= vec 0:real^3<=> A= vec 0)/\ A- vec 0=A`;dist;NORM_NEG] THEN STRIP_TAC; ASM_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`(-- A= vec 0:real^3<=> A= vec 0)/\ A- vec 0=A`;dist;NORM_NEG] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[VECTOR_ARITH`a % --b= -- c <=> a % b=c:real^3`]; REWRITE_TAC[SIN_SUB;COS_SUB] THEN MRESAL_TAC SIN_PERIODIC[`&0`][REAL_ARITH`&0+A=A`] THEN MRESAL_TAC COS_PERIODIC[`&0`][REAL_ARITH`&0+A=A `;SIN_0;COS_0] THEN STRIP_TAC; VECTOR_ARITH_TAC; REWRITE_TAC[REAL_ARITH`A-B+A-C=(A+A)-(B+C)`;SIN_SUB;COS_SUB] THEN MRESAL_TAC SIN_PERIODIC[`&2 *pi`][REAL_ARITH`&0+A=A`] THEN MRESAL_TAC COS_PERIODIC[`&2 *pi`][REAL_ARITH`&0+A=A `;SIN_0;COS_0] THEN VECTOR_ARITH_TAC]);; let AZIM_COMPL_NEG=prove(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2} ==> azim (vec 0) (--v1) w1 w2 = azim (vec 0) v1 w2 w1`, REPEAT STRIP_TAC THEN MRESA_TAC AZIM_COMPL[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`] THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`] THEN MP_TAC(REAL_ARITH`&0 <= azim (vec 0) v1 w1 w2 ==> azim (vec 0) v1 w1 w2 = &0 \/ (&0 < azim (vec 0) v1 w1 (w2:real^3)/\ ~(azim (vec 0) v1 w1 w2 = &0))`) THEN RESA_TAC THENL[ POP_ASSUM MP_TAC THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`w1:real^3`;`v1:real^3`] THEN MRESA_TAC(GEN_ALL COLLINEAR_POINT_SYM_0)[`w2:real^3`;`v1:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN RESA_TAC THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`] THEN MRESA_TAC th3[`vec 0:real^3`;`-- v1:real^3`;`w2:real^3`]THEN ASM_SIMP_TAC[AZIM_EQ_0;AFF_GT_2_1;IN_ELIM_THM] THEN RESA_TAC THEN EXISTS_TAC`t1+ &2 * t2` THEN EXISTS_TAC`-- t2:real` THEN EXISTS_TAC`t3:real` THEN ASM_REWRITE_TAC[REAL_ARITH`(t1 + &2 * t2) + --t2 + t3= t1+t2+t3`] THEN VECTOR_ARITH_TAC; ASM_SIMP_TAC[AZIM_NEG_FIRST_PI]]);; let REMOVE_NEG_AZIM1_SYM_0=prove_by_refinement(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2} ==> azim (vec 0) v1 (--w1) (--w2) = azim (vec 0) v1 w1 w2`, [STRIP_TAC THEN MATCH_MP_TAC AZIM_UNIQUE THEN MRESA_TAC Fan.properties_coordinate[`vec 0:real^3`;`v1:real^3`;`w1:real^3`] THEN MRESA_TAC th3[`vec 0:real^3`;`v1:real^3`;`w2:real^3`] THEN MRESA_TAC azim[`vec 0:real^3`;`v1:real^3`;`w1:real^3`;`w2:real^3`] THEN POP_ASSUM (fun th-> MRESAL_TAC th[`e1_fan (vec 0:real^3) v1 w1`;`e2_fan (vec 0:real^3) v1 w1`;`e3_fan (vec 0:real^3) v1 w1`][VECTOR_ARITH`A- vec 0=A`]) THEN EXISTS_TAC`--h1:real` THEN EXISTS_TAC`--h2:real` THEN EXISTS_TAC`r1:real` THEN EXISTS_TAC`r2:real` THEN EXISTS_TAC`--e1_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`--e2_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`e3_fan (vec 0:real^3) v1 w1` THEN EXISTS_TAC`psi:real` THEN ASM_REWRITE_TAC[REAL_ARITH`&0<= A-B<=> B<=A`;REAL_ARITH`A-B< A<=> &0 w1 = (r1 * cos psi) % e1_fan (vec 0) v1 w1 + (r1 * sin psi) % e2_fan (vec 0) v1 w1 + h1 % v1:real^3`] THEN ASM_REWRITE_TAC[VECTOR_ARITH`--w2 = (r2 * cos (psi + azim (vec 0) v1 w1 w2)) % --e1_fan (vec 0) v1 w1 + (r2 * sin (psi + azim (vec 0) v1 w1 w2)) % --e2_fan (vec 0) v1 w1 + --h2 % v1<=> w2 = (r2 * cos (psi + azim (vec 0) v1 w1 w2)) % e1_fan (vec 0) v1 w1 + (r2 * sin (psi + azim (vec 0) v1 w1 w2)) % e2_fan (vec 0) v1 w1 + h2 % v1`] THEN RESA_TAC; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]]);; let AZIM_NEG=prove(`~collinear {vec 0, v1, w1:real^3} /\ ~collinear {vec 0, v1, w2} ==> azim (vec 0) (--v1) (--w1) (--w2) = azim (vec 0) v1 w2 w1`, STRIP_TAC THEN MRESA_TAC (GEN_ALL COLLINEAR_POINT_SYM_0)[`w1:real^3`;`v1:real^3`] THEN MRESA_TAC (GEN_ALL COLLINEAR_POINT_SYM_0)[`w2:real^3`;`v1:real^3`] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN RESA_TAC THEN MRESA_TAC (GEN_ALL REMOVE_NEG_AZIM1_SYM_0)[`-- v1:real^3`;`w1:real^3`;` w2:real^3`] THEN ASM_SIMP_TAC[AZIM_COMPL_NEG]);; let FST_SND_NEG_PAIR_SYM_0=prove(`--SND ((\(x,y):real^N#real^N. --x,--y) x)= SND x/\ --FST ((\(x,y):real^N#real^N. --x,--y) x)= FST x`, MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REWRITE_TAC[VECTOR_ARITH`-- -- A=A:real^N`]);; let CONVEX_LOCAL_FAN_SYM_0=prove_by_refinement(` scs_k_v39 s=k /\ IMAGE vv (:num) = V /\ IMAGE (\i. {vv i, vv (SUC i)}) (:num) = E /\ IMAGE (\i. vv i,vv (SUC i)) (:num) = FF /\ is_scs_v39 s /\ ~(k <= 3)/\ BBs_v39 s vv ==> convex_local_fan (IMAGE (\i. --vv (k - SUC (i MOD k))) (:num), IMAGE (\i. {--vv (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num), IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num))`, [REWRITE_TAC[convex_local_fan] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)/\ 1real^3) (SUC i),vv (i)) (:num))`][ID_PAIR_SYM_0] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA) [`IMAGE (\x:real^3. --x) V`;`IMAGE (\(x,y):real^3#real^3. --x,--y) (IMAGE (\i. vv (SUC i),vv i) (:num))`;`IMAGE (\i. {-- (vv:num->real^3) i, --vv (SUC i)}) (:num)`] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:real^3#real^3`]) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM PAIR_FUN_SYM_0] THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[EE_SYM_0] THEN RESA_TAC THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV] THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`;] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x' +k-1`] THEN MRESA_TAC th[`x':num`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x' + k - 1= 1 *k + x'/\ ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x':num`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;] THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))) IN FF` ASSUME_TAC; EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`SUC x':num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; REPLICATE_TAC (19-10)(POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA) [`V:real^3->bool`;` (IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num))`;`IMAGE (\i. { (vv:num->real^3) i, vv (SUC i)}) (:num)`] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`]) THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num `] THEN MRESA_TAC th[`1*k+ x' `]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;CROSS_RNEG;CROSS_LNEG;] THEN REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CROSS_SKEW;] THEN REWRITE_TAC[CROSS_TRIPLE;DOT_LNEG] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE;DOT_LNEG] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[wedge_in_fan_ge2] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM PAIR_FUN_SYM_0] THEN GEN_REWRITE_TAC(LAND_CONV o DEPTH_CONV)[IMAGE;IN_ELIM_THM] THEN REWRITE_TAC[EE_SYM_0] THEN RESA_TAC THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV] THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x'`;`k:num`;] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;convex_local_fan;] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x' +k-1`] THEN MRESA_TAC th[`x':num`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x' + k - 1= 1 *k + x'/\ ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x':num`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0;GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;Polar_fan.SIN_AZIM_MUTUAL_CROSS;DOT_RNEG;] THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x')) IN V` ASSUME_TAC; EXPAND_TAC"V" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`SUC x':num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x':num `] THEN MRESA_TAC th[`1 *k +x'`]) THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`FF:real^3#real^3->bool`;`V:real^3->bool`;`(vv:num->real^3) (SUC x')`;`E:(real^3->bool)->bool`;] THEN MP_TAC Wrgcvdr_cizmrrh.LOCAL_FAN_IMP_FAN THEN RESA_TAC THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_FINITE_EE)[`vec 0:real^3`;`V:real^3->bool`;`(vv:num->real^3) (SUC x')`;`E:(real^3->bool)->bool`;] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[ELEMENT2_SYM_0;CARD_SYM_0;ARITH_RULE`2>1`] THEN SUBGOAL_THEN `((vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))) IN FF` ASSUME_TAC; EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`SUC x':num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; REPLICATE_TAC (25-10)(POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC(SUC x'))`]) THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;wedge_in_fan_ge2;ARITH_RULE`2>1`;wedge_ge;azim;SUBSET;IN_ELIM_THM;IMAGE] THEN REPEAT RESA_TAC THEN MP_TAC(SET_RULE`collinear {(vec 0),(--(vv:num->real^3) (SUC x')),-- x''' }\/ ~(collinear {(vec 0),(--(vv:num->real^3) (SUC x')),-- x''' })`) THEN RESA_TAC; ASM_SIMP_TAC[AZIM_DEGENERATE;azim]; MRESAL_TAC (GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (SUC x'), --x'''}`][ELEMENT2_SYM_0;REFL_SYM_0] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[GSYM ELEMENT2_SYM_0;SET_RULE`{A} UNION {B,C}={A,B,C}`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`collinear {(vec 0),(--(vv:num->real^3) (SUC x')),(--vv (1 * k + x')) }\/ ~(collinear {(vec 0),(--(vv:num->real^3) (SUC x')),(--vv (1 * k + x')) })`) THEN RESA_TAC; ASM_SIMP_TAC[AZIM_DEGENERATE;azim;] THEN REAL_ARITH_TAC; MRESAL_TAC (GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (SUC x'), (--vv (1 * k + x'))}`][ELEMENT2_SYM_0;REFL_SYM_0] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[GSYM ELEMENT2_SYM_0;SET_RULE`{A} UNION {B,C}={A,B,C}`] THEN STRIP_TAC THEN REPLICATE_TAC (32-26)(POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`x''':real^3`]) THEN ASM_SIMP_TAC[AZIM_NEG] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (SUC x'), (vv:num->real^3) (SUC (SUC x'))`] THEN ASM_SIMP_TAC[AZIM_NEG] THEN MRESA_TAC Fan.sum4_azim_fan[`vec 0:real^3`;`(vv:num->real^3) (SUC x')`;`(vv:num->real^3) (SUC(SUC x'))`;`x''':real^3`;`(vv:num->real^3) (x')`] THEN REWRITE_TAC[REAL_ARITH`a<=b+a<=> &0<=b`;azim]]);; let PEROPP_IN_BB_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3) ==> BBs_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`, [REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;scs_opp_v39;PAIR_EQ;LET_DEF;LET_END_DEF;BBs_v39;scs_v39_explicit;peropp2;peropp;is_scs_v39] THEN STRIP_TAC THEN ASM_TAC THEN REPEAT RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)/\ 1real^3`] THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[SYM th] THEN REPEAT STRIP_TAC) THEN REPLICATE_TAC (29-21)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT DISCH_TAC THEN MP_TAC th) THEN MATCH_MP_TAC(SET_RULE`a IN A ==> (A SUBSET B==> a IN B)`) THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`x':num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num) IN (:num)`]; ASM_TAC THEN REWRITE_TAC[periodic;peropp;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`]; ASM_SIMP_TAC[DIST_SYM_0]; ASM_SIMP_TAC[DIST_SYM_0]; MRESA_TAC (GEN_ALL CONVEX_LOCAL_FAN_SYM_0)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (\i. (vv:num->real^3) i,vv (SUC i)) (:num)`;`s:scs_v39`;`(vv:num->real^3)`;`k:num`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[scs_arrow_v39;IN_SING;scs_opp_v39;PAIR_EQ;LET_DEF;LET_END_DEF;BBs_v39;scs_v39_explicit;peropp2;peropp;is_scs_v39]]);; let NO_IS_EAR=prove(`~(scs_k_v39 s<=3)==> ~(is_ear_v39 s)`, REWRITE_TAC[is_ear_v39] THEN ARITH_TAC);; let NO_IS_EAR_SCS_OPP=prove(`~(scs_k_v39 s<=3)==> ~(is_ear_v39 (scs_opp_v39 s))`, REWRITE_TAC[is_ear_v39;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit] THEN ARITH_TAC);; let DSV_EQ_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3) ==> dsv_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = dsv_v39 s vv`, [STRIP_TAC THEN ASM_SIMP_TAC[dsv_v39;NO_IS_EAR_SCS_OPP;NO_IS_EAR;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit;peropp2;DIST_SYM_0;peropp] THEN MATCH_MP_TAC(REAL_ARITH`a=b==> c+ #0.1 * -- &1 *a= c+ #0.1 * -- &1 *b`) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN EXISTS_TAC`(\j. k - SUC(SUC(j MOD k) MOD k))` THEN REWRITE_TAC[IN_ELIM_THM] THEN REPEAT RESA_TAC; REWRITE_TAC[EXISTS_UNIQUE] THEN MP_TAC(ARITH_RULE`~(k<=3)==> k-1 y=k-1\/ SUC y REPEAT DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[is_scs_v39;periodic2] THEN REPEAT RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`scs_J_v39 s (k-1)`][ARITH_RULE`~(3=0)`;periodic] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`]) THEN REMOVE_ASSUM_TAC THEN MRESA_TAC DIVISION[`SUC(y' MOD k)`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC (y' MOD k) MOD k < k /\ 1 SUC (y' MOD k) MOD k = 0`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> 1+k-1=k`) THEN RESA_TAC THEN MRESAL_TAC Hdplygy.MOD_EQ_MOD[`y' MOD k`;`k-1`;`1`;`k:num`][GSYM ADD1;ARITH_RULE`1+A=A+1`] THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`]; EXISTS_TAC`k- SUC(SUC y)` THEN MP_TAC(ARITH_RULE`SUC y k - SUC (SUC y) < k/\ SUC (k - SUC (SUC y))= k - SUC y/\ k - SUC y y'=k-1\/ SUC y' ~(k-1=y)`) THEN RESA_TAC; MRESA_TAC MOD_LT[`SUC y':num`;`k:num`] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`SUC y' y' = k - SUC (SUC y)`) THEN RESA_TAC; MP_TAC(ARITH_RULE`~(k<=3)==> k-1 k-1 k-1 REPEAT DISCH_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN MP_TAC(ARITH_RULE`xx=k-1\/ SUC x MRESA_TAC th[`k:num`]); MRESA_TAC MOD_LT[`SUC x`;`k:num`]; MP_TAC(ARITH_RULE`~(k<=3)==> k-1 k-1x=k-1\/ SUC xreal^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`]) THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM] THEN REWRITE_TAC[]; MRESA_TAC MOD_LT[`SUC x`;`k:num`] THEN GEN_REWRITE_TAC(LAND_CONV o ONCE_DEPTH_CONV)[DIST_SYM] THEN REWRITE_TAC[]]);; let SUM_PAIR_SYM_0=prove(`sum (IMAGE (\(x,y):real^N#real^N. --x,--y) s) f= sum s (f o ((\(x,y). --x,--y)))`, MATCH_MP_TAC SUM_IMAGE THEN REPEAT GEN_TAC THEN MP_TAC(SET_RULE`x=(FST (x:real^N#real^N),SND (x:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN MP_TAC(SET_RULE`y=(FST (y:real^N#real^N),SND (y:real^N#real^N))`) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN ASM_SIMP_TAC[VECTOR_ARITH`(--a= --b)<=> (a=b:real^N)`;PAIR_EQ] THEN ASM_REWRITE_TAC[GSYM PAIR_EQ] THEN RESA_TAC);; let TAUSTAR_EQ_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBs_v39 s vv /\ ~(k<=3) ==> taustar_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = taustar_v39 s vv`, [STRIP_TAC THEN MP_TAC DSV_EQ_SYM_0 THEN RESA_TAC THEN ASM_REWRITE_TAC[taustar_v39;LET_DEF;LET_END_DEF;scs_opp_v39;scs_v39_explicit] THEN MATCH_MP_TAC (REAL_ARITH`C=A==>A-B=C-B`) THEN MP_TAC(ARITH_RULE`~(k<=3)==> 3<=k/\ 1real^3) (SUC i)) (:num)`;`IMAGE (vv:num->real^3) (:num)`;` IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;] THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.LOCAL_FAN_FINITE_FF)[`IMAGE (vv:num->real^3) (:num)`;` IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;` IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`] THEN MRESA_TAC (GEN_ALL Wrgcvdr_cizmrrh.LOCAL_IMP_FINITE_DARTS) [` IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;` IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`IMAGE (vv:num->real^3) (:num)`] THEN MRESA_TAC(GEN_ALL DART_OF_HYP_VV)[`vv:num->real^3`] THEN ASSUME_TAC(SET_RULE`IMAGE (\i. vv (SUC i),vv i) (:num) SUBSET IMAGE (\i. vv i,vv (SUC i)) (:num) UNION IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num)`) THEN MRESA_TAC(FINITE_SUBSET)[`IMAGE (\i. (vv:num->real^3) (SUC i),vv i) (:num)`;`darts_of_hyp (IMAGE (\i. {vv i, (vv:num->real^3) (SUC i)}) (:num)) (IMAGE vv (:num))`] THEN ASM_SIMP_TAC[CARD_PAIR_SYM_0;CARD_EQUI_FF_SYM_0] THEN MATCH_MP_TAC (REAL_ARITH`A=C==>A-B=C-B`) THEN ASM_SIMP_TAC[SUM_PAIR_SYM_0;o_DEF;FST_SND_PAIR_SYM_0] THEN MRESA_TAC(GEN_ALL Qknvmlb.SUM_AZIM_EQ_ANGLE_LE4)[`IMAGE (vv:num->real^3) (:num)`;`vv:num->real^3`;`1:num`;`s:scs_v39`;`(vv:num->real^3) (1 MOD scs_k_v39 s)`;` IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;` IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN RESA_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MATCH_MP_TAC SUM_EQ_GENERAL THEN ASM_REWRITE_TAC[IN_ELIM_THM;] THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(k-1)=k/\ SUC(SUC(k-1))=k+1/\ SUC 0=1/\ ~(k=0)/\ 1 * k + 0=k/\ 1 * k + 1=k+1/\1real^3) (SUC i),vv i)` THEN RESA_TAC; REWRITE_TAC[IN_ELIM_THM;IMAGE;EXISTS_UNIQUE] THEN REPEAT RESA_TAC THEN EXISTS_TAC`x MOD k` THEN ASM_REWRITE_TAC[] THEN MRESA_TAC DIVISION[`x:num`;`k:num`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`] THEN MRESA_TAC th[`SUC x:num`] THEN MRESA_TAC th[`SUC(x MOD k):num`]) THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[MOD_SUC_MOD;PAIR_EQ] THEN REPEAT RESA_TAC THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_INJ)[`s:scs_v39`;`k:num`;`vv:num->real^3`] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`y':num`;`x MOD k`]); REPEAT RESA_TAC; REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; REWRITE_TAC[ADD1;NORM_NEG;REAL_EQ_MUL_LCANCEL] THEN MATCH_MP_TAC(SET_RULE`A==> C\/A`) THEN REWRITE_TAC[GSYM ADD1] THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)` THEN ABBREV_TAC`E = IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)` THEN ABBREV_TAC`FF = IMAGE (\i. ((vv:num->real^3) i, vv (SUC i))) (:num)` THEN MP_TAC LOCAL_FAN_DUAL_SYM_0 THEN ASM_TAC THEN REWRITE_TAC[BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[OPP_IMAGE_F_EQ_NEG;OPP_IMAGE_E_EQ_NEG;OPP_IMAGE_V_EQ_NEG;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2] THEN ASM_SIMP_TAC[PAIR_FUN_SYM_0;IMAGE_E_SYM_0;IMAGE_V_SYM_0;OPP_IMAGE_E_EQ;OPP_IMAGE_F_EQ2] THEN STRIP_TAC THEN SUBGOAL_THEN`(--vv (SUC x),--vv x) IN IMAGE (\(x,y). --x,--y) (IMAGE (\i. vv (SUC i),(vv:num->real^3) i) (:num))`ASSUME_TAC; REWRITE_TAC[GSYM PAIR_FUN_SYM_0] THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA) [`IMAGE (\x:real^3. --x) (IMAGE vv (:num))`;`IMAGE (\(x,y):real^3#real^3. --x,--y) (IMAGE (\i. vv (SUC i),vv i) (:num))`;`IMAGE (\i. {-- (vv:num->real^3) i, --vv (SUC i)}) (:num)`] THEN POP_ASSUM(fun th-> MRESA_TAC th[`(--vv (SUC x),--(vv:num->real^3) x)`]) THEN ASM_SIMP_TAC[EE_SYM_0;EE_EXPAND_BB_VV] THEN MRESAL_TAC (GEN_ALL EE_EXPAND_BB_VV)[`V:real^3->bool`;`FF:real^3#real^3->bool`;`s:scs_v39`;`E:(real^3->bool)->bool`;`vv:num->real^3`;`SUC x`;`k:num`;] [BBs_v39;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x +k-1`] THEN MRESA_TAC th[`x:num`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MP_TAC(ARITH_RULE`~(k<=3) ==> SUC x + k - 1= 1 *k + x/\ ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`x:num`] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_SIMP_TAC[Local_lemmas.AZIM_CYCLE_TWO_POINT_SET;GSYM ELEMENT2_SYM_0] THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`(vv:num->real^3) (1 MOD k)`;`vv:num->real^3`;`1 MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;GSYM ADD1] THEN SUBGOAL_THEN`(vv:num->real^3) (SUC x) IN V`ASSUME_TAC; EXPAND_TAC"V" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`SUC x:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; MP_TAC Nkezbfc_local.CONVEX_LOFA_IMP_INANGLE_EQ_AZIM_IVS THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x)`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`SUC x `]) THEN MRESAL_TAC(GEN_ALL CARD_V_EQ_SCS_K1)[`s:scs_v39`;`vv:num->real^3`;`IMAGE (vv:num->real^3) (:num)`;`k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39] THEN MP_TAC Local_lemmas.ITER_CARD_MINUS1_EQ_IVS_RN1 THEN RESA_TAC THEN POP_ASSUM(fun th-> MRESA_TAC th[`(vv:num->real^3) (SUC x)`]) THEN MRESAL_TAC (GEN_ALL Qknvmlb.VV_SUC_EQ_RHO_NODE_PRIME)[`IMAGE (vv:num->real^3) (:num)`;`IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)`;`k:num`;`s:scs_v39`;`IMAGE (\i. vv i,(vv:num->real^3) (SUC i)) (:num)`;`(vv:num->real^3) (SUC x MOD k)`;`vv:num->real^3`;`SUC x MOD k:num`][MMs_v39;LET_DEF;LET_END_DEF;BBprime2_v39;BBs_v39;GSYM ADD1] THEN POP_ASSUM (fun th-> MRESAL_TAC th[`SUC 0`][ITER] THEN MRESAL_TAC th[`k - 1`][ITER;ARITH_RULE`1+A=SUC A`]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`x:num`] THEN MRESA_TAC th[`SUC (SUC x )`] THEN MRESA_TAC th[`SUC (SUC x MOD k) `] THEN MRESA_TAC th[`k-1+ (SUC x MOD k) `]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[MOD_SUC_MOD] THEN MP_TAC(ARITH_RULE`3 k-1real^3) (SUC x),vv (SUC (SUC x)) IN FF`ASSUME_TAC; EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`SUC x:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (SUC x), (vv:num->real^3) (SUC (SUC x))`] THEN SUBGOAL_THEN`(vv:num->real^3) ( x),vv ( (SUC x)) IN FF`ASSUME_TAC; EXPAND_TAC"FF" THEN REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`x:num` THEN ASM_REWRITE_TAC[SET_RULE`(a:num)IN(:num)`]; ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR)[`V:real^3->bool`;`E:(real^3->bool)->bool`;`FF:real^3#real^3->bool`;`(vv:num->real^3) (x), (vv:num->real^3) ( (SUC x))`]]);; let OPP_IS_SCS=prove_by_refinement( `is_scs_v39 s/\ s' = scs_opp_v39 s==> is_scs_v39 (scs_opp_v39 s)`, [ ABBREV_TAC`k=scs_k_v39 s` THEN ASM_TAC THEN REWRITE_TAC[scs_v39_explicit;scs_opp_v39;LET_DEF;LET_END_DEF;is_scs_v39;peropp] THEN RESA_TAC THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3<=k==> ~(k=0)`) THEN RESA_TAC THEN REPEAT RESA_TAC; ASM_TAC THEN REWRITE_TAC[periodic;peropp;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESA_TAC MOD_LT[`i:num`;`k:num`] THEN MRESA_TAC MOD_LT[`j:num`;`k:num`] THEN MRESA_TAC SUC_INJ[`i:num`;`j:num`] THEN MP_TAC(ARITH_RULE`i < k/\ j k- SUC i i MOD 3=0\/ i MOD 3=1\/ i MOD 3=2`) THEN RESA_TAC; MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`0:num`;`3`][ARITH_3_TAC] THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`1:num`[ARITH_3_TAC]) ; MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`1:num`;`3`][ARITH_3_TAC] THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`0:num`[ARITH_3_TAC]) ; MRESAL_TAC (GEN_ALL Zithlqn.IMP_SUC_MOD_EQ)[`i:num`;`2:num`;`3`][ARITH_3_TAC] THEN REPLICATE_TAC (29-16)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`2:num`[ARITH_3_TAC]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (29-22)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN ASSUME_TAC th THEN REPEAT STRIP_TAC) THEN POP_ASSUM MP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s 2`][ARITH_3_TAC;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`3:num`[ARITH_3_TAC]) ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT RESA_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k i MOD k= k-1 \/ i MOD k k- SUC(k-1)=0/\ 1 ASM_REWRITE_TAC[SYM th]) THEN ASM_TAC THEN REWRITE_TAC[periodic2] THEN REPEAT RESA_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_b_v39 s (k-1)`][ARITH_3_TAC;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN REPLICATE_TAC (37-17)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`k-1:num`[ARITH_3_TAC]) ; MP_TAC(ARITH_RULE`3 k- SUC(k-1)=0/\ 1 ASM_REWRITE_TAC[SYM th]) THEN REPLICATE_TAC (38-17)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`(k - ((i MOD k + 1) + 1)):num`[ARITH_3_TAC]) ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] THEN STRIP_TAC THEN MRESA_TAC DIVISION[`i:num`;`k:num`] THEN MRESA_TAC DIVISION[`j:num`;`k:num`] THEN MP_TAC(ARITH_RULE`3<=k/\ i MOD k SUC (k - SUC (i MOD k)) = (k - (i MOD k))/\ k- SUC(i MOD k) REPEAT STRIP_TAC THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC]) ; POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`i MOD k< k==> i MOD k=0 \/ k-i MOD k j MOD k= k-1 /\ k-1 i MOD k = SUC (j MOD k)/\ (j MOD k) +1 SUC(k- SUC(j MOD k))= k -j MOD k`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`j MOD k< k==> j MOD k=0 \/ k-j MOD k i MOD k= k-1 /\ k-1 j MOD k = SUC (i MOD k)/\ (i MOD k) +1 REPEAT STRIP_TAC THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC]) ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT DISCH_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] THEN STRIP_TAC THEN REPLICATE_TAC (25-19)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL_TAC th[`k - SUC (i MOD k):num`;`(k - SUC (j MOD k))`][ARITH_3_TAC]) ; ASM_TAC THEN REWRITE_TAC[periodic;peropp;periodic2;peropp2;] THEN REPEAT DISCH_TAC THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`i:num`][ARITH_RULE`1*k+i=i+k`] THEN MRESAL_TAC MOD_MULT_ADD[`1:num`;`k:num`;`j:num`][ARITH_RULE`1*k+i=i+k`] THEN SUBGOAL_THEN` CARD {i | i < k /\ (&2 * h0 < scs_b_v39 s i (SUC i) \/ &2 < scs_a_v39 s i (SUC i))} =CARD {i | i < k /\ (&2 * h0 < scs_b_v39 s (k - SUC (i MOD k)) (k - SUC (SUC i MOD k)) \/ &2 < scs_a_v39 s (k - SUC (i MOD k)) (k - SUC (SUC i MOD k)))} ` ASSUME_TAC ; MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`(\x. k - SUC (SUC x MOD k))` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0..k` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_NUMSEG;IN_ELIM_THM] THEN ARITH_TAC; STRIP_TAC; GEN_TAC THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_LT[`x:num`;`k:num`] THEN MRESA_TAC DIVISION[`SUC x`;`k:num`] THEN MP_TAC(ARITH_RULE`3<=k /\ SUC x MOD k < k ==> k - SUC(SUC x MOD k ) MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN MP_TAC(ARITH_RULE`x SUC x=k \/ SUC x y=k-1\/ y< k-1`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k==> k-1 MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`y' SUC y' k-y-2 SUC y' y'= k-y-2`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`] ; MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y' y'= k-y-2`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`] ; POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`y y=k-1\/ y< k-1`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k==> k-1 MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN REPEAT STRIP_TAC THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`y' SUC y' k-y-2 SUC y' y'= k-y-2`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`] ; MRESAL_TAC MOD_LT[`SUC y':num`;`k:num`][ARITH_RULE`~(SUC a=0)`] THEN STRIP_TAC THEN MP_TAC(ARITH_RULE`k - y - 2 < k/\ k - SUC (SUC y') = y/\ SUC y' y'= k-y-2`) THEN RESA_TAC; MP_TAC(ARITH_RULE`3<=k/\ y< k-1 ==>SUC(k-1)=k/\ ~(k-1=y)`) THEN RESA_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`] ; POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]) ; ]);; let DUAL_PEROPP=prove(`~(k=0) /\ periodic a k==> peropp (peropp a k) k=a`, STRIP_TAC THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp;OPP_SUC_MOD;PERIODIC_PROPERTY]);; let DUAL_PEROPP2=prove(`~(k=0) /\ periodic2 a k==> peropp2 (peropp2 a k) k=a`, REWRITE_TAC[periodic2] THEN STRIP_TAC THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp2;OPP_SUC_MOD;PERIODIC_PROPERTY;periodic]);; let SCS_OPP_REFL=prove(`is_scs_v39 s ==> (scs_opp_v39 ((scs_opp_v39 s)))=s`, SIMP_TAC[scs_opp_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;is_scs_v39;BBprime_v39;is_scs_v39;DUAL_PEROPP2;DUAL_PEROPP] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`3<= scs_k_v39 s==> ~(scs_k_v39 s=0)`) THEN RESA_TAC THEN ASM_SIMP_TAC[scs_opp_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;is_scs_v39;BBprime_v39;is_scs_v39;DUAL_PEROPP2;DUAL_PEROPP] THEN POP_ASSUM(fun th-> REWRITE_TAC[th;scs_v39_explicit;scs_k_v39; scs_d_v39;scs_a_v39 ; scs_am_v39 ; scs_bm_v39 ; scs_b_v39 ; scs_J_v39 ; scs_lo_v39 ; scs_hi_v39 ; scs_str_v39; scs_v39;Misc_defs_and_lemmas.part6;Misc_defs_and_lemmas.drop3;FST; Misc_defs_and_lemmas.part1;Misc_defs_and_lemmas.drop1; Misc_defs_and_lemmas.part2;Misc_defs_and_lemmas.drop2; Misc_defs_and_lemmas.part3;Misc_defs_and_lemmas.drop3; Misc_defs_and_lemmas.part4;Misc_defs_and_lemmas.drop0; Misc_defs_and_lemmas.part5; Misc_defs_and_lemmas.part7; Misc_defs_and_lemmas.part8; Misc_defs_and_lemmas.part0;]));; let K_SCS_OPP=prove(`scs_k_v39 (scs_opp_v39 s) = scs_k_v39 s`, REWRITE_TAC[scs_v39_explicit;scs_opp_v39;LET_DEF;LET_END_DEF;is_scs_v39;peropp] );; let DUAL_NEG_PEROPP=prove(`~(k=0) /\ periodic ww k==>(\i. --peropp (\i. --peropp (ww:num->real^N) k i) k i)= ww`, STRIP_TAC THEN ASM_SIMP_TAC[FUN_EQ_THM;peropp;OPP_SUC_MOD;VECTOR_ARITH`-- -- A=A:real^N`] THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`ww:num->real^N`][ARITH_3_TAC;]);; let DUALNEG_PEROPP_BB=prove(`scs_k_v39 s=k /\BBs_v39 (scs_opp_v39 s) ww /\ ~(k<=3) ==> (\i. --peropp (\i. --peropp (ww:num->real^3) k i) k i)= ww`, STRIP_TAC THEN MATCH_MP_TAC DUAL_NEG_PEROPP THEN ASM_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBs_v39;scs_opp_v39] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC);; let BBPRIME_EQ_OPP_SYM_0=prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3) ==> BBprime_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`, REPEAT GEN_TAC THEN STRIP_TAC THEN MP_TAC PEROPP_IN_BB_SYM_0 THEN RESA_TAC THEN MRESA_TAC(GEN_ALL OPP_IS_SCS)[`scs_opp_v39 s`;`s:scs_v39`] THEN MP_TAC SCS_OPP_REFL THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBprime_v39] THEN REPEAT RESA_TAC THENL[ MRESAL_TAC (GEN_ALL PEROPP_IN_BB_SYM_0)[`scs_opp_v39 s`;`ww:num->real^3`;`k:num`][K_SCS_OPP;] THEN MP_TAC TAUSTAR_EQ_SYM_0 THEN RESA_TAC THEN MP_TAC DUALNEG_PEROPP_BB THEN RESA_TAC THEN MRESA_TAC (GEN_ALL TAUSTAR_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(\i. --peropp (ww:num->real^3) k i)`] THEN REPLICATE_TAC (13-3)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESAL1_TAC th`(\i. --peropp (ww:num->real^3) k i)`[ARITH_3_TAC]); MP_TAC TAUSTAR_EQ_SYM_0 THEN RESA_TAC]);; let BBINDEX_EQ_SYM_0=prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3) ==> BBindex_v39 (scs_opp_v39 s) (\i. --peropp vv k i) = BBindex_v39 s vv`, [ STRIP_TAC THEN ASM_REWRITE_TAC[BBindex_v39;scs_opp_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;peropp;DIST_SYM_0] THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN MATCH_MP_TAC CARD_IMAGE_INJ_EQ THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`(\x:num. (k - SUC(SUC (x MOD k)MOD k)))` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC; MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC`0..k` THEN REWRITE_TAC[FINITE_NUMSEG;SUBSET;IN_NUMSEG;IN_ELIM_THM] THEN ARITH_TAC; STRIP_TAC; GEN_TAC THEN RESA_TAC; ASM_SIMP_TAC[OPP_SUC_MOD] THEN MRESA_TAC MOD_LT[`x:num`;`k:num`] THEN MRESA_TAC DIVISION[`SUC x:num`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x MOD k< k/\ ~(k<=3)==> k - SUC (SUC x MOD k) < k /\ SUC (k-1)=k/\ k-1 x=k-1\/ SUC x REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_3_TAC;] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN REPLICATE_TAC (4)(POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT RESA_TAC; MRESA_TAC DIVISION[`SUC x:num`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC x SUC (k - SUC (SUC x))= k- SUC x/\ k - SUC x k - SUC (SUC y MOD k) < k/\ SUC(k-1)=k/\ k-1 y=k-1\/ SUC y REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39] THEN REPEAT DISCH_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`scs_a_v39 s (k-1)`][ARITH_3_TAC;periodic] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC]) THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`scs_k_v39 s`;`vv:num->real^3`][ARITH_3_TAC;] THEN POP_ASSUM (fun th-> MRESAL1_TAC th`k:num`[ARITH_3_TAC;]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN REPLICATE_TAC (4)(POP_ASSUM MP_TAC) THEN ASM_REWRITE_TAC[] THEN REPEAT RESA_TAC THEN POP_ASSUM(fun th-> ASM_REWRITE_TAC[SYM th]); REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC MOD_LT[`y':num`;`k:num`] THEN STRIP_TAC THEN MRESA_TAC DIVISION[`SUC y':num`;`k:num`] THEN MP_TAC(ARITH_RULE`SUC y' MOD k< k /\ k - SUC (SUC y' MOD k) = k - 1 ==> SUC y' MOD k=0`) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`y' SUC y' k- SUC(SUC y) REPEAT STRIP_TAC THEN MP_TAC th) THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[periodic2;is_scs_v39;LET_DEF;LET_END_DEF;BBprime_v39;BBs_v39] THEN REPEAT RESA_TAC THEN REPLICATE_TAC (3)(POP_ASSUM MP_TAC) THEN MP_TAC(ARITH_RULE`y' SUC y' y'= k-SUC(SUC y)`) THEN RESA_TAC; MRESA_TAC MOD_LT[`k-1`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`1:num`][ARITH_RULE`A*1=A/\ k-0=k /\ SUC 0=1/\ k-k=0`] THEN MP_TAC(ARITH_RULE`SUC y ~(k-1=y)`) THEN RESA_TAC]);; let IMAGE_BBINDEX_SYM_0=prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3) ==>(IMAGE (BBindex_v39 (scs_opp_v39 s)) (BBprime_v39 (scs_opp_v39 s))) = (IMAGE (BBindex_v39 s) (BBprime_v39 s))`, REPEAT STRIP_TAC THEN REWRITE_TAC[IMAGE;IN_ELIM_THM;EXTENSION] THEN REWRITE_TAC[IN] THEN GEN_TAC THEN EQ_TAC THEN RESA_TAC THENL[ MRESA_TAC(GEN_ALL OPP_IS_SCS)[`scs_opp_v39 s`;`s:scs_v39`] THEN MP_TAC SCS_OPP_REFL THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL BBPRIME_EQ_OPP_SYM_0)[`scs_opp_v39 s`;`x':num->real^3`;`k:num`][K_SCS_OPP;] THEN EXISTS_TAC`(\i. --peropp (x':num->real^3) k i)` THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN REWRITE_TAC[BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;] THEN REPEAT RESA_TAC THEN MRESA_TAC(GEN_ALL DUALNEG_PEROPP_BB)[`s:scs_v39`;`k:num`;`x':num->real^3`] THEN MRESAL_TAC (GEN_ALL BBINDEX_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(\i. --peropp (x':num->real^3) k i)`][BBprime_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;]; EXISTS_TAC`(\i. --peropp (x':num->real^3) k i)` THEN MRESAL_TAC (GEN_ALL BBPRIME_EQ_OPP_SYM_0)[`s:scs_v39`;`x':num->real^3`;`k:num`][K_SCS_OPP;] THEN MRESA_TAC (GEN_ALL BBINDEX_EQ_SYM_0)[`k:num`;`s:scs_v39`;`(x':num->real^3)`]]);; let BBINDEX_MIN_SYM_0=prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime_v39 s vv /\ ~(k<=3) ==> BBindex_min_v39 (scs_opp_v39 s) =BBindex_min_v39 (s)`, STRIP_TAC THEN ASM_REWRITE_TAC[BBindex_min_v39;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;peropp;DIST_SYM_0] THEN MP_TAC(ARITH_RULE`~(k<=3)==> ~(k=0)`) THEN RESA_TAC THEN MP_TAC IMAGE_BBINDEX_SYM_0 THEN RESA_TAC);; let BBPRIME2_SYM_0=prove(`scs_k_v39 s=k /\ is_scs_v39 s /\ BBprime2_v39 s vv /\ ~(k<=3) ==> BBprime2_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`, STRIP_TAC THEN MP_TAC BBPRIME_EQ_OPP_SYM_0 THEN RESA_TAC THEN MP_TAC BBINDEX_EQ_SYM_0 THEN RESA_TAC THEN MP_TAC BBINDEX_MIN_SYM_0 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;BBprime2_v39] THEN REPEAT RESA_TAC) ;; let MM_SCS_OPP=prove_by_refinement(`scs_k_v39 s=k /\ is_scs_v39 s /\ MMs_v39 s vv /\ ~(k<=3) ==> MMs_v39 (scs_opp_v39 s) (\i. -- peropp vv k i)`, [ STRIP_TAC THEN MP_TAC BBPRIME2_SYM_0 THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;MMs_v39;scs_opp_v39;peropp;AZIM_NEG;BBprime2_v39;BBprime_v39] THEN REPEAT RESA_TAC THEN ABBREV_TAC`V= IMAGE (vv:num->real^3) (:num)` THEN ABBREV_TAC`E = IMAGE (\i. {(vv:num->real^3) i, vv (SUC i)}) (:num)` THEN ABBREV_TAC`FF = IMAGE (\i. ((vv:num->real^3) i, vv (SUC i))) (:num)` THEN MP_TAC LOCAL_FAN_DUAL_SYM_0 THEN RESA_TAC; SUBGOAL_THEN`--(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k)) IN IMAGE (\i. --vv (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num)` ASSUME_TAC; REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[SET_RULE`(i:num)IN(:num)`]; SUBGOAL_THEN`--vv (k - SUC ((i + k - 1) MOD k)),--vv (k - SUC (i MOD k)) IN IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num)`ASSUME_TAC; REWRITE_TAC[IMAGE;IN_ELIM_THM] THEN EXISTS_TAC`i+k-1:num` THEN ASM_REWRITE_TAC[SET_RULE`(i:num)IN(:num)`] THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(i+k-1)=1*k+i/\ ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`i:num`]; MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR) [`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`;` IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;` IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num)`;`((--(vv:num->real^3) (k - SUC (i MOD k))) ,(--vv (k - SUC (SUC i MOD k))))`] THEN MRESA_TAC(GEN_ALL Local_lemmas.LOCAL_FAN_IN_FF_NOT_COLLINEAR) [`IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k))) (:num)`;` IMAGE (\i. {--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}) (:num)`;` IMAGE (\i. --(vv:num->real^3) (k - SUC (i MOD k)),--vv (k - SUC (SUC i MOD k))) (:num)`;`((--vv (k - SUC ((i + k - 1) MOD k))), (--(vv:num->real^3) (k - SUC (i MOD k))) )`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC (SUC i MOD k))}`][ELEMENT2_SYM_0;REFL_SYM_0] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM ELEMENT2_SYM_0] THEN ASM_REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`] THEN MRESAL_TAC(GEN_ALL VEC0_NOT_COLLINEAR_SYM_0)[`{--(vv:num->real^3) (k - SUC (i MOD k)), --vv (k - SUC ((i + k - 1) MOD k))}`][ELEMENT2_SYM_0;REFL_SYM_0] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM ELEMENT2_SYM_0] THEN ASM_REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[AZIM_NEG] THEN REPLICATE_TAC (26-6)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(k - SUC (i MOD k))`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`~(k<=3)==> SUC(i+k-1)=1*k+i/\ ~(k=0)/\ k-1 SUC (k - SUC (i MOD k))=k-i MOD k/\ (i MOD k + k - 1) + 1= 1*k + i MOD k`) THEN RESA_TAC THEN ASM_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;PAIR_EQ;LET_DEF;LET_END_DEF;scs_v39_explicit;peropp2;MMs_v39;scs_opp_v39;peropp;AZIM_NEG;BBprime2_v39;BBprime_v39;BBs_v39] THEN REPEAT RESA_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC(GEN_ALL PERIODIC_PROPERTY)[`k:num`;`vv:num->real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k - SUC (i MOD k) + k - 1`] THEN MRESA_TAC th[`k - SUC (SUC i MOD k)`]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN ASM_SIMP_TAC[ADD1] THEN MRESA_TAC MOD_LT[`1:num`;`k:num`] THEN MRESA_TAC MOD_LT[`0:num`;`k:num`] THEN MRESA_TAC MOD_LT[`k-1:num`;`k:num`] THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`k-1:num`;`k:num`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_ADD_MOD[`i:num`;`1:num`;`k:num`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th]) THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`0:num`] THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`k-2:num`] THEN MP_TAC(ARITH_RULE`i MOD k=0 \/ 0real^3`][ARITH_RULE`~(3=0)`;] THEN POP_ASSUM(fun th-> MRESA_TAC th[`k:num`]); MP_TAC(ARITH_RULE`0< i MOD k/\ ~(k<=3)/\ i MOD k i MOD k + k - 1= 1*k+ (i MOD k -1)/\ i MOD k-1 i MOD k=k-1\/ i MOD k +1k-1+1=k`) THEN RESA_TAC; MRESA_TAC MOD_LT[`i MOD k +1`;`k:num`] THEN MP_TAC(ARITH_RULE`i MOD k +1 k - (i MOD k + 1) + k - 1= 1*k+(k - ((i MOD k + 1) + 1))`) THEN RESA_TAC THEN MRESA_TAC MOD_MULT_ADD[`1`;`k:num`;`k - ((i MOD k + 1) + 1)`]; ASM_REWRITE_TAC[NORM_NEG] THEN REPLICATE_TAC (20-7)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(k - SUC (i MOD k))`]) ; ASM_REWRITE_TAC[NORM_NEG] THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(k - SUC (i MOD k))`]); ASM_REWRITE_TAC[DIST_SYM_0] THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(k - SUC (i MOD k))`]); ASM_REWRITE_TAC[DIST_SYM_0] THEN REPLICATE_TAC (20-8)(POP_ASSUM MP_TAC) THEN POP_ASSUM(fun th-> REPEAT STRIP_TAC THEN MRESA_TAC th[`(k - SUC (i MOD k))`])]) ;; let YXIONXL2=prove_by_refinement( `!s. is_scs_v39 s /\ scs_k_v39 s=k /\ ~(k<=3) ==> scs_arrow_v39 {s} {scs_opp_v39 s}`, [REPEAT GEN_TAC THEN REWRITE_TAC[scs_arrow_v39;IN_SING;subdiv_v39;PAIR_EQ;LET_DEF;LET_END_DEF;] THEN REPEAT RESA_TAC; MRESA_TAC(GEN_ALL OPP_IS_SCS)[`(scs_opp_v39 s)`;`s:scs_v39`]; DISJ_CASES_TAC(SET_RULE`(!s'. s' = s ==> MMs_v39 s' = {}) \/ ~((!s'. s' = s ==> MMs_v39 s' = {}))`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_FORALL_THM;NOT_IMP] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN EXISTS_TAC`scs_opp_v39 s` THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`~(A={})<=> ?vv. vv IN A`;IN] THEN STRIP_TAC THEN EXISTS_TAC`(\i. -- peropp (vv:num->real^3) k i)` THEN ASM_SIMP_TAC[MM_SCS_OPP]]);; end;; (* let check_completeness_claimA_concl = Ineq.mk_tplate `\x. scs_arrow_v13 (set_of_list x) *)