(* ========================================================================= *)
(* File Name: z_Delete_Theorems.ml		                             *)
(*---------------------------------------------------------------------------*)
(* Description: Z_DELETE FUNCTION THEOREMS     		                     *)
(*                                                                           *)
(*                                                                           *)
(*     (c) Author :  Adnan Rashid					     *)
(*      Co-Author :  Sohaib Ahmad					     *)
(*      Co-Author :  Dr. Osman Hasan			             	     *)
(* 	    SYSTEM ANALYSIS & VERIFICATION (SAVe) LAB                        *)
(*	    National University of Sciences and Technology (NUST), PAKISTAN  *)
(* NOTE: This Script is written in HOL Light		               	     *)
(*                                                                           *)
(* ========================================================================= *)
		
(* ========================================================================= *)
(* Theorems List			  			             *)
(*---------------------------------------------------------------------------*)
(*   zsyn_delet_LENGTH_THM;							     *)
(*   zsyn_delet_MEM_THM;				                             *)
(*   zsyn_delet_ASSOC_THM;							     *)
(*   zsyn_delet_NOT_MEM_THM;							     *)
(*	    This file needs Formalization.ml to be uploaded first   	     *)
(*	    This file needs Supporting_Theorems.ml to be uploaded first      *)
(*	    This file needs Delete_Theorems.ml to be uploaded first   	     *)
(*---------------------------------------------------------------------------*)
 
(*---------------------------------------------------------------------------*)
(* 			      zsyn_delet_LENGTH_THM		    		     *)
(*---------------------------------------------------------------------------*)

g `!(x:num) y (l:(((A)list) list)).
    (1 < LENGTH l) /\ (x < LENGTH l) /\ (y < LENGTH l) /\ ~(x = y)
    ==> (LENGTH (zsyn_delet l x y) = LENGTH l - 2)`;;

e (INDUCT_TAC);;
e (SIMP_TAC [zsyn_delet; delet]);;
e (REPEAT STRIP_TAC);;
e (COND_CASES_TAC);;

(*- BASE CASE--*)

e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(!y. (TL (delet (l:(((A)list) list)) y)) =(delet (TL l) (y - 1)))` ASSUME_TAC);;
      e (INDUCT_TAC);;
      e (ASM_SIMP_TAC [delet; TL]);;
      e (SUBGOAL_THEN `(0 - 1) = 0` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

      e (REWRITE_TAC [delet; HD; TL]);;
      e (SUBGOAL_THEN `SUC y' - 1 = y'` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `LENGTH (delet (TL (l:(((A)list) list))) (y - 1)) = (LENGTH (TL l) - 1)` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC LENGTH_TL);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;

(*- SUC CASE--*)

e (REPEAT STRIP_TAC);;
e (SIMP_TAC [zsyn_delet; delet]);;
e (COND_CASES_TAC);;
e (SUBGOAL_THEN `LENGTH (delet (CONS (HD l) (delet (TL (l:(((A)list) list))) x)) y) = (LENGTH (CONS (HD l) (delet (TL l) x)) - 1)` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (SIMP_TAC [LENGTH]);;
      e (SUBGOAL_THEN `LENGTH (delet (TL (l:(((A)list) list))) x) = (LENGTH (TL l) - 1)` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC[]);;
e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC LENGTH_TL);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM MP_TAC);;
e (REWRITE_TAC [LENGTH]);;
e (SUBGOAL_THEN `(SUC (LENGTH (delet (TL (l:(((A)list) list))) x)) - 1) = (LENGTH (delet (TL l) x))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `~NULL (l:(((A)list) list))` ASSUME_TAC);;
      e (SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(l:(((A)list) list) = (CONS (HD l) (TL l)))` ASSUME_TAC);;
      e (ASM_SIMP_TAC [LENGTH_NOT_NULL]);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (ASM_SIMP_TAC [CONS_NOT_NULL]);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SIMP_TAC [LENGTH]);;
e (SIMP_TAC [TL]);;
e (SIMP_TAC [ADD1]);;
e (SUBGOAL_THEN `((LENGTH (TL (l:(((A)list) list))) + 1) - 2) = (LENGTH (TL l) - 1)` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SIMP_TAC [TL]);;
e (MATCH_MP_TAC delet_LENGTH_THM);;
e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC LENGTH_TL);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;
e (POP_ASSUM MP_TAC);;
e (SUBGOAL_THEN `~(SUC x > y) = (SUC x <= y)` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(SUC x <= y) = ((SUC x < y) \/ (SUC x = y))` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (SIMP_TAC [GSYM delet]);;
e (SUBGOAL_THEN `LENGTH (delet (delet (l:(((A)list) list)) y) (SUC x)) = LENGTH (delet l y) - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (SUBGOAL_THEN `LENGTH (delet l y) = LENGTH (l:(((A)list) list)) - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) y) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (ARITH_TAC);;

