(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Chapter: Local Fan                                              *)
(* Author: Hoang Le Truong                                        *)
(* Date: 2012-04-01                                                           *)
(* ========================================================================= *)




module   Wjscpro = struct





open Polyhedron;;
open Sphere;;
open Fan_defs;;
open Hypermap;;
open Vol1;;
open Fan;;
open Topology;;		
open Fan_misc;;
open Planarity;; 
open Conforming;;
open Sphere;;
open Hypermap;;
open Fan;;
open Topology;;
open Prove_by_refinement;;
open Pack_defs;;
open Wrgcvdr_cizmrrh;;
open Local_lemmas;;
open Collect_geom;;
open Dih2k_hypermap;;



let POWER_MOD_FUN=
prove(`!n. 1<=n /\ 1<k ==> ((\i. ((1+i):num MOD k)) POWER n) i = (\i. ((n+i):num MOD k)) i`,
INDUCT_TAC THENL[ARITH_TAC; DISJ_CASES_TAC(ARITH_RULE`n=0 \/ 1<=n`) THENL[ ASM_REWRITE_TAC[POWER;I_DEF;ARITH_RULE`SUC 0=1`;o_DEF]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY") THEN STRIP_TAC THEN STRIP_TAC THEN REMOVE_THEN "THY" MP_TAC THEN RESA_TAC THEN ASM_REWRITE_TAC[COM_POWER;o_DEF;ADD1;MOD_ADD_MOD] THEN MP_TAC(ARITH_RULE`1<k==> ~(k=0)`) THEN RESA_TAC THEN MRESA_TAC MOD_LT[`1:num`;`k:num`] THEN MRESAL_TAC MOD_ADD_MOD[`1`;`n+i:num`;`k:num`][ARITH_RULE`(n + 1) + i=1+n+i`]]]);;
let CLOSED_SY=
prove_by_refinement(` stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 1< k /\ 2<k ==> closed {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v /\ CONDITION2_SY v }`,
[REWRITE_TAC[CONDITION2_SY;CONDITION1_SY;stable_system] THEN REPEAT GEN_TAC THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[LIM_SEQUENTIALLY; IN_ELIM_THM; dist] THEN REPEAT STRIP_TAC THEN ASM_TAC THEN DISCH_THEN(LABEL_TAC"THYGIANG2") THEN DISCH_THEN(LABEL_TAC"THYGIANG") THEN DISCH_THEN(LABEL_TAC"THYGIANG1") THEN REPEAT STRIP_TAC THEN EXISTS_TAC`vecmats (l:real^(M,3)finite_product)` THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[SKOLEM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY1") THEN DISCH_THEN(LABEL_TAC"THY2") THEN SUBGOAL_THEN` !i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) ==> ((\n. row i (v n) - row j ((v:num->real^3^M) n)) --> row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) sequentially`ASSUME_TAC; SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY] THEN REPEAT STRIP_TAC THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`] THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`) THEN RESA_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e/ &2:real`) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY2") THEN EXISTS_TAC`N:num` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`) THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`j-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`j-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN MRESAL_TAC NORM_TRIANGLE[`row i ((v:num->real^3^M) n) - row i (vecmats (l:real^(M,3)finite_product))`;`--(row j ((v:num->real^3^M) n) - row j (vecmats (l:real^(M,3)finite_product)))`][NORM_NEG;VECTOR_ARITH`A+ --B=A-B:real^N` ] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; SUBGOAL_THEN` !i. 1 <= i /\ i <= dimindex (:M) ==> ((\n. row i ((v:num->real^3^M) n)) --> row i (vecmats (l:real^(M,3)finite_product))) sequentially`ASSUME_TAC; SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY] THEN REPEAT STRIP_TAC THEN SIMP_TAC[dist;VECTOR_ARITH`A-B-(C-D)=(A-C)-(B-D):real^N`] THEN MP_TAC(REAL_ARITH`&0< e==> &0< e/ &2`) THEN RESA_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`e:real`) THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY2") THEN EXISTS_TAC`N:num` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY2"(fun th-> MRESA1_TAC th`n:num`) THEN MP_TAC(ARITH_RULE`1<=i /\ i <= dimindex (:M)==> i -1 < dimindex (:M)/\ SUC(i-1)=i`) THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<=j /\ j <= dimindex (:M)==> j -1 < dimindex (:M)/\ SUC(j-1)=j`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`((v:num->real^3^M) n)`] THEN MRESA_TAC (GEN_ALL VECMAT_ROW)[`i-1`;`vecmats (l:real^(M,3)finite_product)`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[MATVEC_VECMATS_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL NORM_VECMAT)[`i-1`;`matvec ((v:num->real^3^M) n) - (l:real^(M,3)finite_product)`][VECMAT_SUB] THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU2") THEN SUBGOAL_THEN`(!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) ==> (a:num#num->real) (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\ norm (row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))) <= (b:num#num->real) (i,j))` ASSUME_TAC; REPEAT STRIP_TAC; MRESA_TAC LIM_NORM_LBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(a:num#num->real)(i,j)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]; MRESA_TAC LIM_NORM_UBOUND[`sequentially`;`(\n. row i (v n) - row j ((v:num->real^3^M) n))`;`row i (vecmats l) - row j (vecmats (l:real^(M,3)finite_product))`;`(b:num#num->real)(i,j)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[EVENTUALLY_SEQUENTIALLY;TRIVIAL_LIMIT_SEQUENTIALLY;LIM_SEQUENTIALLY]; ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) /\ ~(i=j) ==> &2 <= norm (row i (vecmats (l:real^(M,3)finite_product)) - row j (vecmats l))` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY3") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY3"(fun th-> MRESA_TAC th[`i:num`;`j:num`]) THEN MATCH_MP_TAC(REAL_ARITH`a (i,j) <= norm (row i (vecmats l) - row j (vecmats l)) /\ &2<= a(i,j)==> &2 <= norm (row i (vecmats l) - row j (vecmats l))`) THEN MP_TAC(ARITH_RULE`i <= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`); RESA_TAC; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`); RESA_TAC; REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`]); MP_TAC(ARITH_RULE`1<= i==> ~(i = 0)`) THEN RESA_TAC THEN REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`]) THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`); RESA_TAC; MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`) THEN RESA_TAC THEN REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`]); POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th]) THEN SET_TAC[]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY3") THEN DISCH_THEN(LABEL_TAC"THY4") THEN SUBGOAL_THEN`!i. 1 <= i /\ i <= dimindex (:M) ==> norm (row i (vecmats (l:real^(M,3)finite_product)) - row (SUC (i MOD dimindex (:M))) (vecmats l))<= cstab` ASSUME_TAC; REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`i<= dimindex (:M) ==> i< dimindex (:M) \/ i=dimindex (:M)`) THEN RESA_TAC; MP_TAC(ARITH_RULE`i< dimindex (:M) ==> i<= dimindex (:M) /\ i+1<=dimindex (:M) /\ i<= dimindex (:M)-1`) THEN RESA_TAC THEN MRESAL_TAC MOD_LT[`i:num`;`k:num`][ADD1] THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`][ARITH_RULE`1<= i+1`]) THEN POP_ASSUM MP_TAC THEN REMOVE_THEN"THYGIANG1"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL1_TAC th`i:num`[ARITH_RULE`0<= i:num`]) THEN POP_ASSUM MP_TAC THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`i+1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`i+1:num`;`k:num`] THEN MRESAL_TAC MOD_MULT_ADD[`1`;`k:num`;`i+1`][ARITH_RULE`1*A=A`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[ARITH_RULE`A+1=1+A`] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ SUC 0=1`] THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`k:num`;`1:num`][ARITH_RULE`1<= 1/\ dimindex (:M) <= dimindex (:M)`;DIMINDEX_GE_1]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE` (1 <= dimindex (:M)) ==> 0 <= dimindex (:M) - 1` ) THEN SIMP_TAC[DIMINDEX_GE_1] THEN STRIP_TAC THEN REMOVE_THEN"THYGIANG1"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL1_TAC th`0:num`[ARITH_RULE`0<= 0:num/\ 0+1=1`;]) THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_LT[`1:num`;`k:num`][ARITH_RULE`0<1`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`k:num`;`1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `] THEN MRESAL_TAC th[`0:num`;`1:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN MP_TAC(ARITH_RULE`1<k ==> 1<=k`) THEN RESA_TAC THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REAL_ARITH_TAC; SUBGOAL_THEN`(!i. 1 <= i /\ i <= dimindex (:M) ==> row i (vecmats (l:real^(M,3)finite_product)) IN ball_annulus)` ASSUME_TAC; MP_TAC COMPACT_BALL_ANNULUS THEN ASM_SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED] THEN REWRITE_TAC[CLOSED_SEQUENTIAL_LIMITS] THEN REWRITE_TAC[ IN_ELIM_THM; dist] THEN REWRITE_TAC[SKOLEM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN REPEAT STRIP_TAC THEN REMOVE_THEN "YEU" (fun th-> MRESA_TAC th[`(\n. row i ((v:num->real^3^M) n)) `;` row i (vecmats (l:real^(M,3)finite_product))`]) THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[]; SUBGOAL_THEN`!i. 1 <= i /\ i <= dimindex (:M) ==> ~(row i (vecmats l) = row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))) `ASSUME_TAC; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY5") THEN REPEAT STRIP_TAC THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`] THEN REMOVE_THEN"THY5"(fun th-> MRESAL_TAC th[`i:num`;`SUC (i MOD dimindex (:M))`][VECTOR_ARITH`A-A = vec 0`;NORM_0]) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[convex_local_fan] THEN ASM_REWRITE_TAC[local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN SUBGOAL_THEN `FAN (vec 0,V_SY (vecmats (l:real^(M,3)finite_product)),E_SY (vecmats l))`ASSUME_TAC; REWRITE_TAC[FAN] THEN STRIP_TAC; REWRITE_TAC[SUBSET;UNIONS;E_SY;V_SY;IN_ELIM_THM;rows] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SET_RULE`A IN {B,C}<=> A=B \/ A=C`] THEN STRIP_TAC; EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; STRIP_TAC; REWRITE_TAC[GRAPH;E_SY;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[HAS_SIZE] THEN ASM_SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY ; IN_INSERT; NOT_IN_EMPTY] THEN ARITH_TAC; STRIP_TAC; REWRITE_TAC[fan1;V_SY;rows] THEN STRIP_TAC; MRESAL_TAC FINITE_IMAGE[`(\i. row i (vecmats (l:real^(M,3)finite_product)))`;`1..k`][IMAGE;IN_ELIM_THM;FINITE_NUMSEG;IN_NUMSEG] THEN POP_ASSUM MP_TAC THEN SUBGOAL_THEN`{y | ?x. (1 <= x /\ x <= dimindex (:M)) /\ y = row x (vecmats l)}={row i (vecmats (l:real^(M,3)finite_product)) | 1 <= i /\ i <= dimindex (:M)}`ASSUME_TAC; REWRITE_TAC[EXTENSION;IN_ELIM_THM]; ASM_REWRITE_TAC[]; REWRITE_TAC[SET_RULE`~(A SUBSET {})<=> ?a. a IN A`;IN_ELIM_THM] THEN EXISTS_TAC`row 1(vecmats (l:real^(M,3)finite_product))` THEN EXISTS_TAC`1` THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`;DIMINDEX_GE_1]; STRIP_TAC; REWRITE_TAC[fan2;V_SY;IN_ELIM_THM;rows;NOT_EXISTS_THM;DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`~(1<= i) \/ 1<= i`); ASM_REWRITE_TAC[]; DISJ_CASES_TAC(SET_RULE`~(i<= dimindex (:M)) \/ i<= dimindex (:M)`); ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUEM") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"YEUEM"(fun th-> MRESAL1_TAC th `i:num`[ball_annulus;IN_ELIM_THM]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;DIFF;IN_ELIM_THM;ball;DE_MORGAN_THM;dist;VECTOR_ARITH`vec 0- vec 0=vec 0`;NORM_0;REAL_ARITH`&0< &2`]); SUBGOAL_THEN`!i. (1 <= i /\ i <= dimindex (:M)) ==> ~collinear ({vec 0} UNION {row i (vecmats l), row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))})`ASSUME_TAC; REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS THEN ASM_SIMP_TAC[] THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`] THEN ASM_SIMP_TAC[]; POP_ASSUM MP_TAC THEN REWRITE_TAC[SET_RULE`{A} UNION {B,C}={A,B,C}`] THEN REPEAT STRIP_TAC; REWRITE_TAC[fan6;E_SY;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NONPARALLEL_BALL_ANNULUS THEN ASM_SIMP_TAC[] THEN MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`] THEN ASM_SIMP_TAC[]; REWRITE_TAC[fan7;] THEN SUBGOAL_THEN`!i. 1 <= i /\ i <= dimindex (:M) ==> ~(vec 0= row i (vecmats l)) /\ ~(vec 0 = row (SUC (i MOD dimindex (:M)))(vecmats (l:real^(M,3)finite_product)))`ASSUME_TAC; STRIP_TAC THEN STRIP_TAC THEN MRESA_TAC th3[`(vec 0):real^3`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[]; SUBGOAL_THEN`!u w. u IN V_SY (vecmats l) /\ w IN V_SY (vecmats (l:real^(M,3)finite_product)) ==> aff_ge {vec 0} {u} INTER aff_ge {vec 0} {w} = aff_ge {vec 0} ({u} INTER {w})`ASSUME_TAC; REWRITE_TAC[V_SY;IN_ELIM_THM;rows] THEN REPEAT STRIP_TAC THEN DISJ_CASES_TAC(SET_RULE`u=w:real^3 \/ {u} INTER {w}={}`); POP_ASSUM(fun th-> REWRITE_TAC[th;SET_RULE`A INTER A=A`]); ASM_REWRITE_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[SET_RULE`{u} INTER {w} = {} <=> ~(u=w) `;EXTENSION; INTER;IN_ELIM_THM;IN_SING] THEN REPEAT STRIP_TAC THEN EQ_TAC; REPEAT STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL VEC0_BALL_ANNULUS) THEN EXISTS_TAC`u:real^3` THEN EXISTS_TAC`w:real^3` THEN DISJ_CASES_TAC(SET_RULE`i=i':num \/ ~(i=i')`); POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN SET_TAC[]); ASM_SIMP_TAC[]; REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[ENDS_IN_HALFLINE]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY50") THEN DISCH_THEN(LABEL_TAC"THY5") THEN DISCH_THEN(LABEL_TAC"THY55") THEN DISCH_THEN(LABEL_TAC"THY6") THEN DISCH_THEN(LABEL_TAC"THY7") THEN DISCH_THEN(LABEL_TAC"THY8") THEN SUBGOAL_THEN`!e1 v. e1 IN E_SY (vecmats l) /\ v IN V_SY (vecmats (l:real^(M,3)finite_product)) ==> aff_ge {vec 0} e1 INTER aff_ge {vec 0} {v} = aff_ge {vec 0} (e1 INTER {v})` ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"GIANG") THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN ASM_REWRITE_TAC[] THEN DISJ_CASES_TAC(SET_RULE`y= v' \/ z= v' \/ (~(v'=y)/\ ~(v'=z:real^3))`); ASM_REWRITE_TAC[SET_RULE`{A,B} INTER {A}={A}`] THEN REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN SET_TAC[]; POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_REWRITE_TAC[SET_RULE`{A,B} INTER {B}={B}`] THEN REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN SET_TAC[]; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "THY6"(fun th-> MRESA1_TAC th`i:num`) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`v':real^3`] THEN MRESA_TAC th[`z:real^3`;`v':real^3`]) THEN MP_TAC(SET_RULE`~(y= v') /\ ~(z= v') ==> {y} INTER {v':real^3}={}/\ {z} INTER {v':real^3}={} /\ {y,z} INTER {v':real^3}={}`) THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`(A UNION B UNION C) INTER D=(A INTER D) UNION (B INTER D) UNION (C INTER D)`;SET_RULE`A UNION A=A`] THEN REMOVE_THEN "THY50"(fun th-> MRESA1_TAC th`i:num`) THEN USE_THEN"GIANG" MP_TAC THEN REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN STRIP_TAC THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\ SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "THY5"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MRESA1_TAC th`(SUC (i MOD dimindex (:M))):num`) THEN DISJ_CASES_TAC(SET_RULE`i= i' \/ ~(i= i':num)`); POP_ASSUM( fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC); DISJ_CASES_TAC(SET_RULE`i'= SUC (i MOD dimindex (:M)) \/ ~(i'= SUC (i MOD dimindex (:M)):num)`); POP_ASSUM( fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT RESA_TAC); MRESA_TAC (GEN_ALL SUC_NOT)[`i:num`;`k:num`] THEN REMOVE_THEN"THY4"(fun th-> MRESA_TAC th[`i':num`;`i:num`] THEN MRESA_TAC th[`i':num`;`SUC (i MOD dimindex (:M)):num`] THEN MRESA_TAC th[`i:num`;`SUC (i MOD dimindex (:M)):num`]) THEN DISJ_CASES_TAC(SET_RULE`collinear{vec 0, y, v':real^3}\/ ~collinear{vec 0, y, v':real^3}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESA_TAC (GEN_ALL Local_lemmas.collinear_fan22)[`vec 0:real^3`;`v':real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`] THEN RESA_TAC THEN REMOVE_THEN"THY7"(fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC Planarity.sym_line_fan[`vec 0:real^3`;`v':real^3`;`y:real^3`][SET_RULE`DISJOINT {x} {y,z} <=> ~(x=y)/\ ~(x=z)`] THEN MRESA_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0:real^3}`;`{v':real^3}`][SET_RULE`{A} UNION {B}={A,B}`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[aff] THEN STRIP_TAC THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v'} SUBSET affine hull {vec 0, v'} /\ affine hull {vec 0, v'} INTER aff_gt {vec 0} {y, z} = {} ==> aff_gt {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {v'} = {}`) THEN RESA_TAC THEN SET_TAC[]; DISJ_CASES_TAC(SET_RULE`collinear{vec 0, z, v':real^3}\/ ~collinear{vec 0, z, v':real^3}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESA_TAC (GEN_ALL Local_lemmas.collinear_fan22)[`vec 0:real^3`;`v':real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,B,A}`] THEN RESA_TAC THEN REMOVE_THEN"THY7"(fun th-> MRESA1_TAC th`i':num`) THEN MRESAL_TAC Planarity.sym_line_fan[`vec 0:real^3`;`v':real^3`;`z:real^3`][SET_RULE`DISJOINT {x} {y,z} <=> ~(x=y)/\ ~(x=z)`] THEN MRESA_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0:real^3}`;`{v':real^3}`][SET_RULE`{A} UNION {B}={A,B}`] THEN POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[aff] THEN STRIP_TAC THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {v'} SUBSET affine hull {vec 0, v'} /\ affine hull {vec 0, v'} INTER aff_gt {vec 0} {z,y} = {} ==> aff_gt {vec 0} { z:real^3,y} INTER aff_ge {vec 0} {v'} = {}`) THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; MRESA_TAC (GEN_ALL BALL_ANNULUS_4PONITS_AFF_GT)[`v':real^3`;`y:real^3`;`z:real^3`] THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`v':real^3`] THEN MRESA_TAC (GEN_ALL AFF_GE_INTER_AFF_GT_EQ_EMPTY)[`v':real^3`;`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN ASM_REWRITE_TAC[] THEN SET_TAC[]; SUBGOAL_THEN`!e1 e2. e1 IN E_SY (vecmats l) /\ e2 IN E_SY (vecmats (l:real^(M,3)finite_product)) /\ (e1 INTER e2={}) ==> aff_gt {vec 0} e1 INTER aff_gt {vec 0} e2 = {}` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEU") THEN REPEAT GEN_TAC THEN DISCH_TAC THEN POP_ASSUM (fun th-> MP_TAC th THEN REWRITE_TAC[E_SY;IN_ELIM_THM] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN MP_TAC th THEN STRIP_TAC) THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`y1=row i' (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`z1=row (SUC (i' MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y1, z1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y1, z1:real^3}={}`); POP_ASSUM MP_TAC THEN REWRITE_TAC[INTER;IN_ELIM_THM] THEN STRIP_TAC THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6")) THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`v3:real^3`;] THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`v3:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`;] THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z1:real^3`;`y1:real^3`;`v3:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH`(v3 cross y:real^3) dot y1 = &0 \/ &0< (v3 cross y) dot y1 \/ &0< --((v3 cross y) dot y1)`); MRESAL_TAC (GEN_ALL Local_lemmas.COPLANAR_IFF_CROSS_DOT)[`y:real^3`;`v3:real^3`;`y1:real^3`;`vec 0:real^3`;][VECTOR_ARITH`A- vec 0=A`] THEN SUBGOAL_THEN`y1 IN aff {vec 0, v3,y:real^3}` ASSUME_TAC; ASM_SIMP_TAC[Conforming.aff_3_rep_cross_dot;IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`]; POP_ASSUM MP_TAC THEN REWRITE_TAC[aff; AFFINE_HULL_3;IN_ELIM_THM;VECTOR_ARITH`A % vec 0+B=B`] THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASSUME_TAC(SYM th)) THEN DISJ_CASES_TAC(REAL_ARITH`&0<= w\/ &0<= -- w`); SUBGOAL_THEN`y1 IN aff_ge {vec 0,v3} {y:real^3}` ASSUME_TAC; ASM_SIMP_TAC[AFF_GE_2_1;th3;IN_ELIM_THM] THEN EXISTS_TAC`u:real` THEN EXISTS_TAC`v':real` THEN EXISTS_TAC`w:real` THEN ASM_REWRITE_TAC[] THEN VECTOR_ARITH_TAC; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v3:real^3`;`y:real^3`;`y1:real^3`]; MRESA_TAC Planarity.aff_gt3_subset_aff_gt[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {v3, y1} /\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1} /\ aff_gt {vec 0} {y1, z1} SUBSET aff_ge {vec 0} {y1, z1} ==> y IN aff_ge {vec 0} {y1, z1:real^3}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN STRIP_TAC THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`y:real^3`;] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y:real^3`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y} SUBSET aff_ge {vec 0} {y1, z1} ==> aff_ge {vec 0} {y1, z1} INTER aff_ge {vec 0} {y} =aff_ge {vec 0} {y:real^3} `) THEN RESA_TAC THEN SUBGOAL_THEN`y IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC; ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`y IN aff_gt {vec 0} {v3, y1}/\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1:real^3} ==> y IN aff_gt {vec 0} {y1, z1}`) THEN RESA_TAC THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`] THEN RESA_TAC THEN MRESA_TAC th3[`y:real^3`;`y1:real^3`;`vec 0:real^3`] THEN MRESA_TAC Planarity.properties_of_collinear4_points_fan[`vec 0:real^3`;`z1:real^3`;`y1:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={B,C,A}`] THEN RESA_TAC THEN MRESA_TAC th3[`z1:real^3`;`y:real^3`;`vec 0:real^3`] THEN MP_TAC(SET_RULE`~(y = y1) /\ ~(z1=y)==> {y1,z1:real^3} INTER {y}={}`) THEN RESA_TAC THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING]; MP_TAC(SET_RULE`v3 IN aff_gt {vec 0} {y, z} /\ aff_gt {vec 0} {y, z} SUBSET aff_ge {vec 0} {y, z} ==> v3 IN aff_ge {vec 0} {y, z:real^3}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN STRIP_TAC THEN MRESA_TAC Planarity.aff_ge1_subset_aff_ge[`vec 0:real^3`;`z:real^3`;`y:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {v3, y} /\ aff_ge {vec 0} {v3, y} SUBSET aff_ge {vec 0} {y, z} ==> y1 IN aff_ge {vec 0} {y, z:real^3}`) THEN RESA_TAC THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`;] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y1:real^3`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y1} SUBSET aff_ge {vec 0} {y, z} ==> aff_ge {vec 0} {y, z} INTER aff_ge {vec 0} {y1} =aff_ge {vec 0} {y1:real^3} `) THEN RESA_TAC THEN SUBGOAL_THEN`y1 IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC; ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`{y,z} INTER {y1,z1:real^3}={}==> {y,z} INTER {y1}={}`) THEN RESA_TAC THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING]; SUBGOAL_THEN`y1 IN aff_ge {vec 0,v3} {z:real^3}` ASSUME_TAC; ASM_SIMP_TAC[AFF_GE_2_1;th3;IN_ELIM_THM] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;VECTOR_ARITH`v' % (t2 % y + t3 % z) + w % y= (v' * t2+w) % y + (v'*t3) % z /\ t2' % (t2 % y + t3 % z) + t3' % z = (t2' *t2) % y + (t2'*t3+t3') % z`]) THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`&0<t2/\ &0< t3==> ~(t2= &0) /\ &0<= t3 /\ &0<= t2`) THEN RESA_TAC THEN MRESA1_TAC REAL_MUL_LINV`t2:real` THEN EXISTS_TAC`&1- (v' * t2 + w)* inv t2 -(v' * t3 - (v' * t2 + w)* inv t2 * t3):real` THEN EXISTS_TAC`(v' * t2 + w)* inv t2 :real` THEN EXISTS_TAC`v' * t3 - (v' * t2 + w)* inv t2 * t3:real` THEN ASM_REWRITE_TAC[REAL_ARITH`&1-A-B+A+B= &1/\ ((v' * t2 + w) * inv t2) * t3 + v' * t3 - (v' * t2 + w) * inv t2 * t3 =v' * t3 /\ (A*B)*C=A*(B*C) /\A * &1=A /\ v' * t3 - (v' * t2 + w) * inv t2 * t3= (v' - v' * (inv t2 *t2) - w* inv t2) * t3 /\ A-A -B*C= (--B)* C`;] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_INV THEN ASM_REWRITE_TAC[]; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`v3:real^3`;`z:real^3`;`y1:real^3`]; MRESA_TAC Planarity.aff_gt3_subset_aff_gt[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3;SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {v3, y1} /\ aff_gt {vec 0} {v3, y1} SUBSET aff_gt {vec 0} {y1, z1} /\ aff_gt {vec 0} {y1, z1} SUBSET aff_ge {vec 0} {y1, z1} ==> z IN aff_ge {vec 0} {y1, z1:real^3}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN STRIP_TAC THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y1:real^3`;`z1:real^3`;`z:real^3`;] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`z:real^3`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {z} SUBSET aff_ge {vec 0} {y1, z1} ==> aff_ge {vec 0} {y1, z1} INTER aff_ge {vec 0} {z} =aff_ge {vec 0} {z:real^3} `) THEN RESA_TAC THEN SUBGOAL_THEN`z IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC; ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`(SUC (i MOD dimindex (:M))):num` THEN ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(SET_RULE`{y,z} INTER {y1,z1}={} ==> {y1, z1} INTER {z:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING]; MP_TAC(SET_RULE`v3 IN aff_gt {vec 0} {y, z} /\ aff_gt {vec 0} {y, z} SUBSET aff_ge {vec 0} {y, z} ==> v3 IN aff_ge {vec 0} {y, z:real^3}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN STRIP_TAC THEN MRESA_TAC Planarity.aff_ge1_subset_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3;] THEN STRIP_TAC THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {v3, z} /\ aff_ge {vec 0} {v3, z} SUBSET aff_ge {vec 0} {y, z} ==> y1 IN aff_ge {vec 0} {y, z:real^3}`) THEN RESA_TAC THEN MRESA_TAC Planarity.aff_ge_1_1_subset_aff_ge_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`;] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN MRESA_TAC th3[`vec 0:real^3`;`v3:real^3`;`y1:real^3`] THEN STRIP_TAC THEN MP_TAC(SET_RULE`aff_ge {vec 0} {y1} SUBSET aff_ge {vec 0} {y, z} ==> aff_ge {vec 0} {y, z} INTER aff_ge {vec 0} {y1} =aff_ge {vec 0} {y1:real^3} `) THEN RESA_TAC THEN SUBGOAL_THEN`y1 IN V_SY(vecmats (l:real^(M,3)finite_product))`ASSUME_TAC; ASM_SIMP_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[]; MP_TAC(SET_RULE`{y,z} INTER {y1,z1}={} ==> {y, z} INTER {y1:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"YEU"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING]; POP_ASSUM MP_TAC THEN STRIP_TAC; MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`y:real^3`;`y1:real^3`;`z1:real^3`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN RESA_TAC THEN SUBGOAL_THEN`&0<(z cross y) dot y1` ASSUME_TAC; REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`] THEN REWRITE_TAC[DOT_LMUL] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z cross y) dot y1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; SUBGOAL_THEN`&0< --((z cross y) dot z1)` ASSUME_TAC; REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`] THEN REWRITE_TAC[DOT_LMUL;REAL_ARITH`--(A*B)=A*(--B)`] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * --((z cross y) dot z1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; SUBGOAL_THEN`&0<(z1 cross y) dot y1` ASSUME_TAC; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`t* &0 +A=A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z1 cross y) dot y1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`z1:real^3`;`y:real^3`;`z:real^3`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN REWRITE_TAC[DOT_LNEG] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[REAL_ARITH`-- -- A=A`] THEN STRIP_TAC THEN SUBGOAL_THEN`&0< --((z1 cross z) dot y1)` ASSUME_TAC; POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`A+t* &0 =A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL;REAL_ARITH`--(A*B)= A*(--B)`] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t2==> ~(t2= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t2:real` THEN MRESA1_TAC REAL_MUL_LINV`t2:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t2`;`t2 * ((y1 cross z) dot z1)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`] THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\ SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\ SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`SUC (i' MOD dimindex (:M))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2")) THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z:real^3`;`y:real^3`;`y1:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< (z cross y) dot y1==> &0< ((z cross y) dot y1)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z cross y) dot y1)/ &4`) THEN SUBGOAL_THEN`!n. N <= n ==> &0< (row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n)`;`(z cross y) dot y1`]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY1") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z1:real^3`;`y:real^3`;`y1:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< (z1 cross y) dot y1==> &0< ((z1 cross y) dot y1)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z1 cross y) dot y1)/ &4`) THEN SUBGOAL_THEN`!n. N' <= n ==> &0< (row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row i' (v n)`;`(z1 cross y) dot y1`]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY2") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`z:real^3`;`y:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< --((z cross y) dot z1)==> &0< --((z cross y) dot z1)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z cross y) dot z1)/ &4`) THEN SUBGOAL_THEN`!n. N'' <= n ==> &0< --((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row (SUC (i' MOD dimindex (:M))) (v n)) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i (v n)) dot row (SUC (i' MOD dimindex (:M))) (v n))`;`--((z cross y) dot z1)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY3") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`z1:real^3`;`z:real^3`;`y1:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< --((z1 cross z) dot y1)==> &0< --((z1 cross z) dot y1)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z1 cross z) dot y1)/ &4`) THEN SUBGOAL_THEN`!n. N''' <= n ==> &0< --((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i MOD dimindex (:M))) (v n)) dot row i' (v n)) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i MOD dimindex (:M))) (v n)) dot row i' (v n))`;`--((z1 cross z) dot y1)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG]; MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N2:num. !n. N2<=n ==> ~( row (SUC (i MOD dimindex (:M))) (v n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`z:real^3`][o_DEF] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MP_TAC(SET_RULE`z IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`) THEN RESA_TAC; MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N3:num. !n. N3<=n ==> ~(row i ((v:num->real^3^M) n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row i ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`y:real^3`][o_DEF] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MP_TAC(SET_RULE`y IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY4") THEN DISCH_THEN(LABEL_TAC"YEUTHY5") THEN DISCH_THEN(LABEL_TAC"YEUTHY6") THEN ABBREV_TAC`N1=N+N'+N''+N'''+N2+N3:num` THEN MP_TAC(ARITH_RULE`N+N'+N''+N'''+N2+N3= N1:num ==> N<= N1/\ N'<= N1 /\ N''<= N1/\ N'''<= N1 /\ N2<= N1/\ N3<=N1`) THEN RESA_TAC THEN REMOVE_THEN "YEUTHY1"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY2"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY3"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY4"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY5"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY6"(fun th-> MRESA1_TAC th`N1:num`) THEN ABBREV_TAC`y'=row i ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`z'=row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`y1'=row i' ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`z1'=row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) N1)` THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[convex_local_fan;local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY1") THEN DISCH_THEN(LABEL_TAC"YEUTHY2") THEN SUBGOAL_THEN`{y',z'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`{y1',z1'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN "YEUTHY1"(fun th-> MRESAL1_TAC th`{y',z':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN MRESAL1_TAC th`{y1',z1':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`]) THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`y':real^3`;`z':real^3`;`y1':real^3`;`z1':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN STRIP_TAC THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`z1':real^3`;`y1':real^3`;`y':real^3`;`z':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC`a=(y' cross z')` THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ONCE_REWRITE_TAC[GSYM CROSS_LNEG] THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN STRIP_TAC THEN MP_TAC(SET_RULE`--((y1' cross z1') cross a') IN aff_gt {vec 0} {y1', z1'} /\ --((y1' cross z1') cross a') IN aff_gt {vec 0} {y', z'} /\ aff_gt {vec 0} {y', z'} SUBSET aff_ge {vec 0} {y', z'} /\ aff_gt {vec 0} {y1', z1'} SUBSET aff_ge {vec 0} {y1', z1'} ==> --((y1' cross z1') cross a') IN aff_ge {vec 0} {y', z'} INTER aff_ge {vec 0} {y1', z1'}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MP_TAC(SET_RULE`~(y' IN {y1',z1'}) /\ ~(z' IN {y1',z1':real^3})==> ({y',z'}INTER{y1',z1'}={})`) THEN RESA_TAC THEN REMOVE_THEN"YEUTHY2"(fun th-> MRESAL_TAC th[`{y',z':real^3}`;`{y1',z1':real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`vec 0:real^3`;`y':real^3`;`z':real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3]; POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN STRIP_TAC THEN MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`y1:real^3`;`y:real^3`;`z:real^3`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN RESA_TAC THEN SUBGOAL_THEN`&0<(z1 cross y1) dot y` ASSUME_TAC; REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`] THEN REWRITE_TAC[DOT_LMUL] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z1 cross y1) dot y)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; SUBGOAL_THEN`&0< --((z1 cross y1) dot z)` ASSUME_TAC; REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y1:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y1, z1:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;VECTOR_ARITH`t% vec 0 +A=A`] THEN REWRITE_TAC[DOT_LMUL;REAL_ARITH`--(A*B)=A*(--B)`] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * --((z1 cross y1) dot z)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; SUBGOAL_THEN`&0<(z cross y1) dot y` ASSUME_TAC; REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`t* &0 +A=A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t3==> ~(t3= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t3:real` THEN MRESA1_TAC REAL_MUL_LINV`t3:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t3`;`t3 * ((z cross y1) dot y)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`]; MRESAL_TAC Planarity.aff_gt_1_2_cross_dotr_4point[`vec 0:real^3`;`v3:real^3`;`z:real^3`;`y1:real^3`;`z1:real^3`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN REWRITE_TAC[DOT_LNEG] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[REAL_ARITH`-- -- A=A`] THEN STRIP_TAC THEN SUBGOAL_THEN`&0< --((z cross z1) dot y)` ASSUME_TAC; POP_ASSUM MP_TAC THEN MRESA_TAC AFF_GT_1_2[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3] THEN STRIP_TAC THEN FIND_ASSUM(MP_TAC)`v3 IN aff_gt {vec 0} {y, z:real^3}` THEN POP_ASSUM(fun th-> REWRITE_TAC[th;IN_ELIM_THM;VECTOR_ARITH`a % vec 0 + b=b`]) THEN RESA_TAC THEN REWRITE_TAC[CROSS_LADD;CROSS_LMUL;CROSS_REFL;REAL_ARITH`A+t* &0 =A`;DOT_LADD;DOT_CROSS_SELF;DOT_LMUL;REAL_ARITH`--(A*B)= A*(--B)`] THEN RESA_TAC THEN MP_TAC(REAL_ARITH`&0 < t2==> ~(t2= &0)`) THEN RESA_TAC THEN MRESA1_TAC REAL_LT_INV`t2:real` THEN MRESA1_TAC REAL_MUL_LINV`t2:real` THEN MRESAL_TAC REAL_LT_MUL[`inv t2`;`t2 * ((y cross z1) dot z)`][REAL_ARITH`A *B*C=(A*B)*C/\ &1*A=A`] THEN ONCE_REWRITE_TAC[GSYM CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\ SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`1 <= SUC (i' MOD dimindex (:M)) /\ SUC (i' MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`SUC (i' MOD dimindex (:M))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2")) THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z1:real^3`;`y1:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< (z1 cross y1) dot y==> &0< ((z1 cross y1) dot y)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z1 cross y1) dot y)/ &4`) THEN SUBGOAL_THEN`!n. N <= n ==> &0< (row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n)`;`(z1 cross y1) dot y`]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY1") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z:real^3`;`y1:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< (z cross y1) dot y==> &0< ((z cross y1) dot y)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`((z cross y1) dot y)/ &4`) THEN SUBGOAL_THEN`!n. N' <= n ==> &0< (row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`(row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row i (v n)`;`(z cross y1) dot y`]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY2") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i' ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`z1:real^3`;`y1:real^3`;`z:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< --((z1 cross y1) dot z)==> &0< --((z1 cross y1) dot z)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z1 cross y1) dot z)/ &4`) THEN SUBGOAL_THEN`!n. N'' <= n ==> &0< --((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row (SUC (i MOD dimindex (:M))) (v n)) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row i' (v n)) dot row (SUC (i MOD dimindex (:M))) (v n))`;`--((z1 cross y1) dot z)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY3") THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`z:real^3`;`z1:real^3`;`y:real^3`] THEN POP_ASSUM MP_TAC THEN SIMP_TAC[LIM_SEQUENTIALLY;dist;o_DEF;GSYM LIFT_SUB;NORM_LIFT] THEN MP_TAC(REAL_ARITH`&0< --((z cross z1) dot y)==> &0< --((z cross z1) dot y)/ &4`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th`--((z cross z1) dot y)/ &4`) THEN SUBGOAL_THEN`!n. N''' <= n ==> &0< --((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i' MOD dimindex (:M))) (v n)) dot row i (v n)) ` ASSUME_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"CHANGE") THEN REPEAT STRIP_TAC THEN REMOVE_THEN"CHANGE"(fun th-> MRESA1_TAC th`n:num`) THEN MRESA_TAC ABS_LT_EPSI[`--((row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) n) cross row (SUC (i' MOD dimindex (:M))) (v n)) dot row i (v n))`;`--((z cross z1) dot y)`] THEN POP_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH`-- A - --B= --(A-B)`;REAL_ABS_NEG]; MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N2:num. !n. N2<=n ==> ~( row (SUC (i MOD dimindex (:M))) (v n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`z:real^3`][o_DEF] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MP_TAC(SET_RULE`z IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`) THEN RESA_TAC; MRESA1_TAC (SET_RULE`!A. ~A\/ A`)`(?N3:num. !n. N3<=n ==> ~(row i ((v:num->real^3^M) n) IN {row i' ((v:num->real^3^M) n), row (SUC (i' MOD dimindex (:M))) (v n)}))`; POP_ASSUM MP_TAC THEN REWRITE_TAC[NOT_EXISTS_THM;NOT_FORALL_THM;SKOLEM_THM;NOT_IMP;] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y:real^3`;`(\n. row i ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`y1:real^3`;`(\n. row i' ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z:real^3`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC (GEN_ALL LIM_SUBSEQUENCE1)[`z1:real^3`;`(\n. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) n))`;`n:num->num`][o_DEF] THEN MRESAL_TAC LIM_IN_SET[`(\m:num. row i' ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row (SUC (i' MOD dimindex (:M))) ((v:num->real^3^M) m)) o (n:num->num)`;`(\m:num. row i ((v:num->real^3^M) m)) o (n:num->num)`;`y1:real^3`;`z1:real^3`;`y:real^3`][o_DEF] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[] THEN STRIP_TAC THEN MP_TAC(SET_RULE`y IN{y1,z1}==> ~({y,z} INTER {y1,z1:real^3}={})`) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY4") THEN DISCH_THEN(LABEL_TAC"YEUTHY5") THEN DISCH_THEN(LABEL_TAC"YEUTHY6") THEN ABBREV_TAC`N1=N+N'+N''+N'''+N2+N3:num` THEN MP_TAC(ARITH_RULE`N+N'+N''+N'''+N2+N3= N1:num ==> N<= N1/\ N'<= N1 /\ N''<= N1/\ N'''<= N1 /\ N2<= N1/\ N3<=N1`) THEN RESA_TAC THEN REMOVE_THEN "YEUTHY1"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY2"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY3"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY4"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY5"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_THEN "YEUTHY6"(fun th-> MRESA1_TAC th`N1:num`) THEN ABBREV_TAC`y'=row i ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`z'=row (SUC (i MOD dimindex (:M))) ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`y1'=row i' ((v:num-> real^3^M) N1)` THEN ABBREV_TAC`z1'=row (SUC (i' MOD dimindex (:M))) ((v:num-> real^3^M) N1)` THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`N1:num`) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[convex_local_fan;local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[FAN;fan7;fan6] THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"YEUTHY1") THEN DISCH_THEN(LABEL_TAC"YEUTHY2") THEN SUBGOAL_THEN`{y',z'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`{y1',z1'} IN E_SY((v:num->real^3^M) N1)`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN "YEUTHY1"(fun th-> MRESAL1_TAC th`{y',z':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`] THEN MRESAL1_TAC th`{y1',z1':real^3}`[SET_RULE`{a} UNION {b,c}={a,b,c}`]) THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`y1':real^3`;`z1':real^3`;`y':real^3`;`z':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN STRIP_TAC THEN MRESAL_TAC Planarity.condition_cross_dot_4point[`vec 0:real^3`;`z':real^3`;`y':real^3`;`y1':real^3`;`z1':real^3`][VECTOR_ARITH`A- vec 0=A/\ A+ vec 0=A`] THEN POP_ASSUM MP_TAC THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ASM_REWRITE_TAC[DOT_LNEG;REAL_ARITH`-- --A=A`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ASM_REWRITE_TAC[] THEN ABBREV_TAC`a=(y1' cross z1')` THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN ONCE_REWRITE_TAC[GSYM CROSS_LNEG] THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] THEN ONCE_REWRITE_TAC[GSYM CROSS_SKEW] THEN ONCE_REWRITE_TAC[CROSS_SKEW] THEN STRIP_TAC THEN MP_TAC(SET_RULE`--((y' cross z') cross a') IN aff_gt {vec 0} {y1', z1'} /\ --((y' cross z') cross a') IN aff_gt {vec 0} {y', z'} /\ aff_gt {vec 0} {y', z'} SUBSET aff_ge {vec 0} {y', z'} /\ aff_gt {vec 0} {y1', z1'} SUBSET aff_ge {vec 0} {y1', z1'} ==> --((y' cross z') cross a') IN aff_ge {vec 0} {y', z'} INTER aff_ge {vec 0} {y1', z1'}`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MP_TAC(SET_RULE`~(y' IN {y1',z1'}) /\ ~(z' IN {y1',z1':real^3})==> ({y',z'}INTER{y1',z1'}={})`) THEN RESA_TAC THEN REMOVE_THEN"YEUTHY2"(fun th-> MRESAL_TAC th[`{y',z':real^3}`;`{y1',z1':real^3}`][UNION;IN_ELIM_THM;AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> ASM_TAC THEN REWRITE_TAC[th] THEN REPEAT STRIP_TAC) THEN MRESA_TAC Planarity.origin_is_not_aff_gt_fan[`vec 0:real^3`;`y':real^3`;`z':real^3`] THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[th3]; ASM_REWRITE_TAC[]; POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"MA1") THEN DISCH_THEN(LABEL_TAC"MA2") THEN REWRITE_TAC[UNION;IN_ELIM_THM] THEN REPEAT STRIP_TAC; POP_ASSUM(fun th-> POP_ASSUM(fun th1-> MP_TAC th1 THEN REWRITE_TAC[E_SY;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th1 )THEN MP_TAC th THEN REWRITE_TAC[E_SY;IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN ASSUME_TAC th) THEN ABBREV_TAC`y=row i (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`z=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`y1=row i' (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`z1=row (SUC (i' MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN DISJ_CASES_TAC(SET_RULE`{y,z}INTER {y1,z1:real^3}={} \/ {y,z} INTER {y1,z1}={y} \/ {y,z} INTER {y1,z1}={z}\/ {y,z} INTER {y1,z1}={y,z}`); ASM_SIMP_TAC[] THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6")) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`]) THEN MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {} ==> {y} INTER {y1:real^3}={}/\ {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {y,z} INTER {y1:real^3}={} /\ {y,z} INTER {z1:real^3}={} /\ {z} INTER {y1:real^3,z1}={}/\ {y} INTER {y1:real^3,z1}={}`) THEN RESA_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN RESA_TAC THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN REMOVE_THEN"MA2"(fun th-> MRESA_TAC th[`e1:real^3->bool`;`e2:real^3->bool`]) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; POP_ASSUM MP_TAC THEN STRIP_TAC; ASM_SIMP_TAC[] THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6")) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]; MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {y}==> y1=y \/ z1=y:real^3`) THEN RESA_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, z1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, z1:real^3}={}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`y:real^3`;`z:real^3`;`z1:real^3`;`v3:real^3`] THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`z1:real^3`]; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING] THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {y, z1} /\ aff_gt {vec 0} {y, z1} SUBSET aff_ge {vec 0} {y, z1:real^3} /\ aff_ge {vec 0} {y, z1:real^3} INTER aff_ge {vec 0} {z} = aff_ge {vec 0} ({y, z1:real^3} INTER {z}) /\ z IN aff_ge {vec 0} {z} ==> z IN aff_ge {vec 0} ({y, z1} INTER {z})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y, z1} = {y} ==> {y, z1} INTER {z:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`z1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z1:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z1:real^3`][IN_SING] THEN MP_TAC(SET_RULE`z1 IN aff_ge {vec 0} {y, z} /\ aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {z1} = aff_ge {vec 0} ({y, z:real^3} INTER {z1}) /\ z1 IN aff_ge {vec 0} {z1} ==> z1 IN aff_ge {vec 0} ({y, z} INTER {z1})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`y:real^3`;`z1:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=z1) /\ {y, z} INTER {y, z1} = {y} ==> {y, z} INTER {z1:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`]) THEN MRESA_TAC th3[`y:real^3`;`z1:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`{y, z} INTER {y, z1} = {y} /\ ~(y=z) /\ ~(y=z1) ==> {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y:real^3}={} /\ {y,z} INTER {z1:real^3}={} /\ {y,z1} INTER {z:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z1:real^3`][aff] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`][aff] THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`y:real^3`] THEN MP_TAC(SET_RULE` affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z1} = {} /\ affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z} = {} /\ aff_ge {vec 0} {y} SUBSET affine hull {vec 0, y:real^3} ==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y}={} /\ aff_ge {vec 0} {y} INTER aff_gt {vec 0} {y, z1}={}`) THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`{} UNION A=A /\ aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION (aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y} UNION aff_ge {vec 0} {}) UNION aff_ge {vec 0} {}= (aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {}) UNION (aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y} UNION aff_ge {vec 0} {}) `;] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING] THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING] THEN POP_ASSUM MP_TAC THEN SET_TAC[]; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, y1}) \/ aff_gt {vec 0} {y, z} INTER aff_gt {vec 0} {y, y1:real^3}={}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`y:real^3`;`z:real^3`;`y1:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`y:real^3`;`z:real^3`;`y1:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`z:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING] THEN MP_TAC(SET_RULE`z IN aff_gt {vec 0} {y1, y} /\ aff_gt {vec 0} {y1, y} SUBSET aff_ge {vec 0} {y1, y:real^3} /\ aff_ge {vec 0} {y1, y:real^3} INTER aff_ge {vec 0} {z} = aff_ge {vec 0} ({y1, y:real^3} INTER {z}) /\ z IN aff_ge {vec 0} {z} ==> z IN aff_ge {vec 0} ({y1, y} INTER {z})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[] THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y1, y} = {y} ==> {y, y1} INTER {z:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`y:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING] THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {y, z} /\ aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {y1} = aff_ge {vec 0} ({y, z:real^3} INTER {y1}) /\ y1 IN aff_ge {vec 0} {y1} ==> y1 IN aff_ge {vec 0} ({y, z} INTER {y1})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`y1:real^3`;`y:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=y1) /\ {y, z} INTER {y1, y} = {y} ==> {y, z} INTER {y1:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`]) THEN MRESA_TAC th3[`y1:real^3`;`y:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`{y, z} INTER {y1, y} = {y} /\ ~(y=z) /\ ~(y=y1) ==> {y} INTER {y1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {z} INTER {y:real^3}={} /\ {y,z} INTER {y1:real^3}={} /\ {y1,y} INTER {z:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`z:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`y1:real^3`][aff] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`y:real^3`;`z:real^3`][aff] THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`y:real^3`] THEN MP_TAC(SET_RULE` affine hull {vec 0, y} INTER aff_gt {vec 0} {y, y1} = {} /\ affine hull {vec 0, y} INTER aff_gt {vec 0} {y, z} = {} /\ aff_ge {vec 0} {y} SUBSET affine hull {vec 0, y:real^3} ==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y}={} /\ aff_ge {vec 0} {y} INTER aff_gt {vec 0} {y, y1}={}`) THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[SET_RULE`A UNION {}=A`;] THEN SUBGOAL_THEN`aff_gt{vec 0} {y1,y}=aff_gt{vec 0} {y,y1:real^3}` ASSUME_TAC; ASSUME_TAC(SET_RULE`{y1,y}={y,y1:real^3}`) THEN POP_ASSUM(fun th-> REWRITE_TAC[th]); ASM_REWRITE_TAC[SET_RULE`({} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1}) UNION ({} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {y} INTER aff_ge {vec 0} {y}) UNION aff_ge {vec 0} {} =(aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {}) UNION aff_ge {vec 0} {y}`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING] THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; ASM_SIMP_TAC[] THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6")) THEN MRESA_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.aff_ge_eq_aff_gt_union_aff_ge[`vec 0:real^3`;`y1:real^3`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]; MP_TAC(SET_RULE`{y, z} INTER {y1, z1} = {z}==> y1=z \/ z1=z:real^3`) THEN RESA_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {z,y} INTER aff_gt {vec 0} {z, z1}) \/ aff_gt {vec 0} {z,y} INTER aff_gt {vec 0} {z, z1:real^3}={}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`z:real^3`;`y:real^3`;`z1:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`z1:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING] THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {z, z1} /\ aff_gt {vec 0} {z, z1} SUBSET aff_ge {vec 0} {z, z1:real^3} /\ aff_ge {vec 0} {z, z1:real^3} INTER aff_ge {vec 0} {y} = aff_ge {vec 0} ({z, z1:real^3} INTER {y}) /\ y IN aff_ge {vec 0} {y} ==> y IN aff_ge {vec 0} ({z, z1} INTER {y})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {z, z1} = {z} ==> {z, z1} INTER {y:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`z1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`z:real^3`;`z1:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z1:real^3`][IN_SING] THEN MP_TAC(SET_RULE`z1 IN aff_ge {vec 0} {y, z} /\ aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {z1} = aff_ge {vec 0} ({y, z:real^3} INTER {z1}) /\ z1 IN aff_ge {vec 0} {z1} ==> z1 IN aff_ge {vec 0} ({y, z} INTER {z1})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`z:real^3`;`z1:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(z=z1) /\ {y, z} INTER {z, z1} = {z} ==> {y, z} INTER {z1:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; POP_ASSUM MP_TAC THEN SUBGOAL_THEN`aff_gt{vec 0} {z,y}=aff_gt{vec 0} {y,z:real^3}` ASSUME_TAC; ASSUME_TAC(SET_RULE`{z,y}={y,z:real^3}`) THEN POP_ASSUM(fun th-> REWRITE_TAC[th]); RESA_TAC THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`z1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i' MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`z1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`z1:real^3`]) THEN MRESA_TAC th3[`z:real^3`;`z1:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`{y, z} INTER {z, z1} = {z} /\ ~(y=z) /\ ~(z=z1) ==> {y} INTER {z1:real^3}={} /\ {z} INTER {z1:real^3}={} /\ {z} INTER {y:real^3}={} /\ {y,z} INTER {z1:real^3}={} /\ {z,z1} INTER {y:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`z1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`z1:real^3`][aff] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`][aff] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`z:real^3`] THEN MP_TAC(SET_RULE` affine hull {vec 0, z} INTER aff_gt {vec 0} {z, z1} = {} /\ affine hull {vec 0, z} INTER aff_gt {vec 0} {y, z} = {} /\ aff_ge {vec 0} {z} SUBSET affine hull {vec 0, z:real^3} ==> aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z}={} /\ aff_ge {vec 0} {z} INTER aff_gt {vec 0} {z, z1}={}`) THEN RESA_TAC THEN ASM_REWRITE_TAC[SET_RULE`({} UNION {} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1}) UNION aff_ge {vec 0} {} UNION {} UNION aff_ge {vec 0} {z} INTER aff_ge {vec 0} {z} UNION aff_ge {vec 0} {}= (aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {z1} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {}) UNION ( aff_ge {vec 0} {z}) `;] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING] THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN DISJ_CASES_TAC(SET_RULE`(?v3. v3 IN aff_gt {vec 0} {z, y} INTER aff_gt {vec 0} {z, y1}) \/ aff_gt {vec 0} {z, y} INTER aff_gt {vec 0} {z, y1:real^3}={}`); POP_ASSUM MP_TAC THEN RESA_TAC THEN MRESA_TAC POINT_COM_AFF_GT_INTER[`z:real^3`;`y:real^3`;`y1:real^3`;`v3:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MRESA_TAC Planarity.decomposition_planar_by_angle_fan[`vec 0:real^3`;`z:real^3`;`y:real^3`;`y1:real^3`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC; POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e2:(real^3->bool)`;`y:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y:real^3`][IN_SING] THEN MP_TAC(SET_RULE`y IN aff_gt {vec 0} {y1, z} /\ aff_gt {vec 0} {y1, z} SUBSET aff_ge {vec 0} {y1, z:real^3} /\ aff_ge {vec 0} {y1, z:real^3} INTER aff_ge {vec 0} {y} = aff_ge {vec 0} ({y1, z:real^3} INTER {y}) /\ y IN aff_ge {vec 0} {y} ==> y IN aff_ge {vec 0} ({y1, z} INTER {y})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[] THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y=z) /\ {y, z} INTER {y1, z} = {z} ==> { z,y1} INTER {y:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i':num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:(real^3->bool)`;`y1:real^3`][AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING]) THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`z:real^3`] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`y1:real^3`][IN_SING] THEN MP_TAC(SET_RULE`y1 IN aff_ge {vec 0} {y, z} /\ aff_ge {vec 0} {y, z:real^3} INTER aff_ge {vec 0} {y1} = aff_ge {vec 0} ({y, z:real^3} INTER {y1}) /\ y1 IN aff_ge {vec 0} {y1} ==> y1 IN aff_ge {vec 0} ({y, z} INTER {y1})`) THEN ASM_SIMP_TAC[AFF_GT_SUBSET_AFF_GE] THEN MRESA_TAC th3[`y1:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(z=y1) /\ {y, z} INTER {y1, z} = {z} ==> {y, z} INTER {y1:real^3}={}`) THEN RESA_TAC THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING]; POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN STRIP_TAC THEN SUBGOAL_THEN`z IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`SUC (i MOD dimindex (:M))` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y1 IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i':num` THEN ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`k:num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`y IN V_SY (vecmats (l:real^(M,3)finite_product))` ASSUME_TAC; REWRITE_TAC[IN_ELIM_THM;V_SY;rows] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN REMOVE_THEN"THY8"(fun th-> MRESA_TAC th[`y:real^3`;`y1:real^3`] THEN MRESA_TAC th[`z:real^3`;`y:real^3`] THEN MRESA_TAC th[`z:real^3`;`y1:real^3`]) THEN MRESA_TAC th3[`y1:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`{y, z} INTER {y1, z} = {z} /\ ~(y=z) /\ ~(z=y1) ==> {y} INTER {y1:real^3}={} /\ {z} INTER {y1:real^3}={} /\ {z} INTER {y:real^3}={} /\ {y,z} INTER {y1:real^3}={} /\ {y1,z} INTER {y:real^3}={}`) THEN RESA_TAC THEN REMOVE_THEN"MA1"(fun th-> MRESAL_TAC th[`e1:real^3->bool`;`y1:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`] THEN MRESAL_TAC th[`e2:real^3->bool`;`y:real^3`][SET_RULE`(A UNION B) INTER C=(A INTER C) UNION (B INTER C)/\ A INTER (B UNION C)=(A INTER B) UNION (A INTER C)`]) THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B= B INTER A`] THEN ASM_REWRITE_TAC[] THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y1:real^3`][aff] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN MRESAL_TAC (GEN_ALL AFF_INTER_AFF_GT_EQ_EMPTY)[`vec 0:real^3`;`z:real^3`;`y:real^3`][aff] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC THEN MRESA_TAC HALFLINE_SUBSET_AFFINE_HULL[`vec 0:real^3`;`z:real^3`] THEN MP_TAC(SET_RULE` affine hull {vec 0, z} INTER aff_gt {vec 0} {z, y1} = {} /\ affine hull {vec 0, z} INTER aff_gt {vec 0} {z, y} = {} /\ aff_ge {vec 0} {z} SUBSET affine hull {vec 0, z:real^3} ==> aff_gt {vec 0} {z, y} INTER aff_ge {vec 0} {z}={} /\ aff_ge {vec 0} {z} INTER aff_gt {vec 0} {z, y1}={}`) THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[SET_RULE`{B,C}={C,B}`] THEN ASM_REWRITE_TAC[SET_RULE`({} UNION aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION {}) UNION aff_ge {vec 0} {} UNION {} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {z} INTER aff_ge {vec 0} {z} = (aff_gt {vec 0} {y, z} INTER aff_ge {vec 0} {y1} UNION aff_ge {vec 0} {} UNION aff_ge {vec 0} {}) UNION aff_ge {vec 0} {z} `;] THEN MRESA_TAC th3[`vec 0:real^3`;`y1:real^3`;`z:real^3`;] THEN MRESAL_TAC Planarity.point_in_aff_ge_1_1[`vec 0:real^3`;`z:real^3`][IN_SING] THEN ASM_SIMP_TAC[AFF_GE_EQ_AFFINE_HULL;AFFINE_HULL_SING;IN_SING] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN SET_TAC[]; ASM_SIMP_TAC[] THEN REMOVE_THEN"THY6"(fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`i':num` THEN MP_TAC(th) THEN DISCH_THEN(LABEL_TAC"THY6")) THEN MRESA_TAC th3[`y:real^3`;`z:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MRESA_TAC th3[`y1:real^3`;`z1:real^3`;`vec 0:real^3`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={C,A,B}`] THEN RESA_TAC THEN MP_TAC(SET_RULE`~(y1=z1)/\ ~(y=z)/\ {y, z} INTER {y1, z1} = {y, z}==> {y1, z1:real^3} = {y, z}`) THEN RESA_TAC THEN SET_TAC[]; ASM_SIMP_TAC[]; REMOVE_THEN "MA1"(fun th-> MRESA_TAC th[`e2:real^3->bool`;`v':real^3`]) THEN ONCE_REWRITE_TAC[SET_RULE`A INTER B=B INTER A`] THEN ASM_REWRITE_TAC[]; ASM_SIMP_TAC[]; SUBGOAL_THEN`!i j. 1 <= i /\ i <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) /\ row i (vecmats l) = row j (vecmats (l:real^(M,3)finite_product)) ==> i = j` ASSUME_TAC; REPEAT STRIP_TAC THEN REMOVE_THEN "THY3"(fun th-> MRESAL_TAC th[`i:num`;`j:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0]) THEN DISJ_CASES_TAC(SET_RULE`~(i=j:num)\/ (i=j)`); MP_TAC(ARITH_RULE`i <= dimindex (:M)==> i <= dimindex (:M)-1 \/ i = dimindex (:M)`) THEN RESA_TAC; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`) THEN RESA_TAC; REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i:num`;`j:num`][ARITH_RULE`0<= i:num`]) THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN MP_TAC(ARITH_RULE`1<= i==> ~(i = 0)`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i:num`;`0:num`][ARITH_RULE`0<= i:num`]) THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN STRIP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A `]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`) THEN RESA_TAC THEN REMOVE_THEN"THYGIANG"MP_TAC THEN ASM_SIMP_TAC[IN_NUMSEG] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`]) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[]; SET_TAC[]; SUBGOAL_THEN`local_fan (V_SY (vecmats l),E_SY (vecmats l), F_SY(vecmats (l:real^(M,3)finite_product)))` ASSUME_TAC; ASM_REWRITE_TAC[local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN REPEAT STRIP_TAC; EXISTS_TAC`(row 1 (vecmats (l:real^(M,3)finite_product)), row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))` THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.ELMS_OF_HYPERMAP_HYP)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`] THEN STRIP_TAC; SIMP_TAC[darts_of_hyp;ord_pairs;E_SY;] THEN MATCH_MP_TAC(SET_RULE`A IN B ==> A IN B UNION C`) THEN REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC`row 1 (vecmats (l:real^(M,3)finite_product))` THEN EXISTS_TAC`row (SUC (1 MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN ASM_REWRITE_TAC[] THEN EXISTS_TAC`1` THEN ASM_REWRITE_TAC[ARITH_RULE`1<=1`; DIMINDEX_GE_1]; MATCH_MP_TAC FACE_HYP_FAN_SY THEN ASM_REWRITE_TAC[] THEN ASM_TAC THEN MESON_TAC[]; MRESA1_TAC (GEN_ALL DIH2K_FAN_HYP_SY)`l:real^(M,3)finite_product` THEN POP_ASSUM MP_TAC THEN FIND_ASSUM MP_TAC`2<k` THEN ONCE_REWRITE_TAC[ARITH_RULE`2= SUC 1`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE`SUC 1=2`] THEN RESA_TAC; POP_ASSUM (fun th-> MP_TAC th THEN ASM_REWRITE_TAC[local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN DISCH_TAC THEN ASSUME_TAC th) THEN ASM_REWRITE_TAC[] THEN SUBGOAL_THEN`!i u v w. 1<= i /\ i<= dimindex (:M) /\ row i (vecmats l)=u /\ row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))=v /\ (row (SUC ((SUC (i MOD dimindex (:M))) MOD dimindex (:M))) (vecmats l))=w ==> &0<= (v cross w) dot u` ASSUME_TAC; REPEAT STRIP_TAC THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\ SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; SUBGOAL_THEN`1 <= SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) /\ SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`SUC (i MOD dimindex (:M)):num`;`dimindex (:M):num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`(SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M)))` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2")) THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row i ((v:num->real^3^M) n))`;`v':real^3`;`w:real^3`;`u:real^3`] THEN SUBGOAL_THEN`eventually (\x. &0 <= drop ((lift o (\n. (row (SUC (i MOD dimindex (:M))) (v n) cross row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)) dot row i ((v:num->real^3^M) n))) x)) sequentially` ASSUME_TAC; REWRITE_TAC[EVENTUALLY_SEQUENTIALLY;o_DEF;LIFT_DROP] THEN EXISTS_TAC`0` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[convex_local_fan;] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY30") THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN ASSUME_TAC th) THEN SUBGOAL_THEN`row (SUC (i MOD dimindex (:M))) (v n), row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n) IN F_SY ((v:num->real^3^M) n)`ASSUME_TAC; REWRITE_TAC[F_SY;IN_ELIM_THM] THEN EXISTS_TAC`(SUC (i MOD dimindex (:M)))` THEN ASM_REWRITE_TAC[]; STRIP_TAC THEN POP_ASSUM(fun th-> MRESA1_TAC th` row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n), row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)`) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n), row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)`] THEN FIND_ASSUM MP_TAC`1<k` THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`] THEN RESA_TAC THEN SUBGOAL_THEN `(!i1 j. 1 <= i1 /\ i1 <= dimindex (:M) /\ 1 <= j /\ j <= dimindex (:M) /\ row i1 (v n) = row j ((v:num->real^3^M) n) ==> i1 = j)` ASSUME_TAC; REPEAT STRIP_TAC THEN REMOVE_THEN "THY30"(fun th-> MRESAL_TAC th[`i1:num`;`j:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0]) THEN DISJ_CASES_TAC(SET_RULE`~(i1=j:num)\/ (i1=j)`); MP_TAC(ARITH_RULE`i1 <= dimindex (:M)==> i1 <= dimindex (:M)-1 \/ i1 = dimindex (:M)`) THEN RESA_TAC; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`) THEN RESA_TAC; REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i1:num`;`j:num`][ARITH_RULE`0<= i:num`]) THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`] THEN MP_TAC(ARITH_RULE`1<= i1==> ~(i1 = 0)`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i1:num`;`0:num`][ARITH_RULE`0<= i1:num`]) THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(ARITH_RULE`j <= dimindex (:M)==> j <= dimindex (:M)-1 \/ j = dimindex (:M)`) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN STRIP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A `]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= j==> ~(j = 0)`) THEN RESA_TAC THEN REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`j:num`;`0:num`][ARITH_RULE`0<= i:num`]) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[]; ASM_MESON_TAC[]; MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i:num`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (i) ((v:num->real^3^M) n)`;`matvec((v:num-> real^3^M) n)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`;VECMATS_MATVEC_ID] THEN STRIP_TAC THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`matvec ((v:num->real^3^M) n)`][VECMATS_MATVEC_ID] THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`(SUC (i MOD dimindex (:M)))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`;`matvec ((v:num->real^3^M) n)`][VECMATS_MATVEC_ID] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_ge_fan[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) ((v:num->real^3^M) n)`][azim;VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN RESA_TAC; MRESAL_TAC LIM_DROP_LBOUND[`sequentially`;`lift o (\n. (row (SUC (i MOD dimindex (:M))) (v n) cross row (SUC (SUC (i MOD dimindex (:M)) MOD dimindex (:M))) (v n)) dot row i ((v:num->real^3^M) n))`;`lift ((v' cross w:real^3) dot u)`;`&0`][TRIVIAL_LIMIT_SEQUENTIALLY;LIFT_DROP]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY30") THEN GEN_TAC THEN STRIP_TAC THEN SUBGOAL_THEN`azim_in_fan x' (E_SY (vecmats (l:real^(M,3)finite_product))) <= pi` ASSUME_TAC; POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[F_SY;IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`] THEN ABBREV_TAC`u1=row i (vecmats (l:real^(M,3)finite_product))` THEN ABBREV_TAC`v1=row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))` THEN FIND_ASSUM MP_TAC`1<k` THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`) THEN RESA_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO] THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`u1:real^3`;`v1:real^3`;`(row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN REMOVE_THEN"THY30"(fun th-> MRESAL_TAC th [`k:num`;`(row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`u1:real^3`;`v1:real^3`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]) THEN MP_TAC(REAL_ARITH`&0 <= (u1 cross v1) dot row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)) ==> &0 < (u1 cross v1) dot row (dimindex (:M)) (vecmats l)\/ (u1 cross v1) dot row (dimindex (:M)) (vecmats l)= &0`) THEN RESA_TAC; MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`1:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`] THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`dimindex (:M):num`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B}={B,A}`] THEN RESA_TAC THEN REMOVE_ASSUM_TAC THEN MRESA_TAC (GEN_ALL Local_lemmas.MIXED_PROD_POS_IMP_RANGE_AZIM)[`u1:real^3`;`v1:real^3`;`(row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{C,A,B}={C,B,A}`] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[Local_lemmas.CROSS_DOT_COPLANAR] THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`1:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`] THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`dimindex (:M):num`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN MRESAL_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u1:real^3`;`v1:real^3`;`row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product))`][PI_POS_LE;REAL_ARITH`a<=a`]; MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)`) THEN RESA_TAC THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`] THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i-1:num`;`u1:real^3`;`v1:real^3`;`(row (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN POP_ASSUM MP_TAC THEN REMOVE_THEN"THY30"(fun th-> MRESAL_TAC th [`i-1:num`;`(row (i-1) (vecmats (l:real^(M,3)finite_product)))`;`u1:real^3`;`v1:real^3`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN STRIP_TAC THEN STRIP_TAC THEN MP_TAC(REAL_ARITH`&0 <= (u1 cross v1) dot row (i-1) (vecmats (l:real^(M,3)finite_product)) ==> &0 < (u1 cross v1) dot row (i-1) (vecmats l)\/ (u1 cross v1) dot row (i-1) (vecmats l)= &0`) THEN RESA_TAC; MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`] THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i-1:num`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN STRIP_TAC THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`] THEN REMOVE_ASSUM_TAC THEN MRESA_TAC (GEN_ALL Local_lemmas.MIXED_PROD_POS_IMP_RANGE_AZIM)[`u1:real^3`;`v1:real^3`;`(row (i-1) (vecmats (l:real^(M,3)finite_product)))`;] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{C,A,B}={C,B,A}`] THEN RESA_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN REWRITE_TAC[Local_lemmas.CROSS_DOT_COPLANAR] THEN MRESA_TAC (GEN_ALL EDGE_IN_E_SY)[`i:num`;`u1:real^3`;`v1:real^3`;`(l:real^(M,3)finite_product)`] THEN MRESAL_TAC (GEN_ALL EDGE_IN_E_SY)[`i-1:num`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`(l:real^(M,3)finite_product)`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN STRIP_TAC THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`v1:real^3`;`u1:real^3`] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`u1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN STRIP_TAC THEN MRESAL_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`u1:real^3`;`v1:real^3`;`row (i-1) (vecmats (l:real^(M,3)finite_product))`][PI_POS_LE;REAL_ARITH`a<=a`]; SUBGOAL_THEN`!i j u v w. 1<= i /\ i<= dimindex (:M) /\ 1<= j /\ j<= dimindex (:M) /\ row i (vecmats l)=u /\ row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))=v /\ row j (vecmats l)=w ==> &0<= (u cross v) dot w` ASSUME_TAC; REPEAT STRIP_TAC THEN SUBGOAL_THEN`1 <= SUC (i MOD dimindex (:M)) /\ SUC (i MOD dimindex (:M)) <= dimindex (:M)` ASSUME_TAC; ASM_REWRITE_TAC[ARITH_RULE`1<= SUC a`] THEN MRESAL_TAC DIVISION[`i:num`;`dimindex (:M):num`][DIMINDEX_NONZERO] THEN POP_ASSUM MP_TAC THEN ARITH_TAC; REMOVE_THEN "YEU2" (fun th-> MRESA1_TAC th`i:num` THEN MRESA1_TAC th`SUC (i MOD dimindex (:M))` THEN MRESA1_TAC th`j:num` THEN MP_TAC th THEN DISCH_THEN(LABEL_TAC"YEU2")) THEN MRESA_TAC (GEN_ALL CROSS_DOT_SEQUENTIALLY)[`(\n. row i ((v:num->real^3^M) n))`;`(\n. row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`(\n. row j ((v:num->real^3^M) n))`;`u:real^3`;`v':real^3`;`w:real^3`] THEN SUBGOAL_THEN`eventually (\x. &0 <= drop ((lift o (\n. (row i (v n) cross row (SUC (i MOD dimindex (:M))) (v n)) dot row j ((v:num->real^3^M) n))) x)) sequentially` ASSUME_TAC; REWRITE_TAC[EVENTUALLY_SEQUENTIALLY;o_DEF;LIFT_DROP] THEN EXISTS_TAC`0` THEN REPEAT STRIP_TAC THEN REMOVE_THEN "THY1"(fun th-> MRESA1_TAC th`n:num`) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REWRITE_TAC[convex_local_fan;] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY31") THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[local_fan] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN STRIP_TAC THEN ASSUME_TAC th) THEN SUBGOAL_THEN`row i (v n), row (SUC (i MOD dimindex (:M))) (v n) IN F_SY ((v:num->real^3^M) n)`ASSUME_TAC; REWRITE_TAC[F_SY;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; SUBGOAL_THEN`row j ((v:num->real^3^M) n) IN V_SY((v:num->real^3^M) n)` ASSUME_TAC; REWRITE_TAC[V_SY;rows;IN_ELIM_THM] THEN EXISTS_TAC`j:num` THEN ASM_REWRITE_TAC[]; STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL1_TAC th` row i ((v:num->real^3^M) n), row (SUC (i MOD dimindex (:M))) (v n)`[SUBSET;IN_ELIM_THM]) THEN POP_ASSUM(fun th-> MRESAL1_TAC th` row j ((v:num->real^3^M) n)`[SUBSET;IN_ELIM_THM]) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n), row (SUC (i MOD dimindex (:M))) (v n)`] THEN MRESA_TAC (GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN)[`V_SY (((v:num->real^3^M) n))`;`F_SY (((v:num->real^3^M) n))`;`E_SY ( ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n), row (SUC (i MOD dimindex (:M))) (v n)`] THEN FIND_ASSUM MP_TAC`1<k` THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`] THEN RESA_TAC THEN SUBGOAL_THEN `(!i1 j1. 1 <= i1 /\ i1 <= dimindex (:M) /\ 1 <= j1 /\ j1 <= dimindex (:M) /\ row i1 (v n) = row j1 ((v:num->real^3^M) n) ==> i1 = j1)` ASSUME_TAC; REPEAT STRIP_TAC THEN REMOVE_THEN "THY31"(fun th-> MRESAL_TAC th[`i1:num`;`j1:num`][VECTOR_ARITH`A-A= vec 0`;NORM_0]) THEN DISJ_CASES_TAC(SET_RULE`~(i1=j1:num)\/ (i1=j1)`); MP_TAC(ARITH_RULE`i1 <= dimindex (:M)==> i1 <= dimindex (:M)-1 \/ i1 = dimindex (:M)`) THEN RESA_TAC; MP_TAC(ARITH_RULE`j1 <= dimindex (:M)==> j1 <= dimindex (:M)-1 \/ j1 = dimindex (:M)`) THEN RESA_TAC; REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i1:num`;`j1:num`][ARITH_RULE`0<= i:num`]) THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`i1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`] THEN MP_TAC(ARITH_RULE`1<= i1==> ~(i1 = 0)`) THEN RESA_TAC THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`i1:num`;`0:num`][ARITH_RULE`0<= i1:num`]) THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`i1:num`;`k:num`;][IN_NUMSEG;ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; MP_TAC(ARITH_RULE`j1 <= dimindex (:M)==> j1 <= dimindex (:M)-1 \/ j1 = dimindex (:M)`) THEN RESA_TAC; POP_ASSUM MP_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN STRIP_TAC THEN MRESAL_TAC MOD_MULT[`k:num`;`1`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A`] THEN MRESA_TAC (GEN_ALL POWER_MOD_FUN)[`k:num`;`k:num`;`k:num`] THEN MRESAL_TAC MOD_MULT[`k:num`;`2`][DIMINDEX_NONZERO;ARITH_RULE`A*1=A/\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`] THEN REMOVE_THEN "THYGIANG2" MP_TAC THEN REWRITE_TAC[constraint_system] THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A `]) THEN STRIP_TAC THEN POP_ASSUM(fun th-> MRESAL_TAC th[`j1:num`;`k:num`;][ARITH_RULE`0<=a:num/\ A+0=A /\ dimindex (:M) + dimindex (:M)= dimindex (:M) *2`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= j1==> ~(j1 = 0)`) THEN RESA_TAC THEN REMOVE_THEN"THYGIANG"MP_TAC THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`j1:num`] THEN MRESA_TAC IN_NUMSEG[`0`;`k-1:num`;`0:num`] THEN STRIP_TAC THEN POP_ASSUM (fun th-> MRESAL_TAC th[`j1:num`;`0:num`][ARITH_RULE`0<= i:num`]) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN MESON_TAC[]; ASM_MESON_TAC[]; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY32") THEN REWRITE_TAC[REAL_ARITH`A<=B <=> A=B\/ A< B`] THEN STRIP_TAC; MRESAL_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE (row i (v n)) (E_SY (v n))) (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)))`;`(row i ((v:num->real^3^M) n))`;`(row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`vec 0:real^3`][IN_ELIM_THM;REAL_ARITH`A=B\/ A< B<=> A<=B`;VECTOR_ARITH`A- vec 0=A`] THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN SUBGOAL_THEN`{row i (v n), row (SUC (i MOD dimindex (:M))) (v n)} IN E_SY ((v:num->real^3^M) n)`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`] THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;] THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`row i ((v:num->real^3^M) n)`] THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN STRIP_TAC THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`] THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))) ==> azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))) = &0 \/ &0< azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)))`) THEN REWRITE_TAC[azim] THEN STRIP_TAC; MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY ((v:num->real^3^M) n)`;`E_SY ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th; SET_RULE`{A,A}={A}`]) THEN STRIP_TAC THEN MRESAL_TAC AFF_GE_SUBSET_AFFINE_HULL[`{vec 0,row i ((v:num->real^3^M) n)}`;`{(row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))}`][GSYM aff] THEN MP_TAC(SET_RULE`row j (v n) IN aff_ge {vec 0, row i (v n)} {row (SUC (i MOD dimindex (:M))) (v n)} /\ aff_ge {vec 0, row i (v n)} {row (SUC (i MOD dimindex (:M))) (v n)} SUBSET aff ({vec 0, row i (v n)} UNION {row (SUC (i MOD dimindex (:M))) (v n)}) ==> row j ((v:num->real^3^M) n) IN aff ({vec 0, row i (v n)} UNION {row (SUC (i MOD dimindex (:M))) (v n)})`) THEN ASM_REWRITE_TAC[SET_RULE` {A,B}UNION{C}={A,B,C}`] THEN MRESAL_TAC Conforming.aff_3_rep_cross_dot[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`] [IN_ELIM_THM;VECTOR_ARITH`A- vec 0=A`] THEN RESA_TAC; MP_TAC(REAL_ARITH` &0<azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))) /\ azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))) < pi ==> ~(azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))) = &0 \/ azim (vec 0) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n)) (sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) (v n))) = pi)`) THEN RESA_TAC THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`] THEN STRIP_TAC THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`row i ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM]) THEN STRIP_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`][VECTOR_ARITH`A- vec 0=A`] THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i ((v:num->real^3^M) n)`;`row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n)`;`sigma_fan (vec 0) (V_SY (v n)) (E_SY (v n)) (row i (v n)) (row (SUC (i MOD dimindex (:M))) ((v:num->real^3^M) n))`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN REAL_ARITH_TAC; MRESAL_TAC LIM_DROP_LBOUND[`sequentially`;`lift o (\n. (row i (v n) cross row (SUC (i MOD dimindex (:M))) (v n))dot row j ((v:num->real^3^M) n))`;`lift ((u cross v':real^3) dot w)`;`&0`][TRIVIAL_LIMIT_SEQUENTIALLY;LIFT_DROP]; ASM_REWRITE_TAC[] THEN POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[F_SY;IN_ELIM_THM] THEN STRIP_TAC THEN ASSUME_TAC th) THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_DETERMINE_AZIM_IN_FA)[`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`] THEN MRESA_TAC(GEN_ALL Local_lemmas.DETERMINE_WEDGE_IN_FAN) [`V_SY (vecmats (l:real^(M,3)finite_product))`;`F_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`x':real^3#real^3`] THEN REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN REWRITE_TAC[REAL_ARITH`A<=B <=> A=B\/ A< B`] THEN STRIP_TAC; DISCH_THEN(LABEL_TAC"THY31") THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows] THEN STRIP_TAC THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL Local_lemmas.AZIM_PI_WEDGE_GE_CROSS_DOT)[`(azim_cycle (EE (row i (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product)))) (vec 0) (row i (vecmats l)) (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))))`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`vec 0:real^3`][IN_ELIM_THM;REAL_ARITH`A=B\/ A< B<=> A<=B`;VECTOR_ARITH`A- vec 0=A`] THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i:num`;`i':num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`]) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; POP_ASSUM MP_TAC THEN DISCH_THEN(LABEL_TAC"THY32") THEN DISCH_THEN(LABEL_TAC"THY31") THEN GEN_TAC THEN STRIP_TAC THEN POP_ASSUM(fun th-> MP_TAC th THEN REWRITE_TAC[V_SY;IN_ELIM_THM;rows] THEN STRIP_TAC THEN ASSUME_TAC th) THEN SUBGOAL_THEN`{row i (vecmats (l:real^(M,3)finite_product)), row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))} IN E_SY (vecmats (l:real^(M,3)finite_product))`ASSUME_TAC; REWRITE_TAC[E_SY;IN_ELIM_THM] THEN EXISTS_TAC`i:num` THEN ASM_REWRITE_TAC[]; MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`] THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.AZIM_CYCLE_EQ_SIGMA_FAN)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;] THEN MRESA_TAC(sigma_fan_in_set_of_edge)[`vec 0:real^3`;`V_SY (vecmats (l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`row i (vecmats (l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product))`;] THEN MRESA_TAC remark1_fan[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats (l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats (l:real^(M,3)finite_product))) (E_SY (vecmats (l:real^(M,3)finite_product))) (row i (vecmats (l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`] THEN POP_ASSUM MP_TAC THEN RESA_TAC THEN REMOVE_THEN "THY32" MP_TAC THEN RESA_TAC THEN MRESA_TAC(GEN_ALL Local_lemmas.WEDGE_GE_EQ_AFF_GE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`] THEN MP_TAC(REAL_ARITH`&0<= azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) ==> azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/ &0< azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))))`) THEN REWRITE_TAC[azim] THEN STRIP_TAC; MRESA_TAC Fan.UNIQUE_AZIM_0_POINT_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`] THEN MRESA_TAC(GEN_ALL Wrgcvdr_cizmrrh.FAN_IMP_EE_EQ_SET_OF_EDGE)[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`] THEN MRESA_TAC (GEN_ALL Local_lemmas.LOFA_CARD_EE_V_1)[`F_SY (vecmats(l:real^(M,3)finite_product))`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`] THEN POP_ASSUM MP_TAC THEN DISJ_CASES_TAC(SET_RULE`set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={row (SUC (i MOD dimindex (:M))) (vecmats l)} \/ ~(set_of_edge (row i (vecmats l)) (V_SY (vecmats l)) (E_SY (vecmats l)) ={(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))})`); ASM_REWRITE_TAC[] THEN SIMP_TAC[HAS_SIZE; CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY; IN_INSERT; NOT_IN_EMPTY] THEN ARITH_TAC; MRESA_TAC SIGMA_FAN[`vec 0:real^3`;`V_SY (vecmats(l:real^(M,3)finite_product))`;`E_SY (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`] THEN REMOVE_ASSUM_TAC THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`A=B<=>B=A`] THEN REMOVE_ASSUM_TAC THEN REMOVE_ASSUM_TAC THEN POP_ASSUM (fun th-> REWRITE_TAC[SYM th]); MP_TAC(REAL_ARITH` &0<azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) /\ azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) < pi ==> ~(azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = &0 \/ azim (vec 0) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))) (sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))) = pi)`) THEN RESA_TAC THEN MRESA_TAC AZIM_EQ_0_PI_EQ_COPLANAR[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`] THEN STRIP_TAC THEN MRESA_TAC( GEN_ALL Nkezbfc_local.inter_aff_ge_3_1_is_aff_ge_2_2)[`vec 0:real^3`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`] THEN POP_ASSUM(fun th-> REWRITE_TAC[SYM th;INTER;IN_ELIM_THM]) THEN STRIP_TAC; MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`] THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,C,B,D}`] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i:num`;`i':num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`]) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MRESAL_TAC Planarity.cross_dot_fully_surrounded_fan[`vec 0:real^3`;`row i (vecmats(l:real^(M,3)finite_product))`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`][VECTOR_ARITH`A- vec 0=A`] THEN MRESAL_TAC Nkezbfc_local.aff_ge_3_1_rep_cross_dot [`vec 0:real^3`;`sigma_fan (vec 0) (V_SY (vecmats(l:real^(M,3)finite_product))) (E_SY (vecmats(l:real^(M,3)finite_product))) (row i (vecmats(l:real^(M,3)finite_product))) (row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product)))`;`row i (vecmats(l:real^(M,3)finite_product))`;`row (SUC (i MOD dimindex (:M))) (vecmats(l:real^(M,3)finite_product))`;][VECTOR_ARITH`A- vec 0=A`] THEN POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C,D}={A,D,C,B}`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN RESA_TAC THEN ONCE_REWRITE_TAC[SET_RULE`{A,B,C}={A,C,B}`] THEN ASM_REWRITE_TAC[IN_ELIM_THM] THEN FIND_ASSUM MP_TAC`1<k` THEN ONCE_REWRITE_TAC[ARITH_RULE`1= SUC 0`] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[ARITH_RULE`SUC 0=1`] THEN RESA_TAC THEN MP_TAC(ARITH_RULE`1<= i==> i=1 \/ 1<= i-1`) THEN RESA_TAC; POP_ASSUM (fun th-> SUBST_ALL_TAC(th)) THEN MRESAL_TAC MOD_MULT[`dimindex (:M)`;`1`][ARITH_RULE`k*1=k`;ARITH_RULE`SUC 0=1`;DIMINDEX_NONZERO] THEN MRESA_TAC MOD_LT[`1:num`;`dimindex (:M)`] THEN POP_ASSUM (fun th-> SUBST_ALL_TAC(th) THEN ASSUME_TAC th) THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`k:num`;`row 1 (vecmats (l:real^(M,3)finite_product))`;`row (SUC 1) (vecmats (l:real^(M,3)finite_product))`;`(row (dimindex (:M)) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN REMOVE_THEN"THY31"(fun th-> MRESAL_TAC th[`k:num`;`i':num`;`row (dimindex (:M)) (vecmats(l:real^(M,3)finite_product))`;`(row 1 (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`][ARITH_RULE`dimindex (:M) <= dimindex (:M) /\ SUC 0=1`]) THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC; MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)`) THEN RESA_TAC THEN MRESAL_TAC MOD_LT[`i-1:num`;`dimindex (:M):num`][ARITH_RULE`0<1`] THEN MRESAL_TAC(GEN_ALL AZIM_CYCLE_EQ1)[`i-1:num`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row (SUC (i MOD dimindex (:M))) (vecmats (l:real^(M,3)finite_product)))`;`(row (i-1) (vecmats (l:real^(M,3)finite_product)))`;`l:real^(M,3)finite_product`][ARITH_RULE`SUC 0=1/\ dimindex (:M) <= dimindex (:M)`] THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN RESA_TAC THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN ONCE_REWRITE_TAC[CROSS_TRIPLE] THEN REMOVE_THEN"THY31"(fun th-> MRESA_TAC th[`i-1:num`;`i':num`;`row (i - 1) (vecmats(l:real^(M,3)finite_product))`;`(row i (vecmats (l:real^(M,3)finite_product)))`;`(row i' (vecmats (l:real^(M,3)finite_product)))`]) THEN POP_ASSUM MP_TAC THEN MP_TAC(ARITH_RULE`1<= i /\ i<= dimindex (:M) ==> i-1 < dimindex (:M)/\ i-1 <= dimindex (:M)/\ SUC (i-1)=i`) THEN RESA_TAC THEN POP_ASSUM(fun th-> ONCE_REWRITE_TAC[th]) THEN REAL_ARITH_TAC ]);;
let BOUNDED_SY=
prove(` stable_system k d (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 1< k /\ 2<k ==> bounded {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v /\ CONDITION2_SY v }`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC BOUNDED_SUBSET THEN EXISTS_TAC`{matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) }` THEN MP_TAC COMPACT_BALL_ANNULUS_MATVEC THEN SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED] THEN RESA_TAC THEN REWRITE_TAC[SUBSET;IN_ELIM_THM] THEN SET_TAC[]);;
let WJSCPRO= 
prove (` stable_system k (d:real) (0..k-1) a b J (\i. ((1+i):num MOD k)) /\k= dimindex(:M) /\ 2<k ==> compact {matvec(v:real^3^M) | (!i. 1<=i /\ i <= dimindex(:M)==> row i v IN ball_annulus) /\ CONDITION1_SY a b v /\ CONDITION2_SY v }`,
SIMP_TAC[COMPACT_EQ_BOUNDED_CLOSED; BOUNDED_SY; CLOSED_SY;] THEN REPEAT STRIP_TAC THEN MP_TAC(ARITH_RULE`2<k ==> 1<k`) THEN RESA_TAC THENL[ MRESA_TAC (GEN_ALL BOUNDED_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]; MRESA_TAC (GEN_ALL CLOSED_SY)[`d:real`;`J:(num->bool)->bool`;`k:num`;`a:num#num->real`;`b:num#num->real`;]]);;
end;;