(* ========================================================================= *)
(* File Name: One_Reaction.ml		                                     *)
(*---------------------------------------------------------------------------*)
(* Description: Formal Verification of Zsyntax Properties                    *)
(*                                                                           *)
(*                                                                           *)
(*     (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			                                     *)
(*---------------------------------------------------------------------------*)
(*   Z_EVF_MATCH_THM;			                         	     *)
(*   Z_recur1_MATCH_THM;						     *)
(*   Z_recur2_MATCH_THM;				                     *)
(*   Z_DED_MATCH_THM;							     *)
(*   Z_DEDUCTION_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          *)
(*	    This file needs z_Delete_Theorems.ml to be uploaded first        *)
(*	    This file needs No_Reaction.ml to be uploaded first  	     *)
(*---------------------------------------------------------------------------*)

(*---------------------------------------------------------------------------*)
(* 			       z_EVF_MATCH_THM 				     *)
(*---------------------------------------------------------------------------*)

g `!p (e:((((A)list) # (((A)list) list)) list)) (l:(((A)list) list)) x y z.
      ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\ (p < LENGTH e) /\
      (z <= p) /\ (HD l = FST (EL z e)) /\
      (!a b. ~(a = b)  ==> ~(FST (EL a e) = FST (EL b e)))
      ==> ((zsyn_EVF l e p x y) = (T,(zsyn_delet (APPEND (TL l) (SND (EL z e))) x y)))`;;

e (INDUCT_TAC);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [zsyn_EVF]);;
e (COND_CASES_TAC);;
e (UNDISCH_TAC `z <= 0`);;
e (REWRITE_TAC [LE]);;
e (SIMP_TAC []);;
e (UNDISCH_TAC `z <= 0`);;
e (REWRITE_TAC [LE]);;
e (DISCH_TAC);;
e (UNDISCH_TAC `HD (l:(((A)list) list)) = FST (EL z (e:((((A)list) # (((A)list) list)) list)))`);;
e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
e (ASM_SIMP_TAC []);;


e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [zsyn_EVF]);;
e (SUBGOAL_THEN `p < LENGTH (e:((((A)list) # ((A)list) list) list))` ASSUME_TAC);;
      e (MATCH_MP_TAC LT_TRANS);;
      e (EXISTS_TAC `SUC p`);;
      e (ASM_REWRITE_TAC []);;
      e (ARITH_TAC);;