let zsyn_delet_LENGTH_THM = top_thm ();;

(*---------------------------------------------------------------------------*)
(*				zsyn_delet_MEM_THM				     *)
(*---------------------------------------------------------------------------*)

g `!(x:num) a (y:num) (l:(((A)list) list)).
    1 < LENGTH l /\ (x < LENGTH l) /\ (y < LENGTH l) /\
    ~(x = y) /\ MEM a (zsyn_delet l x y) 
    ==> MEM a l`;;

e (INDUCT_TAC);;
e (SIMP_TAC [zsyn_delet; delet]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `0 < y` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `~(0 = y)`);;
e (DISCH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (UNDISCH_TAC `MEM a (if 0 > y then delet (TL (l:(((A)list) list))) y else TL (delet l y))`);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(!y. (TL (delet (l:(((A)list) list)) y)) =(delet (TL l) (y - 1)))` ASSUME_TAC);;
      e (INDUCT_TAC);;
      e (ASM_SIMP_TAC [delet; TL]);;
      e (SUBGOAL_THEN `(0 - 1) = 0` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

      e (REWRITE_TAC [delet; HD; TL]);;
      e (SUBGOAL_THEN `SUC y' - 1 = y'` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

e (ASM_SIMP_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (SUBGOAL_THEN `(y - 1) < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(l:(((A)list) list) = (CONS (HD l) (TL l)))` ASSUME_TAC);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (MATCH_MP_TAC CONS_NOT_NULL);;
      e (ASM_SIMP_TAC [GSYM LENGTH_NOT_NULL]);;

e (ONCE_ASM_REWRITE_TAC []);;
e (ASM_CASES_TAC `a = HD (l:(((A)list) list))`);;
      e (REWRITE_TAC [MEM]);;
      e (DISJ1_TAC);;
      e (ASM_REWRITE_TAC []);;

      e (SIMP_TAC [MEM; HD; TL]);;
      e (DISJ2_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `y - 1`);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

(*---Step Case---*)

e (REPEAT STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (UNDISCH_TAC `!a y (l:(((A)list) list)).
          1 < LENGTH l /\
          x < LENGTH l /\
          y < LENGTH l /\
          ~(x = y) /\
          MEM a (zsyn_delet l x y)
          ==> MEM a l`);;
e (SIMP_TAC [zsyn_delet; delet]);;
e (STRIP_TAC);;
e (COND_CASES_TAC);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `MEM a (CONS (HD l) (delet (TL (l:(((A)list) list))) x))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `y:num`);;
      e (ASM_REWRITE_TAC [LENGTH]);;
      e (SUBGOAL_THEN `(LENGTH (delet (TL (l:(((A)list) list))) x)) = LENGTH (TL l) - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
	    e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
	          e (MATCH_MP_TAC LENGTH_TL);;
      		  e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `~NULL (l:(((A)list) list))` ASSUME_TAC);;
      e (SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(l:(((A)list) list) = (CONS (HD l) (TL l)))` ASSUME_TAC);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (MATCH_MP_TAC CONS_NOT_NULL);;
      e (ASM_SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (UNDISCH_TAC `MEM a (CONS (HD (l:(((A)list) list))) (delet (TL l) x))`);;
e (ASM_SIMP_TAC [MEM]);;
e (STRIP_TAC);;
e (DISJ1_TAC);;
e (ASM_REWRITE_TAC []);;

e (ASM_CASES_TAC `a = HD (l:(((A)list) list))`);;
      e (DISJ1_TAC);;
      e (ASM_REWRITE_TAC []);;

      e (DISJ2_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `x:num`);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;


e (DISCH_TAC);;
e (UNDISCH_TAC `~(SUC x > y)`);;
e (SUBGOAL_THEN `~(SUC x > y) = (SUC x <= y)` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(SUC x <= y) = ((SUC x < y) \/ (SUC x = y))` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC [MEM]);;
e (STRIP_TAC);;
e (DISCH_TAC);;
e (ASM_REWRITE_TAC []);;
e (MATCH_MP_TAC delet_MEM_THM);;
e (EXISTS_TAC `y:num`);;
e (SUBGOAL_THEN `(LENGTH (delet ((l:(((A)list) list))) y)) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (ASM_REWRITE_TAC []);;

e (SUBGOAL_THEN `~NULL (delet (l:(((A)list) list)) y)` ASSUME_TAC);;
      e (ASM_SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(delet (l:(((A)list) list)) y = (CONS (HD (delet l y)) (TL (delet l y))))` ASSUME_TAC);;
      e (SIMP_TAC []);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (MATCH_MP_TAC NOT_NULL_IMP_CONS);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (ASM_SIMP_TAC [MEM; HD; TL]);;
e (DISCH_TAC);;


e (SUBGOAL_THEN `(!y. (TL (delet (l:(((A)list) list)) y)) =(delet (TL l) (y - 1)))` ASSUME_TAC);;
      e (INDUCT_TAC);;
      e (ASM_SIMP_TAC [delet; TL]);;
      e (SUBGOAL_THEN `(0 - 1) = 0` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

      e (REWRITE_TAC [delet; HD; TL]);;
      e (SUBGOAL_THEN `SUC y' - 1 = y'` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC [delet]);;

e (UNDISCH_TAC `MEM a (delet (TL (delet (l:(((A)list) list)) y)) x)`);;
e (ASM_SIMP_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (SUBGOAL_THEN `MEM a (delet (TL (l:(((A)list) list))) (y - 1))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `x:num`);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `(LENGTH (delet (TL (l:(((A)list) list))) (y - 1))) = LENGTH (TL l) - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
	    e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
	          e (MATCH_MP_TAC LENGTH_TL);;
      		  e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `~NULL (l:(((A)list) list))` ASSUME_TAC);;
      e (SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(l:(((A)list) list) = (CONS (HD l) (TL l)))` ASSUME_TAC);;
      e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      e (MATCH_MP_TAC CONS_NOT_NULL);;
      e (ASM_SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SIMP_TAC [MEM]);;
e (ASM_CASES_TAC `a = HD (l:(((A)list) list))`);;
      e (DISJ1_TAC);;
      e (ASM_REWRITE_TAC []);;

      e (DISJ2_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `y - 1`);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

let zsyn_delet_MEM_THM = top_thm ();;

(*---------------------------------------------------------------------------*)
(*				zsyn_delet_ASSOC_THM				     *)
(*---------------------------------------------------------------------------*)

g `!x (e:(((A)list) list)) (y:num) (l:(((A)list) list)).
     1 < LENGTH l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ ~(x = y)
     ==> (zsyn_delet (APPEND l e) x y = (APPEND (zsyn_delet l x y) e))`;;

e (INDUCT_TAC);;
e (REPEAT STRIP_TAC);;
e (ASM_SIMP_TAC [zsyn_delet; delet]);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(delet (APPEND l e) y) = (APPEND (delet (l:(((A)list) list)) y) (e:(((A)list) list)))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (ASM_REWRITE_TAC []);;

e (ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN `!L M. (0 < LENGTH L) ==> ((TL (APPEND (L:(((A)list) list)) M)) = (APPEND (TL L) (M:(((A)list) list))))` ASSUME_TAC);;
      e (LIST_INDUCT_TAC);;
      e (ASM_SIMP_TAC [LENGTH]);;
      e (ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (ASM_SIMP_TAC [APPEND; TL]);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `(delet (l:(((A)list) list)) y)`));;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (SUBGOAL_THEN `0 < LENGTH (delet (l:(((A)list) list)) y)` ASSUME_TAC);;
      e (SUBGOAL_THEN `(LENGTH (delet (l:(((A)list) list)) y)) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
            e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;

(*----SUC CASE-----*)

e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `!(e:(((A)list) list)) y (l:(((A)list) list)).
          1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y)
          ==> zsyn_delet (APPEND l e) x y = APPEND (zsyn_delet l x y) e`);;
e (SIMP_TAC [zsyn_delet; delet]);;
e (DISCH_TAC);;
e (COND_CASES_TAC);;
e (COND_CASES_TAC);;

r (1);;
e (ASM_ARITH_TAC);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
r (1);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `!L M. (0 < LENGTH L) ==> (HD (APPEND (L:(((A)list) list)) M) = HD L)` ASSUME_TAC);;
      e (LIST_INDUCT_TAC);;
      e (SIMP_TAC [LENGTH]);;
      e (ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (ASM_SIMP_TAC [APPEND; HD]);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (SUBGOAL_THEN `0 < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;

e (UNDISCH_TAC `!(e:(((A)list) list)) y (l:(((A)list) list)).
          1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y)
          ==> (if x > y
               then delet (delet (APPEND l e) x) y
               else delet (delet (APPEND l e) y) x) =
              APPEND (if x > y then delet (delet l x) y else delet (delet l y) x) e`);;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (SUBGOAL_THEN `(1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\  ~(x = y)
          ==> (if x > y
               then delet (delet (APPEND l (e:(((A)list) list))) x) y
               else delet (delet (APPEND (l:(((A)list) list)) e) y) x) =
              APPEND (if x > y then delet (delet l x) y else delet (delet l y) x) e) = 
	      (1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\  ~(x = y) 
	      ==> ((delet (delet (APPEND l e) x) y) = (APPEND (delet (delet l x) y) e)))` ASSUME_TAC);;

e (EQ_TAC);;
e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y)
          ==> (if x > y
               then delet (delet (APPEND l (e:(((A)list) list))) x) y
               else delet (delet (APPEND (l:(((A)list) list)) e) y) x) =
              APPEND (if x > y then delet (delet l x) y else delet (delet l y) x) e`);;
e (COND_CASES_TAC);;
e (COND_CASES_TAC);;
e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (UNDISCH_TAC `~(x = y:num)`);;
e (SIMP_TAC []);;
e (REWRITE_TAC [GSYM LE_ANTISYM]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (REWRITE_TAC [NOT_LE]);;
e (STRIP_TAC);;
e (ASM_ARITH_TAC);;
e (ASM_ARITH_TAC);;

e (REPEAT STRIP_TAC);;
e (COND_CASES_TAC);;
e (COND_CASES_TAC);;
e (UNDISCH_TAC `1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y) ==> delet (delet (APPEND (l:(((A)list) list)) (e:(((A)list) list))) x) y = APPEND (delet (delet l x) y) e`);;
e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;
e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (UNDISCH_TAC `~(x = y:num)`);;
e (REWRITE_TAC [GSYM LE_ANTISYM]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (REWRITE_TAC [NOT_LE]);;
e (STRIP_TAC);;
e (ASM_ARITH_TAC);;
e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;

e (SUBGOAL_THEN	`!L M. (0 < LENGTH L) ==> ((TL (APPEND (L:(((A)list) list)) M)) = (APPEND (TL L) (M:(((A)list) list))))` ASSUME_TAC);;
      e (LIST_INDUCT_TAC);;
      e (SIMP_TAC [LENGTH]);;
      e (ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (REWRITE_TAC [APPEND]);;
      e (REWRITE_TAC [TL]);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (SUBGOAL_THEN `0 < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (SUBGOAL_THEN	`(delet (APPEND (TL l) e) x) = (APPEND (delet ((TL l:(((A)list) list))) x) (e:(((A)list) list)))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;

e (SUBGOAL_THEN `!y. (SUC x > y) /\ (y < LENGTH l) /\  
  (1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y)
      ==> delet (delet (APPEND l e) x) y = APPEND (delet (delet l x) y) e)
  		==>
       (delet (CONS (HD l) (APPEND (delet (TL (l:(((A)list) list))) x) e)) y =
 APPEND (delet (CONS (HD l) (delet (TL l) x)) y) (e:(((A)list) list)))` ASSUME_TAC);;
      e (INDUCT_TAC);;
      e (SIMP_TAC [delet]);;
      e (ASM_SIMP_TAC [TL]);;

      e (UNDISCH_TAC `~(SUC x = y)`);;
      e (UNDISCH_TAC `y < LENGTH (l:(((A)list) list))`);;
      e (UNDISCH_TAC `SUC x > y`);;
      e (UNDISCH_TAC `x < LENGTH l /\ ~(x = y)
      ==> delet (delet (APPEND (l:(((A)list) list)) (e:(((A)list) list))) x) y = APPEND (delet (delet l x) y) e`);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
    
      e (REPEAT STRIP_TAC);;

      e (ASM_SIMP_TAC [delet]);;
      e (ASM_SIMP_TAC [HD; TL]);;
      e (SUBGOAL_THEN `(delet (APPEND (delet (TL l) x) e) y') = (APPEND (delet (delet (TL l:(((A)list) list)) x) y') (e:(((A)list) list)))` ASSUME_TAC);;
	    e (MATCH_MP_TAC delet_ASSOC_THM);;
	    e (SUBGOAL_THEN `(LENGTH (delet (TL (l:(((A)list) list))) x)) = LENGTH (TL l) - 1` ASSUME_TAC);;
                  e (MATCH_MP_TAC delet_LENGTH_THM);;
	    	  e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
	                e (MATCH_MP_TAC LENGTH_TL);;
      		        e (ASM_ARITH_TAC);;

                  e (ASM_REWRITE_TAC []);;
	          e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
      	    e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
                  e (MATCH_MP_TAC LENGTH_TL);;
      	          e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
            e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC [APPEND]);;
e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (ASM_SIMP_TAC []);;


e (SUBGOAL_THEN	`(delet (APPEND l e) y) = (APPEND (delet ((l:(((A)list) list))) y) (e:(((A)list) list)))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN	`!L M. (0 < LENGTH L) ==> (HD (APPEND (L:(((A)list) list)) M) = HD L)` ASSUME_TAC);;
      e (LIST_INDUCT_TAC);;
      e (SIMP_TAC [LENGTH]);;
      e (ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (ASM_SIMP_TAC [APPEND; HD]);;

e (SUBGOAL_THEN `0 < LENGTH (delet (l:(((A)list) list)) y)` ASSUME_TAC);;
      e (SUBGOAL_THEN `(LENGTH (delet (l:(((A)list) list)) y)) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
            e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `!L M. 0 < LENGTH (L:(((A)list) list)) ==> HD (APPEND L (M:(((A)list) list))) = HD L`);;
e (DISCH_THEN (MP_TAC o SPEC `delet (l:(((A)list) list)) y`));;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;

e (SUBGOAL_THEN	`!L M. (0 < LENGTH L) ==> ((TL (APPEND (L:(((A)list) list)) M)) = (APPEND (TL L) (M:(((A)list) list))))` ASSUME_TAC);;
      e (LIST_INDUCT_TAC);;
      e (SIMP_TAC [LENGTH]);;
      e (ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (REWRITE_TAC [APPEND]);;
      e (REWRITE_TAC [TL]);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `delet (l:(((A)list) list)) y`));;
e (DISCH_THEN (MP_TAC o SPEC `(e:(((A)list) list))`));;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (SUBGOAL_THEN	`(delet (APPEND (TL (delet l y)) e) x) = (APPEND (delet (TL (delet (l:(((A)list) list)) y)) x) (e:(((A)list) list)))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;

e (SUBGOAL_THEN `!y. (y < LENGTH l) /\ ~(SUC x = y) /\ ~(SUC x > y) /\
    		(delet (APPEND l e) y = APPEND (delet l y) (e:(((A)list) list))) /\
		(0 < LENGTH (delet l y)) /\ (HD (APPEND (delet l y) e) = HD (delet l y)) /\
		(TL (APPEND (delet l y) e) = APPEND (TL (delet l y)) e)
  		==>
       ((TL (delet (l:(((A)list) list)) y)) = (delet (TL l) (y - 1)))` ASSUME_TAC);;
      e (INDUCT_TAC);;
      e (SUBGOAL_THEN `(0 - 1) = 0` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (SIMP_TAC [delet]);;

      e (UNDISCH_TAC `~(SUC x = y)`);;
      e (UNDISCH_TAC `y < LENGTH (l:(((A)list) list))`);;
      e (UNDISCH_TAC `~(SUC x > y)`);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM MP_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (REPEAT STRIP_TAC);;
      e (ASM_SIMP_TAC [delet]);;
      e (ASM_SIMP_TAC [HD; TL]);;
      e (SUBGOAL_THEN `(SUC y' - 1) = y'` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `LENGTH (delet (TL (l:(((A)list) list))) (y - 1)) = LENGTH (TL l) - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;

e (ASM_ARITH_TAC);;
e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC LENGTH_TL);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC [APPEND]);;

let zsyn_delet_ASSOC_THM = top_thm();;

(*------------------------------------------------------------------------------*)
(*				   zsyn_delet_THM					*)
(*------------------------------------------------------------------------------*)

g `!x (e:((((A)list) # ((A)list) list) list)) (y:num) z (l:(((A)list) list)).
     ALL_DISTINCT (APPEND l (SND (EL z e))) /\ 1 < LENGTH l /\ x < LENGTH l /\ y < LENGTH l /\ ~(x = y)
     ==> (~MEM (EL x l) (zsyn_delet (APPEND l (SND (EL z e))) x y))`;;

e (INDUCT_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (ASM_SIMP_TAC [zsyn_delet]);;
e (SUBGOAL_THEN `0 < y` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (COND_CASES_TAC);;
e (ASM_ARITH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(delet (APPEND l (SND (EL z e))) y) = (APPEND (delet ((l:(((A)list) list))) y) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SUBGOAL_THEN `(delet (APPEND (delet l y) (SND (EL z e))) 0) = (APPEND (delet (delet (l:(((A)list) list)) y) 0) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) y) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
      	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (SIMP_TAC [delet]);;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `!y. (y < LENGTH l) /\ ~(0 = y) ==>
           ((TL (delet (l:(((A)list) list)) y)) =(delet (TL l) (y - 1)))` ASSUME_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (INDUCT_TAC);;
      e (ASM_ARITH_TAC);;

      e (REPEAT STRIP_TAC);;
      e (REWRITE_TAC [delet; HD; TL]);;
      e (SUBGOAL_THEN `SUC y - 1 = y` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (ASM_REWRITE_TAC []);;
e (SIMP_TAC []);;
e (DISCH_TAC);;
e (UNDISCH_TAC `ALL_DISTINCT (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))`);;
e (REWRITE_TAC [ALL_DISTINCT_APPEND_1]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `~NULL (l:(((A)list) list))` ASSUME_TAC);;
      e (SIMP_TAC [GSYM LENGTH_NOT_NULL]);;
      e (ASM_ARITH_TAC);;

e (REWRITE_TAC [MEM_APPEND]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (STRIP_TAC);;

r (1);;

e (SUBGOAL_THEN `MEM (HD l) (l:(((A)list) list))` ASSUME_TAC);;
      e (SUBGOAL_THEN `(l:(((A)list) list) = (CONS (HD l) (TL l)))` ASSUME_TAC);;
            e (ASM_SIMP_TAC [LENGTH_NOT_NULL]);;
      	    e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
      	    e (ASM_SIMP_TAC [CONS_NOT_NULL]);;

      e (ONCE_ASM_REWRITE_TAC []);;
      e (SIMP_TAC [HD; MEM]);;

e (SIMP_TAC [EL; HD; MEM]);;
e (UNDISCH_TAC `!a. MEM a (l:(((A)list) list)) ==> ~MEM a (SND (EL z (e:((((A)list) # ((A)list) list) list))))`);;
e (DISCH_THEN (MP_TAC o SPEC `(HD (l:(((A)list) list)))`));;
e (ASM_SIMP_TAC []);;

r (1);;

e (SIMP_TAC [EL; HD; MEM]);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `MEM (HD l) (TL(l:(((A)list) list)))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `y - 1`);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `LENGTH (TL (l:(((A)list) list))) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC LENGTH_TL);;
      	    e (ASM_ARITH_TAC);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(ALL_DISTINCT (l:(((A)list) list)) = ALL_DISTINCT (CONS (HD l) (TL l)))` ASSUME_TAC);;
      e (ONCE_ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `CONS (HD l) (TL l) = (l:(((A)list) list))` ASSUME_TAC);;
            e (MATCH_MP_TAC NOT_NULL_IMP_CONS);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_SIMP_TAC []);;

e (UNDISCH_TAC `ALL_DISTINCT (l:(((A)list) list))`);;
e (ASM_SIMP_TAC []);;
e (REWRITE_TAC [ALL_DISTINCT]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (DISJ1_TAC);;
e (ASM_SIMP_TAC []);;


(*** SUC CASE ***)

e (REPEAT STRIP_TAC);;
e (POP_ASSUM MP_TAC);;
e (SIMP_TAC [zsyn_delet]);;
e (COND_CASES_TAC);;
e (SUBGOAL_THEN `(delet (APPEND l (SND (EL z e))) (SUC x)) = (APPEND (delet ((l:(((A)list) list))) (SUC x)) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(delet (APPEND (delet l (SUC x)) (SND (EL z e))) y) = (APPEND (delet (delet (l:(((A)list) list)) (SUC x)) y) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) (SUC x)) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
      	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) y z (l:(((A)list) list)).
          ALL_DISTINCT (APPEND l (SND (EL z e))) /\
          1 < LENGTH l /\
          x < LENGTH l /\
          y < LENGTH l /\
          ~(x = y)
          ==> ~MEM (EL x l) (zsyn_delet (APPEND l (SND (EL z e))) x y)`);;
e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `x < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (UNDISCH_TAC `ALL_DISTINCT (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))`);;
e (REWRITE_TAC [ALL_DISTINCT_APPEND_1]);;
e (STRIP_TAC);;


e (REWRITE_TAC [MEM_APPEND]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (STRIP_TAC);;

r (1);;

e (SUBGOAL_THEN `MEM (EL (SUC x) l) (l:(((A)list) list))` ASSUME_TAC);;
      e (POP_ASSUM MP_TAC);;
      e (UNDISCH_TAC `~(x = y) ==> ~MEM (EL x (l:(((A)list) list))) (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x y)`);;
      e (REWRITE_TAC [MEM_EXISTS_EL]);;
      e (SUBGOAL_THEN `~(?i. i < LENGTH (zsyn_delet (APPEND l (SND (EL z e))) x y) /\  EL x (l:(((A)list) list)) = EL i (zsyn_delet (APPEND l (SND (EL z e))) x y)) 
              = (!i. ~(i < LENGTH (zsyn_delet (APPEND l (SND (EL z e))) x y)) \/ ~(EL x l = EL i (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x y)))` ASSUME_TAC);;
            e (MESON_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (SUBGOAL_THEN `!(a:(A)list). ~(?i. i < LENGTH (SND (EL z e)) /\ a = EL i (SND (EL z (e:((((A)list) # ((A)list) list) list))))) 
              = (!i. ~(i < LENGTH (SND (EL z e))) \/ ~(a = EL i (SND (EL z e))))` ASSUME_TAC);;
            e (MESON_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (EXISTS_TAC `SUC x`);;
      e (ASM_REWRITE_TAC []);;
      e (UNDISCH_TAC `!a. MEM a (l:(((A)list) list)) ==> ~MEM a (SND (EL z (e:((((A)list) # ((A)list) list) list))))`);;
      e (DISCH_THEN (MP_TAC o SPEC `(EL (SUC x) (l:(((A)list) list)))`));;
      e (ASM_REWRITE_TAC []);;

r (1);;

e (STRIP_TAC);;
e (SUBGOAL_THEN `MEM (EL (SUC x) l) (delet (l:(((A)list) list)) (SUC x))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_MEM_THM);;
      e (EXISTS_TAC `y:num`);;
      e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) (SUC x)) = LENGTH l - 1` ASSUME_TAC);;
            e (MATCH_MP_TAC delet_LENGTH_THM);;
	    e (ASM_REWRITE_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `!x. x < LENGTH l ==> (~MEM (EL x l) (delet (l:(((A)list) list)) x))` ASSUME_TAC);;

r (1);;

e (POP_ASSUM MP_TAC);;
e (DISCH_THEN (MP_TAC o SPEC `SUC x`));;
e (ASM_SIMP_TAC []);;

r (1);;

e (GEN_TAC);;
e (STRIP_TAC);;
e (MATCH_MP_TAC delet_NOT_MEM_THM);;
e (ASM_SIMP_TAC []);;

e (POP_ASSUM MP_TAC);;
e (SUBGOAL_THEN `(~(SUC x > y) <=> SUC x <= y)` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(SUC x <= y <=> SUC x < y \/ (SUC x = y))` ASSUME_TAC);;
      e (ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (SUBGOAL_THEN `(delet (APPEND l (SND (EL z e))) y) = (APPEND (delet ((l:(((A)list) list))) y) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(delet (APPEND (delet l y) (SND (EL z e))) (SUC x)) = (APPEND (delet (delet (l:(((A)list) list)) y) (SUC x)) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_ASSOC_THM);;
      e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) y) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (ASM_REWRITE_TAC []);;

e (ONCE_ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;
e (ONCE_ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (UNDISCH_TAC `!e y z l.
          ALL_DISTINCT (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) /\
          1 < LENGTH l /\
          x < LENGTH l /\
          y < LENGTH l /\
          ~(x = y)
          ==> ~MEM (EL x l) (zsyn_delet (APPEND (l:(((A)list) list)) (SND (EL z e))) x y)`);;
e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `x < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `~(x = y:num)` ASSUME_TAC);;
      e (SUBGOAL_THEN `~(x = y:num) = ((x < y) \/ (y < x))` ASSUME_TAC);;
            e (ARITH_TAC);;
      
      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISJ1_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (DISCH_TAC);;
e (UNDISCH_TAC `ALL_DISTINCT (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list)))))`);;
e (SIMP_TAC [ALL_DISTINCT_APPEND_1]);;
e (STRIP_TAC);;
e (SIMP_TAC [MEM_APPEND]);;
e (REWRITE_TAC [DE_MORGAN_THM]);;
e (STRIP_TAC);;

r (1);;

e (SUBGOAL_THEN `MEM (EL (SUC x) l) (l:(((A)list) list))` ASSUME_TAC);;
      e (POP_ASSUM MP_TAC);;
      e (UNDISCH_TAC `~MEM (EL x (l:(((A)list) list))) (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x y)`);;
      e (REWRITE_TAC [MEM_EXISTS_EL]);;
      e (SUBGOAL_THEN `~(?i. i < LENGTH (zsyn_delet (APPEND l (SND (EL z e))) x y) /\  EL x (l:(((A)list) list)) = EL i (zsyn_delet (APPEND l (SND (EL z e))) x y)) 
              = (!i. ~(i < LENGTH (zsyn_delet (APPEND l (SND (EL z e))) x y)) \/ ~(EL x l = EL i (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x y)))` ASSUME_TAC);;
            e (MESON_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (SUBGOAL_THEN `!(a:(A)list). ~(?i. i < LENGTH (SND (EL z e)) /\ a = EL i (SND (EL z (e:((((A)list) # ((A)list) list) list))))) 
              = (!i. ~(i < LENGTH (SND (EL z e))) \/ ~(a = EL i (SND (EL z e))))` ASSUME_TAC);;
            e (MESON_TAC []);;

      e (ASM_REWRITE_TAC []);;
      e (POP_ASSUM (K ALL_TAC));;
      e (DISCH_TAC);;
      e (EXISTS_TAC `SUC x`);;
      e (ASM_REWRITE_TAC []);;
      e (UNDISCH_TAC `!a. MEM a (l:(((A)list) list)) ==> ~MEM a (SND (EL z (e:((((A)list) # ((A)list) list) list))))`);;
      e (DISCH_THEN (MP_TAC o SPEC `(EL (SUC x) (l:(((A)list) list)))`));;
      e (ASM_REWRITE_TAC []);;

e (SUBGOAL_THEN `(EL (SUC x) (l:(((A)list) list))) = EL (SUC x) (delet l y)` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_EL_THM);;
      e (ASM_REWRITE_TAC []);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (MATCH_MP_TAC delet_NOT_MEM_THM);;
e (SUBGOAL_THEN `LENGTH (delet (l:(((A)list) list)) y) = LENGTH l - 1` ASSUME_TAC);;
      e (MATCH_MP_TAC delet_LENGTH_THM);;
      e (ASM_REWRITE_TAC []);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (STRIP_TAC);;
e (MATCH_MP_TAC delet_DISTINCT_THM);;
e (ASM_REWRITE_TAC []);;
e (ASM_ARITH_TAC);;

let zsyn_delet_THM = top_thm ();;

(*--------------------------------END_OF_FILE--------------------------------*)