e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x y z.
          ~NULL e /\
          ~NULL l /\
          x < LENGTH l /\
          y < LENGTH l /\
          p < LENGTH e /\
          z <= p /\
          HD l = FST (EL z e) /\
          (!a b. ~(a = b) ==> ~(FST (EL a e) = FST (EL b e)))
          ==> zsyn_EVF l e p x y = T,zsyn_delet (APPEND (TL 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 `(l:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `x:num`));;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (UNDISCH_TAC `z <= SUC p`);;
e (REWRITE_TAC [LE]);;
e (STRIP_TAC);;
e (ASM_MESON_TAC []);;
e (UNDISCH_TAC `z <= p ==> zsyn_EVF (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) p x y = T,zsyn_delet (APPEND (TL l) (SND (EL z e))) x y`);;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `z < LENGTH (e:((((A)list) # (((A)list) list)) list))` ASSUME_TAC);;
      e (MATCH_MP_TAC LET_TRANS);;
      e (EXISTS_TAC `p:num`);;
      e (ASM_SIMP_TAC []);;

e (SUBGOAL_THEN `~((z:num) = (SUC p))` ASSUME_TAC);;
      e (MATCH_MP_TAC LESS_NOT_EQ);;
      e (ASM_ARITH_TAC);;

e (ASM_MESON_TAC []);;

let Z_EVF_MATCH_THM = top_thm();;

(*---------------------------------------------------------------------------*)
(* 			     z_RECUR1_MATCH_THM                              *)
(*---------------------------------------------------------------------------*)

g `!y (e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x z y'.
      ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ (y < LENGTH l) /\
      ((z:num) < LENGTH e) /\ (y':num) <= y /\ ALL_DISTINCT l /\
      (!y. y < LENGTH l ==> 
      if ((EL y l = EL y' l)) then
      	 (HD (zsyn_conjun_intro l x y) = FST (EL z e))
      else
	 (!a. MEM a e ==> ~((FST a) = (HD (zsyn_conjun_intro l x y))))) /\
      (!a b. ~(a = b)  ==> ~((FST (EL a e)) = (FST (EL b e))))
      ==> ((zsyn_recurs1 l e x y) = (T,(zsyn_delet (APPEND l (SND (EL z e))) x y')))`;;

e (INDUCT_TAC);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `TL (zsyn_conjun_intro (l:(((A)list) list)) x y') = l` ASSUME_TAC);;
      e (REWRITE_TAC [zsyn_conjun_intro]);;
      e (ASM_SIMP_TAC [TL; FLAT; EL]);;

e (REWRITE_TAC [zsyn_recurs1]);;
e (SUBGOAL_THEN `((zsyn_EVF (zsyn_conjun_intro (l:(((A)list) list)) x 0) (e:((((A)list) # ((A)list) list) list)) (LENGTH e - 1) x 0) = 
  	    (T, zsyn_delet (APPEND (TL (zsyn_conjun_intro l x 0)) (SND (EL z e))) x 0))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_EVF_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (UNDISCH_TAC `y' <= 0`);;
      e (REWRITE_TAC [LE]);;
      e (STRIP_TAC);;
      e (REWRITE_TAC [zsyn_conjun_intro]);;
      e (REWRITE_TAC [LENGTH]);;
      e (SIMP_TAC [NULL]);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (UNDISCH_TAC `~NULL (l:(((A)list) list))`);;
      e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);;
      e (DISCH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (SUBGOAL_THEN `LENGTH (e:((((A)list) # ((A)list) list) list)) - 1 < LENGTH e` ASSUME_TAC);;
            e (REWRITE_TAC [GSYM REAL_OF_NUM_LT]);;
      	    e (SUBGOAL_THEN `&(LENGTH (e:((((A)list) # ((A)list) list) list)) - 1) = &(LENGTH e) - &1` ASSUME_TAC);;
                  e (ONCE_REWRITE_TAC [EQ_SYM_EQ]);;
	    	  e (MATCH_MP_TAC REAL_OF_NUM_SUB);;
	    	  e (UNDISCH_TAC `~NULL (e:((((A)list) # ((A)list) list) list))`);;
	    	  e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);;
      	    	  e (ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;
      	    e (POP_ASSUM (K ALL_TAC));;
      	    e (REWRITE_TAC [REAL_ARITH `(&m - &1 < &m) = (&0 < &1)`]);;
      	    e (REAL_ARITH_TAC);;

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

      e (UNDISCH_TAC `!y. y < LENGTH (l:(((A)list) list))
          ==> (if EL y l = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `0`));;
      e (ASM_SIMP_TAC [zsyn_conjun_intro]);;
      e (ASM_REWRITE_TAC []);;
      e (SUBGOAL_THEN `(TL (zsyn_conjun_intro (l:(((A)list) list)) x 0)) = (TL (zsyn_conjun_intro l x y'))` ASSUME_TAC);;
            e (UNDISCH_TAC `y' <= 0`);;
      	    e (REWRITE_TAC [LE]);;
      	    e (SIMP_TAC []);;

      e (POP_ASSUM MP_TAC);;
      e (SIMP_TAC []);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (POP_ASSUM (K ALL_TAC));;
      e (ASM_REWRITE_TAC []);;
      e (UNDISCH_TAC `y' <= 0`);;
      e (REWRITE_TAC [LE]);;
      e (SIMP_TAC []);;

e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `TL (zsyn_conjun_intro (l:(((A)list) list)) x y') = l` ASSUME_TAC);;
      e (REWRITE_TAC [zsyn_conjun_intro]);;
      e (ASM_SIMP_TAC [TL; FLAT; EL]);;

e (REWRITE_TAC [zsyn_recurs1]);;
e (SUBGOAL_THEN `y < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `y' <= SUC y`);;
e (REWRITE_TAC [LE]);;
e (STRIP_TAC);;
e (ASM_REWRITE_TAC []);;
e (UNDISCH_TAC `TL (zsyn_conjun_intro (l:(((A)list) list)) x y') = l`);;
e (ASM_REWRITE_TAC []);;
e (STRIP_TAC);;
e (SUBGOAL_THEN `((zsyn_EVF (zsyn_conjun_intro (l:(((A)list) list)) x (SUC y)) (e:((((A)list) # ((A)list) list) list)) (LENGTH e - 1) x (SUC y)) = 
  	    (T, zsyn_delet (APPEND (TL (zsyn_conjun_intro l x (SUC y))) (SND (EL z e))) x (SUC y)))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_EVF_MATCH_THM);;
      e (REWRITE_TAC [zsyn_conjun_intro]);;
      e (REWRITE_TAC [LENGTH]);;
      e (ASM_SIMP_TAC [NULL]);;
      e (CONJ_TAC);;  
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;  
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;  
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;  
      e (ASM_ARITH_TAC);;
      e (UNDISCH_TAC `!y. y < LENGTH l
          ==> (if EL y l = EL y' l
               then HD (zsyn_conjun_intro (l:(((A)list) list)) x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC y`));;
      e (ASM_SIMP_TAC [zsyn_conjun_intro]);;

      e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x z y'.
          ~NULL e /\
          ~NULL l /\
          x < LENGTH l /\
          y < LENGTH l /\
          z < LENGTH e /\
          y' <= y /\
          ALL_DISTINCT l /\
          (!y. y < LENGTH l
               ==> (if EL y l = EL y' l
                    then HD (zsyn_conjun_intro l x y) = FST (EL z e)
                    else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))) /\
          (!a b. ~(a = b) ==> ~(FST (EL a e) = FST (EL b e)))
          ==> zsyn_recurs1 l e x y = T,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 `(l:(((A)list) list))`));;
      e (DISCH_THEN (MP_TAC o SPEC `x:num`));;
      e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
      e (DISCH_THEN (MP_TAC o SPEC `y':num`));;
      e (ASM_SIMP_TAC []);;

e (SUBGOAL_THEN `~(y' = SUC y)` ASSUME_TAC);;
      e (MATCH_MP_TAC LESS_NOT_EQ);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `(zsyn_EVF (zsyn_conjun_intro (l:(((A)list) list)) x (SUC y)) (e:((((A)list) # ((A)list) list) list)) (LENGTH e - 1) x (SUC y)) =
  	    	 (F,TL (zsyn_conjun_intro l x (SUC y)))` ASSUME_TAC);;
      e (MATCH_MP_TAC EVF_GEN_THM);;
      e (ASM_SIMP_TAC [zsyn_conjun_intro; HD; LENGTH; MEM; NULL]);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (STRIP_TAC);;
      e (DISCH_TAC);;
      e (UNDISCH_TAC `!y. y < LENGTH (l:(((A)list) list))
          ==> (if EL y l = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC y`));;
      e (ASM_SIMP_TAC []);;
      e (REWRITE_TAC [zsyn_conjun_intro]);;
      e (REWRITE_TAC [HD]);;
      e (COND_CASES_TAC);;
      e (SIMP_TAC []);;
      e (STRIP_TAC);;
      e (SUBGOAL_THEN `(EL (SUC y) (l:(((A)list) list)) = EL (y':num) l) <=> ((SUC y) = y')` ASSUME_TAC);;
	    e (MATCH_MP_TAC ALL_DISTINCT_EL_IMP);;
      	    e (ASM_SIMP_TAC []);;
	    e (ASM_ARITH_TAC);;

      e (ASM_MESON_TAC []);;

      e (ASM_MESON_TAC []);;

e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) x z y'.
          ~NULL e /\
          ~NULL l /\
          x < LENGTH l /\
          y < LENGTH l /\
          z < LENGTH e /\
          y' <= y /\
          ALL_DISTINCT l /\
          (!y. y < LENGTH l
               ==> (if EL y l = EL y' l
                    then HD (zsyn_conjun_intro l x y) = FST (EL z e)
                    else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))) /\
          (!a b. ~(a = b) ==> ~(FST (EL a e) = FST (EL b e)))
          ==> zsyn_recurs1 l e x y = T,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 `(l:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `x:num`));;
e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
e (DISCH_THEN (MP_TAC o SPEC `y':num`));;
e (ASM_SIMP_TAC []);;

let Z_recur1_MATCH_THM = top_thm();;

(*---------------------------------------------------------------------------*)
(* 			     z_RECUR2_MATCH_THM 	                     *)
(*---------------------------------------------------------------------------*)

g `!x (e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) y z x' y'.
      ~NULL e /\ ~NULL l /\ (x < LENGTH l) /\ ((y:num) < LENGTH l) /\
      ((z:num) < LENGTH e) /\ y' <= y /\ x' <= x /\ ALL_DISTINCT l /\
      (!x y. x < LENGTH l /\ y < LENGTH l ==>
      if ((EL x l = EL x' l) /\ (EL y l = EL y' l)) then
      	 (HD (zsyn_conjun_intro l x y) = FST (EL z e))
      else
	 (!a. MEM a e ==> ~((FST a) = (HD (zsyn_conjun_intro l x y))))) /\

      (!a b. ~(a = b)  ==> ~((FST (EL a e)) = (FST (EL b e))))
      ==> ((zsyn_recurs2 l e x y) = (T,(zsyn_delet (APPEND l (SND (EL z e))) x' y')))`;;

e (INDUCT_TAC);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [zsyn_recurs2]);;
e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # (((A)list) list)) list)) 0 y = (T,(zsyn_delet (APPEND l (SND (EL z e))) 0 y'))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_recur1_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (SUBGOAL_THEN `x' = 0` ASSUME_TAC);;
            e (ASM_ARITH_TAC);;

      e (UNDISCH_TAC `x' <= 0`);;
      e (DISCH_TAC);;
      e (POP_ASSUM (K ALL_TAC));;
      e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH (l:(((A)list) list))
          ==> (if EL x l = EL x' l /\ EL y l = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `0`));;
      e (ASM_SIMP_TAC []);;

e (ASM_SIMP_TAC [FST; SND]);;
e (SUBGOAL_THEN `x' = 0` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;


e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) l y z x' y'.
          ~NULL e /\
          ~NULL l /\
          x < LENGTH (l:(((A)list) list)) /\
          y < LENGTH l /\
          z < LENGTH e /\
          y' <= y /\
          x' <= x /\
          ALL_DISTINCT l /\
          (!x y.
               x < LENGTH l /\ y < LENGTH l
               ==> (if EL x l = EL x' l /\ EL y l = EL y' l
                    then HD (zsyn_conjun_intro l x y) = FST (EL z e)
                    else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))) /\
          (!a b. ~(a = b) ==> ~(FST (EL a e) = FST (EL b e)))
          ==> zsyn_recurs2 l e x y = T,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 `(l:(((A)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 `x':num`));;
e (DISCH_THEN (MP_TAC o SPEC `y':num`));;
e (ASM_SIMP_TAC []);;
e (DISCH_TAC);;
e (REWRITE_TAC [zsyn_recurs2]);;
e (SUBGOAL_THEN `x < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `x' <= SUC x`);;
e (SIMP_TAC [LE]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (SUC x) y = (T,(zsyn_delet (APPEND l (SND (EL z e))) (SUC x) y'))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_recur1_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (GEN_TAC);;
      e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH l
          ==> (if EL x l = EL x' l /\ EL y (l:(((A)list) list)) = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC x`));;
      e (ASM_SIMP_TAC []);;

e (ASM_SIMP_TAC [FST; SND]);;
e (SUBGOAL_THEN `~(x' = SUC x)` ASSUME_TAC);;
      e (MATCH_MP_TAC LESS_NOT_EQ);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (SUC x) (y:num) = (F,l) ` ASSUME_TAC);;
      e (MATCH_MP_TAC RECUR1_GEN_THM);;
      e (ASM_SIMP_TAC []);;
      e (REWRITE_TAC [MEM]);;
      e (REPEAT GEN_TAC);;
      e (STRIP_TAC);;
      e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH (l:(((A)list) list))
          ==> (if EL x l = EL x' l /\ EL y l = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC x`));;
      e (ASM_SIMP_TAC []);;
      e (DISCH_TAC);;
      e (UNDISCH_TAC `x < LENGTH (l:(((A)list) list)) /\ x' <= x
      ==> zsyn_recurs2 l e x y = T,zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x' y'`);;
      e (ASM_SIMP_TAC []);;
      e (DISCH_TAC);;
      e (SUBGOAL_THEN `(~(x' = (SUC x))) ==> (~(EL (SUC x) (l:(((A)list) list)) = EL x' l))` ASSUME_TAC);;
            e (ASM_SIMP_TAC []);;
	    e (SUBGOAL_THEN `((EL (SUC x) (l:(((A)list) list)) = EL x' l)) <=> ((SUC x) = x')` ASSUME_TAC);;
	          e (MATCH_MP_TAC ALL_DISTINCT_EL_IMP);;
		  e (ASM_SIMP_TAC []);;
		  e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;

      e (ASM_MESON_TAC []);;

e (ASM_SIMP_TAC [FST]);;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM (K ALL_TAC));;
e (UNDISCH_TAC `SUC x < LENGTH (l:(((A)list) list))`);;
e (DISCH_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM MP_TAC);;
e (POP_ASSUM (K ALL_TAC));;
e (REPEAT DISCH_TAC);;



e (SUBGOAL_THEN `!x. (x < LENGTH l) /\ (x' <= x) ==> (zsyn_recurs2 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) x (LENGTH l - 1) = T,zsyn_delet (APPEND l (SND (EL z e))) x' y')` ASSUME_TAC);;


e (POP_ASSUM (K ALL_TAC));;
e (POP_ASSUM (K ALL_TAC));;


      e (INDUCT_TAC);;
      e (STRIP_TAC);;
      e (REWRITE_TAC [zsyn_recurs2]);;
      e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) 0 (LENGTH l - 1) = (T,(zsyn_delet (APPEND l (SND (EL z e))) 0 y'))` ASSUME_TAC);;
            e (MATCH_MP_TAC Z_recur1_MATCH_THM);;
	    e (ASM_SIMP_TAC []);;
	    e (CONJ_TAC);;
	    e (ASM_ARITH_TAC);;
 	    e (CONJ_TAC);;
	    e (ASM_ARITH_TAC);;
	    e (SIMP_TAC [zsyn_conjun_intro; HD; LENGTH; MEM]);;
	    e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH l
          ==> (if EL x l = EL x' l /\ EL y l = EL y' (l:(((A)list) list))
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
	    e (SIMP_TAC [zsyn_conjun_intro; HD; LENGTH; MEM]);;
	    e (SUBGOAL_THEN `x' = 0` ASSUME_TAC);;
  	          e (ASM_ARITH_TAC);;

            e (POP_ASSUM MP_TAC);;
	    e (POP_ASSUM (K ALL_TAC));;
	    e (SIMP_TAC []);;
	    e (DISCH_TAC);;
	    e (DISCH_THEN (MP_TAC o SPEC `0`));;
	    e (ASM_SIMP_TAC []);;

      e (ASM_SIMP_TAC [FST]);;
      e (SUBGOAL_THEN `x' = 0` ASSUME_TAC);;
      e (ASM_ARITH_TAC);;
      e (ASM_SIMP_TAC []);;

      e (STRIP_TAC);;
      e (REWRITE_TAC [zsyn_recurs2]);;
      e (SUBGOAL_THEN `x < LENGTH (l:(((A)list) list))` ASSUME_TAC);;
            e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `x' <= SUC x`);;
e (SIMP_TAC [LE]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (SUC x) (LENGTH l - 1) = (T,(zsyn_delet (APPEND l (SND (EL z e))) (SUC x) y'))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_recur1_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (GEN_TAC);;
      e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH l
          ==> (if EL x l = EL x' l /\ EL y (l:(((A)list) list)) = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC x`));;
      e (ASM_SIMP_TAC []);;

e (ASM_SIMP_TAC [FST; SND]);;
e (SUBGOAL_THEN `~((x':num) = (SUC (x:num)))` ASSUME_TAC);;
      e (MATCH_MP_TAC LESS_NOT_EQ);;
      e (ASM_ARITH_TAC);;

e (SUBGOAL_THEN `zsyn_recurs1 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) (SUC x) (LENGTH l - 1) = (F,l) ` ASSUME_TAC);;
      e (MATCH_MP_TAC RECUR1_GEN_THM);;
      e (ASM_SIMP_TAC []);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (REWRITE_TAC [MEM]);;
      e (REPEAT GEN_TAC);;
      e (STRIP_TAC);;
      e (UNDISCH_TAC `!x y.
          x < LENGTH l /\ y < LENGTH (l:(((A)list) list))
          ==> (if EL x l = EL x' l /\ EL y l = EL y' l
               then HD (zsyn_conjun_intro l x y) = FST (EL z (e:((((A)list) # ((A)list) list) list)))
               else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro l x y)))`);;
      e (DISCH_THEN (MP_TAC o SPEC `SUC x`));;
      e (ASM_SIMP_TAC []);;
      e (DISCH_TAC);;
      e (UNDISCH_TAC `x < LENGTH (l:(((A)list) list)) /\ x' <= x
      ==> zsyn_recurs2 l e x (LENGTH l - 1) = T,zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) x' y'`);;
      e (ASM_SIMP_TAC []);;
      e (DISCH_TAC);;
      e (SUBGOAL_THEN `(~(x' = (SUC x))) ==> (~(EL (SUC x) (l:(((A)list) list)) = EL x' l))` ASSUME_TAC);;
            e (ASM_SIMP_TAC []);;
	    e (SUBGOAL_THEN `((EL (SUC x) (l:(((A)list) list)) = EL x' l)) <=> ((SUC x) = x')` ASSUME_TAC);;
	          e (MATCH_MP_TAC ALL_DISTINCT_EL_IMP);;
		  e (ASM_SIMP_TAC []);;
		  e (ASM_ARITH_TAC);;

            e (ASM_REWRITE_TAC []);;

      e (ASM_MESON_TAC []);;

e (ASM_SIMP_TAC []);;
e (POP_ASSUM MP_TAC);;
e (ASM_MESON_TAC []);;

let Z_recur2_MATCH_THM = top_thm();;

(*---------------------------------------------------------------------------*)
(* 		           z_DEDUCTION_RECUR_MATCH_THM 	         	     *)
(*---------------------------------------------------------------------------*)

g `!le (e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) m n z m' n'.
      ~NULL e /\ (1 < LENGTH l) /\ (m < LENGTH l) /\ (n < LENGTH l) /\
      (z < LENGTH e) /\ n' <= n /\ m' <= m /\ (le <= LENGTH e) /\ ~(le = 0) /\
      ALL_DISTINCT (APPEND l (SND (EL z e))) /\ ~(m' = n') /\ ~NULL (SND (EL z e)) /\
      (!k x y. x < LENGTH k /\ y < LENGTH k /\ 
      (!j. MEM j k ==> MEM j l \/ ?q. (MEM q e /\ MEM j (SND q))) ==>
      
      if ((EL x (k:(((A)list) list)) = EL m' l) /\ (EL y k = EL n' l)) then
      	 (HD (zsyn_conjun_intro k x y) = FST (EL z e))
      else
	 (!a. MEM a e ==> ~((FST a) = (HD (zsyn_conjun_intro k x y))))) /\

      (!a b. ~(a = b)  ==> ~(FST (EL a e) = FST (EL b e))) 
      ==> ((zsyn_deduct_recurs l e m n le) = (T,(zsyn_delet (APPEND l (SND (EL z e))) m' n')))`;;

e (INDUCT_TAC);;
e (REPEAT STRIP_TAC);;
e (ASM_MESON_TAC []);;

e (REPEAT STRIP_TAC);;
e (UNDISCH_TAC `!(e:((((A)list) # ((A)list) list) list)) l m n z m' n'.
          ~NULL e /\
          1 < LENGTH (l:(((A)list) list)) /\
          m < LENGTH l /\
          n < LENGTH l /\
          z < LENGTH e /\
          n' <= n /\
          m' <= m /\
          le <= LENGTH e /\
          ~(le = 0) /\
          ALL_DISTINCT (APPEND l (SND (EL z e))) /\
          ~(m' = n') /\
          ~NULL (SND (EL z e)) /\
          (!k x y.
               x < LENGTH k /\
               y < LENGTH k /\
               (!j. MEM j k ==> MEM j l \/ (?q. MEM q e /\ MEM j (SND q)))
               ==> (if EL x k = EL m' l /\ EL y k = EL n' l
                    then HD (zsyn_conjun_intro k x y) = FST (EL z e)
                    else !a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro k x y)))) /\
          (!a b. ~(a = b) ==> ~(FST (EL a e) = FST (EL b e)))
          ==> zsyn_deduct_recurs l e m n le =
              T,zsyn_delet (APPEND l (SND (EL z e))) m' n'`);;
e (DISCH_THEN (MP_TAC o SPEC `(e:((((A)list) # ((A)list) list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `(l:(((A)list) list))`));;
e (DISCH_THEN (MP_TAC o SPEC `m:num`));;
e (DISCH_THEN (MP_TAC o SPEC `n:num`));;
e (DISCH_THEN (MP_TAC o SPEC `z:num`));;
e (DISCH_THEN (MP_TAC o SPEC `m':num`));;
e (DISCH_THEN (MP_TAC o SPEC `n':num`));;
e (ASM_REWRITE_TAC []);;
e (DISCH_TAC);;
e (REWRITE_TAC [zsyn_deduct_recurs]);;
e (SUBGOAL_THEN `zsyn_recurs2 (l:(((A)list) list)) (e:((((A)list) # ((A)list) list) list)) m n = 
  	    (T, zsyn_delet (APPEND l (SND (EL z e))) m' n')` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_recur2_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (REWRITE_TAC [GSYM LENGTH_NOT_NULL]);;
      e (CONJ_TAC);;
      e (ASM_ARITH_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]);;
      e (SIMP_TAC []);;

e (ASM_SIMP_TAC [FST]);;
e (POP_ASSUM (K ALL_TAC));;
e (SUBGOAL_THEN `(zsyn_deduct_recurs (zsyn_delet (APPEND (l:(((A)list) list)) (SND (EL z e))) m' n') e 
(LENGTH (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n') - 1) 
(LENGTH (zsyn_delet (APPEND l (SND (EL z e))) m' n') - 1) le 
= (T,(zsyn_delet (APPEND l (SND (EL z e))) m' n')))` ASSUME_TAC);;

r (1);;

e (ASM_SIMP_TAC []);;

e (POP_ASSUM (K ALL_TAC));;
e (MATCH_MP_TAC RECUR_DED_GEN_THM);;
e (ASM_SIMP_TAC []);;
e (ASM_SIMP_TAC [LENGTH]);;
e (ONCE_REWRITE_TAC [GSYM LENGTH_NOT_NULL]);;
e (SUBGOAL_THEN `(LENGTH (zsyn_delet (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n') - 1 <
 LENGTH (zsyn_delet (APPEND l (SND (EL z e))) m' n')) = (0 < LENGTH (zsyn_delet (APPEND l (SND (EL z e))) m' n'))` ASSUME_TAC);;
      e (ASM_MESON_TAC [NUM_MINUS_ONE_LT_NUM_EQ]);;

e (ASM_REWRITE_TAC []);;
e (POP_ASSUM (K ALL_TAC));;
e (UNDISCH_TAC `~NULL (SND (EL z (e:((((A)list) # ((A)list) list) list))))`);;
e (ONCE_REWRITE_TAC [GSYM LENGTH_NOT_NULL]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `(LENGTH (zsyn_delet (APPEND l (SND (EL z e))) m' n') = LENGTH (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list))))) - 2)` ASSUME_TAC);;
      e (MATCH_MP_TAC zsyn_delet_LENGTH_THM);;
      e (ASM_SIMP_TAC [LENGTH_APPEND]);;
      e (STRIP_TAC);;
      e (SUBGOAL_THEN `(1 = 1 + 0)` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ONCE_ASM_REWRITE_TAC []);;
      e (MATCH_MP_TAC LT_ADD2);;
      e (ASM_REWRITE_TAC []);;
      e (STRIP_TAC);;
      e (SUBGOAL_THEN `(m' = m' + 0)` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ONCE_ASM_REWRITE_TAC []);;
      e (MATCH_MP_TAC LT_ADD2);;
      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;
      e (SUBGOAL_THEN `(n' = n' + 0)` ASSUME_TAC);;
            e (ARITH_TAC);;

      e (ONCE_ASM_REWRITE_TAC []);;
      e (MATCH_MP_TAC LT_ADD2);;
      e (ASM_REWRITE_TAC []);;
      e (ASM_ARITH_TAC);;

e (ASM_REWRITE_TAC []);;
e (ASM_SIMP_TAC [LENGTH_APPEND]);;
e (SUBGOAL_THEN `0 < (LENGTH (l:(((A)list) list)) + LENGTH (SND (EL z (e:((((A)list) # ((A)list) list) list))))) - 2` ASSUME_TAC);;
      e (SUBGOAL_THEN `(0 < (LENGTH (l:(((A)list) list)) + LENGTH (SND (EL z (e:((((A)list) # ((A)list) list) list))))) - 2) = (1 + 1 < (LENGTH l + LENGTH (SND (EL z e))))` ASSUME_TAC);;
            e (ARITH_TAC);;

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

e (ASM_REWRITE_TAC []);;
e (STRIP_TAC);;
e (ASM_ARITH_TAC);;
e (REPEAT GEN_TAC);;
e (STRIP_TAC);;
e (SIMP_TAC [LENGTH_APPEND; MEM]);;
e (UNDISCH_TAC `!k x y.
          x < LENGTH (k:(((A)list) list)) /\
          y < LENGTH k /\
          (!j. MEM j k ==> MEM j l \/ (?q. MEM q e /\ MEM j (SND q)))
          ==> (if EL x k = EL m' l /\ EL y k = EL n' (l:(((A)list) list))
               then HD (zsyn_conjun_intro k x y) = FST (EL z e)
               else !a. MEM a (e:((((A)list) # ((A)list) list) list)) ==> ~(FST a = HD (zsyn_conjun_intro k x y)))`);;
e (DISCH_THEN (MP_TAC o SPEC `(zsyn_delet (APPEND (l:(((A)list) list)) (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n')`));;
e (DISCH_THEN (MP_TAC o SPEC `x:num`));;
e (DISCH_THEN (MP_TAC o SPEC `y:num`));;
e (ASM_SIMP_TAC [LENGTH_APPEND]);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `!j. MEM j (APPEND (zsyn_delet (l:(((A)list) list)) m' n') (SND (EL z (e:((((A)list) # ((A)list) list) list))))) 
==> MEM j l \/ ?q. (MEM q e /\ MEM j (SND q))` ASSUME_TAC);;

r (1);;

e (SUBGOAL_THEN `(zsyn_delet (APPEND l (SND (EL z e))) m' n') = (APPEND (zsyn_delet (l:(((A)list) list)) m' n') (SND (EL z (e:((((A)list) # ((A)list) list) list)))))` ASSUME_TAC);;
      e (MATCH_MP_TAC zsyn_delet_ASSOC_THM);;
      e (ASM_SIMP_TAC []);;
      e (STRIP_TAC);;
      e (ASM_ARITH_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;
e (SUBGOAL_THEN `(~MEM (EL m' (l:(((A)list) list))) (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n'))` ASSUME_TAC);;
      e (MATCH_MP_TAC zsyn_delet_THM);;
      e (ASM_SIMP_TAC []);;
      e (STRIP_TAC);;
      e (ASM_ARITH_TAC);;
      e (ASM_ARITH_TAC);;

e (UNDISCH_TAC `(!j. MEM j (zsyn_delet (APPEND (l:(((A)list) list)) (SND (EL z e))) m' n')
           ==> MEM j l \/ (?q. MEM q e /\ MEM j (SND q)))
      ==> (if EL x (zsyn_delet (APPEND l (SND (EL z e))) m' n') = EL m' l /\
              EL y (zsyn_delet (APPEND l (SND (EL z e))) m' n') = EL n' l
           then HD
                (zsyn_conjun_intro (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n') x y) =
                FST (EL z e)
           else !a. MEM a e
                    ==> ~(FST a =
                          HD
                          (zsyn_conjun_intro (zsyn_delet (APPEND l (SND (EL z e))) m' n')
                           x
                          y)))`);;
e (COND_CASES_TAC);;
e (ASM_SIMP_TAC []);;

r (1);;

e (ASM_SIMP_TAC []);;

r (1);;

e (DISCH_TAC);;
e (SUBGOAL_THEN `(MEM (EL m' (l:(((A)list) list))) (zsyn_delet (APPEND l (SND (EL z (e:((((A)list) # ((A)list) list) list))))) m' n'))` ASSUME_TAC);;
      e (SIMP_TAC [MEM_EXISTS_EL]);;
      e (ASM_SIMP_TAC []);;
      e (SIMP_TAC [LENGTH_APPEND]);;
      e (EXISTS_TAC `x:num`);;
      e (ASM_SIMP_TAC []);;
      e (ASM_MESON_TAC []);;

e (ASM_MESON_TAC []);;

e (SIMP_TAC [MEM_APPEND]);;
e (REPEAT STRIP_TAC);;
e (SUBGOAL_THEN `MEM j (l:(((A)list) list))` ASSUME_TAC);;
      e (MATCH_MP_TAC zsyn_delet_MEM_THM);;
      e (EXISTS_TAC `m':num`);;
      e (EXISTS_TAC `n':num`);;
      e (ASM_SIMP_TAC []);;
      e (STRIP_TAC);;
      e (ASM_ARITH_TAC);;
      e (ASM_ARITH_TAC);;

e (DISJ1_TAC);;
e (ASM_SIMP_TAC []);;

e (SUBGOAL_THEN `~MEM j (l:(((A)list) list))` ASSUME_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]);;
      e (STRIP_TAC);;
      e (POP_ASSUM MP_TAC);;
      e (DISCH_THEN (MP_TAC o SPEC `(j:(A)list)`));;
      e (DISCH_TAC);;
      e (STRIP_TAC);;
      e (UNDISCH_TAC `MEM j (l:(((A)list) list)) ==> ~MEM j (SND (EL z (e:((((A)list) # ((A)list) list) list))))`);;
      e (ASM_REWRITE_TAC []);;

e (DISJ2_TAC);;
e (EXISTS_TAC `(EL z (e:((((A)list) # ((A)list) list) list)))`);;
e (ASM_REWRITE_TAC []);;
e (SIMP_TAC [MEM_EXISTS_EL]);;
e (EXISTS_TAC `z:num`);;
e (ASM_SIMP_TAC []);;

let Z_DED_MATCH_THM = top_thm ();;

(*---------------------------------------------------------------------------*)
(* 			   z_DEDUCTION_MATCH_THM 			     *)
(*---------------------------------------------------------------------------*)

g `!(e:((((A)list) # ((A)list) list) list)) (l:(((A)list) list)) z x' y'.
      ~NULL e /\ 1 < LENGTH l /\ x' < LENGTH l /\ y' < LENGTH l /\
      ALL_DISTINCT (APPEND l (SND (EL z e))) /\ z < LENGTH e /\ ~(x' = y') /\
      (!a b. ~(a = b)  ==> ~(FST (EL a e) = FST (EL b e))) /\ ~NULL (SND (EL z e)) /\  
      (!k x y. x < LENGTH k /\ y < LENGTH k /\ (!j. MEM j k ==> MEM j l \/ ?q. (MEM q e /\ MEM j (SND q))) ==>
      if ((EL x (k:(((A)list) list)) = EL x' l) /\ (EL y k = EL y' l)) then
      	 (HD (zsyn_conjun_intro k x y) = FST (EL z e))
      else
	 (!a. MEM a e ==> ~(FST a = HD (zsyn_conjun_intro k x y))))
      ==> ((zsyn_deduct l e) = (zsyn_delet (APPEND l (SND (EL z e))) x' y'))`;;

e (REPEAT GEN_TAC);;
e (REPEAT STRIP_TAC);;
e (REWRITE_TAC [zsyn_deduct]);;
e (SUBGOAL_THEN `(zsyn_deduct_recurs l e (LENGTH l - 1) (LENGTH l - 1) 
  	    (LENGTH (e:((((A)list) # ((A)list) list) list))) = (T,(zsyn_delet (APPEND l (SND (EL z e))) x' y')))` ASSUME_TAC);;
      e (MATCH_MP_TAC Z_DED_MATCH_THM);;
      e (ASM_SIMP_TAC []);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (CONJ_TAC);;
      e (ASM_ARITH_TAC);;
      e (ASM_ARITH_TAC);;

e (ASM_SIMP_TAC []);;

let Z_DEDUCTION_THM = top_thm ();;

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