(****************************
  This file was automatically generated by Rewrite v1.9.0.

    Brief User Guide to This File

In order to understand the main results shown in this file, it is
sufficient to consider a few definitions and lemmata, only.  We list the
most relevant ones below.  These form a self-contained part of this file,
i.e. there are no references to the other parts, except in the proofs.

* terms definition (Search for "Inductive term")
  This is the set of all terms, inductively defined through constructors.
  Constructors names are prefixed with h_ to avoid clashes.

* term rewriting relation definition (Search for "Inductive R", RC, RCs)
  We actually define three relations between terms: R, RC, RCS.
  Given a set of rewriting rules of the form t1 => t2 ,
     R relates all the variable instantiations of t1 and t2
     RC is the closure of R under ground term contexts and reflexivity
     RCs is the reflexive transitive closure of RC .
  The last one, RCs, is the usual term rewriting relation.

* tree automaton (Search for "User Input Automaton")
  We define the languages for all the automaton states.  Their names are
  prefixed with "O_" to avoid clashes.  Note that here we close the
  languages under intersection contraints and rewritings (RCs).

* unreachability results (Search for "Unreachability")
  These lemmata correspond to the full rules of the form
    | @a : f(X,...,Y) => @zzResult : !FAIL! .
  and prove that f(X,...,Y) is indeed not reachable from @a, for all values
  of X,...,Y.  The number of variables X,...,Y can be zero.

 ****************************)
(* Terms, inductively defined through constructors *)
Inductive term : Set :=
   | h_zi : term -> term 
   | h_ziFAILzi : term 
   | h_zt : term -> term -> term 
   | h_1 : term 
   | h_zc : term -> term -> term 
   | h_a : term 
   | h_b : term 
   | h_cons : term -> term -> term 
   | h_dec : term -> term -> term 
   | h_enc : term -> term -> term 
   | h_fst : term -> term 
   | h_g : term 
   | h_k1 : term 
   | h_k2 : term 
   | h_m : term 
   | h_next : term -> term 
   | h_seed : term 
   | h_snd : term -> term 
.
(* The type of the languages of the automaton states, i.e. a set of
   terms. *)
Definition St := term -> Prop .
(****************************
  The Completed Tree Automaton (approximation result)
 ****************************)
Inductive T_zaziInters : St :=
with T_zazzzzResult : St :=
with T_zr0 : St :=
   | T_T_0 : forall x1 x2, T_zr1 x1 -> T_zr12 x2 -> T_zr0 (h_zc x1 x2)
with T_zr1 : St :=
   | T_T_1 : T_zr1 h_g 
with T_zr10 : St :=
   | T_T_2 : forall x1, T_zr4 x1 -> T_zr10 x1   
   | T_T_3 : forall x1 x2, T_zr1 x1 -> T_zr6 x2 -> T_zr10 (h_zc x1 x2)
   | T_T_4 : forall x1 x2, T_zanet1 x1 -> T_zr11 x2 -> T_zr10 (h_dec x1 x2)
with T_zr11 : St :=
   | T_T_5 : T_zr11 h_k2 
with T_zr12 : St :=
   | T_T_6 : T_zr12 h_a 
with T_zr3 : St :=
   | T_T_7 : T_zr3 h_k1 
with T_zr4 : St :=
   | T_T_8 : forall x1 x2, T_zr1 x1 -> T_zr6 x2 -> T_zr4 (h_zc x1 x2)
with T_zr6 : St :=
   | T_T_9 : T_zr6 h_b 
with T_zr8 : St :=
   | T_T_10 : T_zr8 h_m 
with T_zr9 : St :=
   | T_T_11 : forall x1 x2, T_zr1 x1 -> T_zS0051 x2 -> T_zr9 (h_zc x1 x2)
   | T_T_12 : forall x1 x2, T_zr10 x1 -> T_zr12 x2 -> T_zr9 (h_zc x1 x2)
with T_zanet1 : St :=
   | T_T_13 : forall x1, T_zanet1 x1 -> T_zanet1 x1   
   | T_T_14 : forall x1, T_zanonce x1 -> T_zanet1 x1   
   | T_T_15 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet1 (h_cons x1 x2)
   | T_T_16 : forall x1, T_zanet1 x1 -> T_zanet1 (h_zi x1)
   | T_T_17 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet1 (h_zt x1 x2)
   | T_T_18 : T_zanet1 h_1 
   | T_T_19 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet1 (h_zc x1 x2)
   | T_T_20 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet1 (h_dec x1 x2)
   | T_T_21 : forall x1 x2, T_zr0 x1 -> T_zr3 x2 -> T_zanet1 (h_enc x1 x2)
   | T_T_22 : forall x1 x2, T_zr4 x1 -> T_zr11 x2 -> T_zanet1 (h_enc x1 x2)
   | T_T_23 : forall x1 x2, T_zr8 x1 -> T_zr9 x2 -> T_zanet1 (h_enc x1 x2)
   | T_T_24 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet1 (h_enc x1 x2)
   | T_T_25 : forall x1, T_zanet1 x1 -> T_zanet1 (h_fst x1)
   | T_T_26 : T_zanet1 h_g 
   | T_T_27 : forall x1, T_zanonce x1 -> T_zanet1 (h_next x1)
   | T_T_28 : T_zanet1 h_seed 
   | T_T_29 : forall x1, T_zanet1 x1 -> T_zanet1 (h_snd x1)
with T_zanet2 : St :=
   | T_T_30 : forall x1, T_zr0 x1 -> T_zanet2 x1   
   | T_T_31 : forall x1, T_zr4 x1 -> T_zanet2 x1   
   | T_T_32 : forall x1, T_zanet1 x1 -> T_zanet2 x1   
   | T_T_33 : forall x1, T_zanet2 x1 -> T_zanet2 x1   
   | T_T_34 : forall x1, T_zanonce x1 -> T_zanet2 x1   
   | T_T_35 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet2 (h_cons x1 x2)
   | T_T_36 : forall x1 x2, T_zanet2 x1 -> T_zanet2 x2 -> T_zanet2 (h_cons x1 x2)
   | T_T_37 : forall x1, T_zanet1 x1 -> T_zanet2 (h_zi x1)
   | T_T_38 : forall x1, T_zanet2 x1 -> T_zanet2 (h_zi x1)
   | T_T_39 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet2 (h_zt x1 x2)
   | T_T_40 : forall x1 x2, T_zanet1 x1 -> T_zanet2 x2 -> T_zanet2 (h_zt x1 x2)
   | T_T_41 : forall x1 x2, T_zanet2 x1 -> T_zanet1 x2 -> T_zanet2 (h_zt x1 x2)
   | T_T_42 : forall x1 x2, T_zanet2 x1 -> T_zanet2 x2 -> T_zanet2 (h_zt x1 x2)
   | T_T_43 : T_zanet2 h_1 
   | T_T_44 : forall x1 x2, T_zr1 x1 -> T_zr12 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_45 : forall x1 x2, T_zr1 x1 -> T_zr6 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_46 : forall x1 x2, T_zr1 x1 -> T_zS0052 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_47 : forall x1 x2, T_zr1 x1 -> T_zS0054 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_48 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_49 : forall x1 x2, T_zanet1 x1 -> T_zanet2 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_50 : forall x1 x2, T_zanet2 x1 -> T_zanet2 x2 -> T_zanet2 (h_zc x1 x2)
   | T_T_51 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet2 (h_dec x1 x2)
   | T_T_52 : forall x1 x2, T_zanet2 x1 -> T_zanet2 x2 -> T_zanet2 (h_dec x1 x2)
   | T_T_53 : forall x1 x2, T_zr0 x1 -> T_zr3 x2 -> T_zanet2 (h_enc x1 x2)
   | T_T_54 : forall x1 x2, T_zr4 x1 -> T_zr11 x2 -> T_zanet2 (h_enc x1 x2)
   | T_T_55 : forall x1 x2, T_zr8 x1 -> T_zr9 x2 -> T_zanet2 (h_enc x1 x2)
   | T_T_56 : forall x1 x2, T_zanet1 x1 -> T_zanet1 x2 -> T_zanet2 (h_enc x1 x2)
   | T_T_57 : forall x1 x2, T_zanet2 x1 -> T_zanet2 x2 -> T_zanet2 (h_enc x1 x2)
   | T_T_58 : forall x1, T_zanet1 x1 -> T_zanet2 (h_fst x1)
   | T_T_59 : forall x1, T_zanet2 x1 -> T_zanet2 (h_fst x1)
   | T_T_60 : T_zanet2 h_g 
   | T_T_61 : T_zanet2 h_k1 
   | T_T_62 : T_zanet2 h_k2 
   | T_T_63 : forall x1, T_zanonce x1 -> T_zanet2 (h_next x1)
   | T_T_64 : T_zanet2 h_seed 
   | T_T_65 : forall x1, T_zanet1 x1 -> T_zanet2 (h_snd x1)
   | T_T_66 : forall x1, T_zanet2 x1 -> T_zanet2 (h_snd x1)
with T_zanonce : St :=
   | T_T_67 : forall x1, T_zanonce x1 -> T_zanonce (h_next x1)
   | T_T_68 : T_zanonce h_seed 
with T_zS0051 : St :=
   | T_T_69 : forall x1 x2, T_zr12 x1 -> T_zr6 x2 -> T_zS0051 (h_zt x1 x2)
   | T_T_70 : forall x1 x2, T_zr6 x1 -> T_zr12 x2 -> T_zS0051 (h_zt x1 x2)
with T_zS0052 : St :=
   | T_T_71 : forall x1, T_zr12 x1 -> T_zS0052 x1   
   | T_T_72 : forall x1, T_zS0052 x1 -> T_zS0052 x1   
   | T_T_73 : forall x1, T_zS0053 x1 -> T_zS0052 x1   
   | T_T_74 : forall x1 x2, T_zr12 x1 -> T_zanet1 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_75 : forall x1 x2, T_zr12 x1 -> T_zanet2 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_76 : forall x1 x2, T_zanet1 x1 -> T_zr12 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_77 : forall x1 x2, T_zanet1 x1 -> T_zS0052 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_78 : forall x1 x2, T_zanet1 x1 -> T_zS0053 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_79 : forall x1 x2, T_zanet2 x1 -> T_zr12 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_80 : forall x1 x2, T_zanet2 x1 -> T_zS0052 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_81 : forall x1 x2, T_zanet2 x1 -> T_zS0053 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_82 : forall x1 x2, T_zS0052 x1 -> T_zanet1 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_83 : forall x1 x2, T_zS0052 x1 -> T_zanet2 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_84 : forall x1 x2, T_zS0053 x1 -> T_zanet1 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_85 : forall x1 x2, T_zS0053 x1 -> T_zanet2 x2 -> T_zS0052 (h_zt x1 x2)
   | T_T_86 : T_zS0052 h_a 
with T_zS0053 : St :=
   | T_T_87 : forall x1, T_zr12 x1 -> T_zS0053 x1   
   | T_T_88 : forall x1, T_zS0053 x1 -> T_zS0053 x1   
   | T_T_89 : forall x1 x2, T_zr12 x1 -> T_zanet1 x2 -> T_zS0053 (h_zt x1 x2)
   | T_T_90 : forall x1 x2, T_zanet1 x1 -> T_zr12 x2 -> T_zS0053 (h_zt x1 x2)
   | T_T_91 : forall x1 x2, T_zanet1 x1 -> T_zS0053 x2 -> T_zS0053 (h_zt x1 x2)
   | T_T_92 : forall x1 x2, T_zS0053 x1 -> T_zanet1 x2 -> T_zS0053 (h_zt x1 x2)
   | T_T_93 : T_zS0053 h_a 
with T_zS0054 : St :=
   | T_T_94 : forall x1, T_zr6 x1 -> T_zS0054 x1   
   | T_T_95 : forall x1, T_zS0054 x1 -> T_zS0054 x1   
   | T_T_96 : forall x1, T_zS0055 x1 -> T_zS0054 x1   
   | T_T_97 : forall x1 x2, T_zr6 x1 -> T_zanet1 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_98 : forall x1 x2, T_zr6 x1 -> T_zanet2 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_99 : forall x1 x2, T_zanet1 x1 -> T_zr6 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_100 : forall x1 x2, T_zanet1 x1 -> T_zS0054 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_101 : forall x1 x2, T_zanet1 x1 -> T_zS0055 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_102 : forall x1 x2, T_zanet2 x1 -> T_zr6 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_103 : forall x1 x2, T_zanet2 x1 -> T_zS0054 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_104 : forall x1 x2, T_zanet2 x1 -> T_zS0055 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_105 : forall x1 x2, T_zS0054 x1 -> T_zanet1 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_106 : forall x1 x2, T_zS0054 x1 -> T_zanet2 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_107 : forall x1 x2, T_zS0055 x1 -> T_zanet1 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_108 : forall x1 x2, T_zS0055 x1 -> T_zanet2 x2 -> T_zS0054 (h_zt x1 x2)
   | T_T_109 : T_zS0054 h_b 
with T_zS0055 : St :=
   | T_T_110 : forall x1, T_zr6 x1 -> T_zS0055 x1   
   | T_T_111 : forall x1, T_zS0055 x1 -> T_zS0055 x1   
   | T_T_112 : forall x1 x2, T_zr6 x1 -> T_zanet1 x2 -> T_zS0055 (h_zt x1 x2)
   | T_T_113 : forall x1 x2, T_zanet1 x1 -> T_zr6 x2 -> T_zS0055 (h_zt x1 x2)
   | T_T_114 : forall x1 x2, T_zanet1 x1 -> T_zS0055 x2 -> T_zS0055 (h_zt x1 x2)
   | T_T_115 : forall x1 x2, T_zS0055 x1 -> T_zanet1 x2 -> T_zS0055 (h_zt x1 x2)
   | T_T_116 : T_zS0055 h_b 
.
(****************************
  Completed Automaton, with direct transitions removed
 ****************************)
Inductive N_zaziInters : St :=
with N_zazzzzResult : St :=
with N_zr0 : St :=
   | T_N_117 : forall x1 x2, N_zr1 x1 -> N_zr12 x2 -> N_zr0 (h_zc x1 x2)
with N_zr1 : St :=
   | T_N_118 : N_zr1 h_g 
with N_zr10 : St :=
(* | T_N_119 : forall x1, N_zr4 x1 -> N_zr10 x1    *)
   | T_N_120 : forall x1 x2, N_zr1 x1 -> N_zr6 x2 -> N_zr10 (h_zc x1 x2)
   | T_N_121 : forall x1 x2, N_zanet1 x1 -> N_zr11 x2 -> N_zr10 (h_dec x1 x2)
with N_zr11 : St :=
   | T_N_122 : N_zr11 h_k2 
with N_zr12 : St :=
   | T_N_123 : N_zr12 h_a 
with N_zr3 : St :=
   | T_N_124 : N_zr3 h_k1 
with N_zr4 : St :=
   | T_N_125 : forall x1 x2, N_zr1 x1 -> N_zr6 x2 -> N_zr4 (h_zc x1 x2)
with N_zr6 : St :=
   | T_N_126 : N_zr6 h_b 
with N_zr8 : St :=
   | T_N_127 : N_zr8 h_m 
with N_zr9 : St :=
   | T_N_128 : forall x1 x2, N_zr1 x1 -> N_zS0051 x2 -> N_zr9 (h_zc x1 x2)
   | T_N_129 : forall x1 x2, N_zr10 x1 -> N_zr12 x2 -> N_zr9 (h_zc x1 x2)
with N_zanet1 : St :=
(* | T_N_130 : forall x1, N_zanet1 x1 -> N_zanet1 x1    *)
(* | T_N_131 : forall x1, N_zanonce x1 -> N_zanet1 x1    *)
   | T_N_132 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet1 (h_cons x1 x2)
   | T_N_133 : forall x1, N_zanet1 x1 -> N_zanet1 (h_zi x1)
   | T_N_134 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet1 (h_zt x1 x2)
   | T_N_135 : N_zanet1 h_1 
   | T_N_136 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet1 (h_zc x1 x2)
   | T_N_137 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet1 (h_dec x1 x2)
   | T_N_138 : forall x1 x2, N_zr0 x1 -> N_zr3 x2 -> N_zanet1 (h_enc x1 x2)
   | T_N_139 : forall x1 x2, N_zr4 x1 -> N_zr11 x2 -> N_zanet1 (h_enc x1 x2)
   | T_N_140 : forall x1 x2, N_zr8 x1 -> N_zr9 x2 -> N_zanet1 (h_enc x1 x2)
   | T_N_141 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet1 (h_enc x1 x2)
   | T_N_142 : forall x1, N_zanet1 x1 -> N_zanet1 (h_fst x1)
   | T_N_143 : N_zanet1 h_g 
   | T_N_144 : forall x1, N_zanonce x1 -> N_zanet1 (h_next x1)
   | T_N_145 : N_zanet1 h_seed 
   | T_N_146 : forall x1, N_zanet1 x1 -> N_zanet1 (h_snd x1)
with N_zanet2 : St :=
(* | T_N_147 : forall x1, N_zr0 x1 -> N_zanet2 x1    *)
(* | T_N_148 : forall x1, N_zr4 x1 -> N_zanet2 x1    *)
(* | T_N_149 : forall x1, N_zanet1 x1 -> N_zanet2 x1    *)
(* | T_N_150 : forall x1, N_zanet2 x1 -> N_zanet2 x1    *)
(* | T_N_151 : forall x1, N_zanonce x1 -> N_zanet2 x1    *)
   | T_N_152 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet2 (h_cons x1 x2)
   | T_N_153 : forall x1 x2, N_zanet2 x1 -> N_zanet2 x2 -> N_zanet2 (h_cons x1 x2)
   | T_N_154 : forall x1, N_zanet1 x1 -> N_zanet2 (h_zi x1)
   | T_N_155 : forall x1, N_zanet2 x1 -> N_zanet2 (h_zi x1)
   | T_N_156 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet2 (h_zt x1 x2)
   | T_N_157 : forall x1 x2, N_zanet1 x1 -> N_zanet2 x2 -> N_zanet2 (h_zt x1 x2)
   | T_N_158 : forall x1 x2, N_zanet2 x1 -> N_zanet1 x2 -> N_zanet2 (h_zt x1 x2)
   | T_N_159 : forall x1 x2, N_zanet2 x1 -> N_zanet2 x2 -> N_zanet2 (h_zt x1 x2)
   | T_N_160 : N_zanet2 h_1 
   | T_N_161 : forall x1 x2, N_zr1 x1 -> N_zr12 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_162 : forall x1 x2, N_zr1 x1 -> N_zr6 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_163 : forall x1 x2, N_zr1 x1 -> N_zS0052 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_164 : forall x1 x2, N_zr1 x1 -> N_zS0054 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_165 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_166 : forall x1 x2, N_zanet1 x1 -> N_zanet2 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_167 : forall x1 x2, N_zanet2 x1 -> N_zanet2 x2 -> N_zanet2 (h_zc x1 x2)
   | T_N_168 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet2 (h_dec x1 x2)
   | T_N_169 : forall x1 x2, N_zanet2 x1 -> N_zanet2 x2 -> N_zanet2 (h_dec x1 x2)
   | T_N_170 : forall x1 x2, N_zr0 x1 -> N_zr3 x2 -> N_zanet2 (h_enc x1 x2)
   | T_N_171 : forall x1 x2, N_zr4 x1 -> N_zr11 x2 -> N_zanet2 (h_enc x1 x2)
   | T_N_172 : forall x1 x2, N_zr8 x1 -> N_zr9 x2 -> N_zanet2 (h_enc x1 x2)
   | T_N_173 : forall x1 x2, N_zanet1 x1 -> N_zanet1 x2 -> N_zanet2 (h_enc x1 x2)
   | T_N_174 : forall x1 x2, N_zanet2 x1 -> N_zanet2 x2 -> N_zanet2 (h_enc x1 x2)
   | T_N_175 : forall x1, N_zanet1 x1 -> N_zanet2 (h_fst x1)
   | T_N_176 : forall x1, N_zanet2 x1 -> N_zanet2 (h_fst x1)
   | T_N_177 : N_zanet2 h_g 
   | T_N_178 : N_zanet2 h_k1 
   | T_N_179 : N_zanet2 h_k2 
   | T_N_180 : forall x1, N_zanonce x1 -> N_zanet2 (h_next x1)
   | T_N_181 : N_zanet2 h_seed 
   | T_N_182 : forall x1, N_zanet1 x1 -> N_zanet2 (h_snd x1)
   | T_N_183 : forall x1, N_zanet2 x1 -> N_zanet2 (h_snd x1)
with N_zanonce : St :=
   | T_N_184 : forall x1, N_zanonce x1 -> N_zanonce (h_next x1)
   | T_N_185 : N_zanonce h_seed 
with N_zS0051 : St :=
   | T_N_186 : forall x1 x2, N_zr12 x1 -> N_zr6 x2 -> N_zS0051 (h_zt x1 x2)
   | T_N_187 : forall x1 x2, N_zr6 x1 -> N_zr12 x2 -> N_zS0051 (h_zt x1 x2)
with N_zS0052 : St :=
(* | T_N_188 : forall x1, N_zr12 x1 -> N_zS0052 x1    *)
(* | T_N_189 : forall x1, N_zS0052 x1 -> N_zS0052 x1    *)
(* | T_N_190 : forall x1, N_zS0053 x1 -> N_zS0052 x1    *)
   | T_N_191 : forall x1 x2, N_zr12 x1 -> N_zanet1 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_192 : forall x1 x2, N_zr12 x1 -> N_zanet2 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_193 : forall x1 x2, N_zanet1 x1 -> N_zr12 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_194 : forall x1 x2, N_zanet1 x1 -> N_zS0052 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_195 : forall x1 x2, N_zanet1 x1 -> N_zS0053 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_196 : forall x1 x2, N_zanet2 x1 -> N_zr12 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_197 : forall x1 x2, N_zanet2 x1 -> N_zS0052 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_198 : forall x1 x2, N_zanet2 x1 -> N_zS0053 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_199 : forall x1 x2, N_zS0052 x1 -> N_zanet1 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_200 : forall x1 x2, N_zS0052 x1 -> N_zanet2 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_201 : forall x1 x2, N_zS0053 x1 -> N_zanet1 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_202 : forall x1 x2, N_zS0053 x1 -> N_zanet2 x2 -> N_zS0052 (h_zt x1 x2)
   | T_N_203 : N_zS0052 h_a 
with N_zS0053 : St :=
(* | T_N_204 : forall x1, N_zr12 x1 -> N_zS0053 x1    *)
(* | T_N_205 : forall x1, N_zS0053 x1 -> N_zS0053 x1    *)
   | T_N_206 : forall x1 x2, N_zr12 x1 -> N_zanet1 x2 -> N_zS0053 (h_zt x1 x2)
   | T_N_207 : forall x1 x2, N_zanet1 x1 -> N_zr12 x2 -> N_zS0053 (h_zt x1 x2)
   | T_N_208 : forall x1 x2, N_zanet1 x1 -> N_zS0053 x2 -> N_zS0053 (h_zt x1 x2)
   | T_N_209 : forall x1 x2, N_zS0053 x1 -> N_zanet1 x2 -> N_zS0053 (h_zt x1 x2)
   | T_N_210 : N_zS0053 h_a 
with N_zS0054 : St :=
(* | T_N_211 : forall x1, N_zr6 x1 -> N_zS0054 x1    *)
(* | T_N_212 : forall x1, N_zS0054 x1 -> N_zS0054 x1    *)
(* | T_N_213 : forall x1, N_zS0055 x1 -> N_zS0054 x1    *)
   | T_N_214 : forall x1 x2, N_zr6 x1 -> N_zanet1 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_215 : forall x1 x2, N_zr6 x1 -> N_zanet2 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_216 : forall x1 x2, N_zanet1 x1 -> N_zr6 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_217 : forall x1 x2, N_zanet1 x1 -> N_zS0054 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_218 : forall x1 x2, N_zanet1 x1 -> N_zS0055 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_219 : forall x1 x2, N_zanet2 x1 -> N_zr6 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_220 : forall x1 x2, N_zanet2 x1 -> N_zS0054 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_221 : forall x1 x2, N_zanet2 x1 -> N_zS0055 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_222 : forall x1 x2, N_zS0054 x1 -> N_zanet1 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_223 : forall x1 x2, N_zS0054 x1 -> N_zanet2 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_224 : forall x1 x2, N_zS0055 x1 -> N_zanet1 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_225 : forall x1 x2, N_zS0055 x1 -> N_zanet2 x2 -> N_zS0054 (h_zt x1 x2)
   | T_N_226 : N_zS0054 h_b 
with N_zS0055 : St :=
(* | T_N_227 : forall x1, N_zr6 x1 -> N_zS0055 x1    *)
(* | T_N_228 : forall x1, N_zS0055 x1 -> N_zS0055 x1    *)
   | T_N_229 : forall x1 x2, N_zr6 x1 -> N_zanet1 x2 -> N_zS0055 (h_zt x1 x2)
   | T_N_230 : forall x1 x2, N_zanet1 x1 -> N_zr6 x2 -> N_zS0055 (h_zt x1 x2)
   | T_N_231 : forall x1 x2, N_zanet1 x1 -> N_zS0055 x2 -> N_zS0055 (h_zt x1 x2)
   | T_N_232 : forall x1 x2, N_zS0055 x1 -> N_zanet1 x2 -> N_zS0055 (h_zt x1 x2)
   | T_N_233 : N_zS0055 h_b 
.
(* Table of the states of both automata *)
Inductive State : St -> St -> Prop := 
 | ST_zaziInters : State T_zaziInters N_zaziInters
 | ST_zazzzzResult : State T_zazzzzResult N_zazzzzResult
 | ST_zr0 : State T_zr0 N_zr0
 | ST_zr1 : State T_zr1 N_zr1
 | ST_zr10 : State T_zr10 N_zr10
 | ST_zr11 : State T_zr11 N_zr11
 | ST_zr12 : State T_zr12 N_zr12
 | ST_zr3 : State T_zr3 N_zr3
 | ST_zr4 : State T_zr4 N_zr4
 | ST_zr6 : State T_zr6 N_zr6
 | ST_zr8 : State T_zr8 N_zr8
 | ST_zr9 : State T_zr9 N_zr9
 | ST_zanet1 : State T_zanet1 N_zanet1
 | ST_zanet2 : State T_zanet2 N_zanet2
 | ST_zanonce : State T_zanonce N_zanonce
 | ST_zS0051 : State T_zS0051 N_zS0051
 | ST_zS0052 : State T_zS0052 N_zS0052
 | ST_zS0053 : State T_zS0053 N_zS0053
 | ST_zS0054 : State T_zS0054 N_zS0054
 | ST_zS0055 : State T_zS0055 N_zS0055
.
Definition State_T s_t := exists s_n, State s_t s_n .
Definition State_N s_n := exists s_t, State s_t s_n .
Ltac knownState :=
   match goal with
   | |- State_T _ => solve [ exists N_zaziInters ; apply ST_zaziInters | exists N_zazzzzResult ; apply ST_zazzzzResult | exists N_zr0 ; apply ST_zr0 | exists N_zr1 ; apply ST_zr1 | exists N_zr10 ; apply ST_zr10 | exists N_zr11 ; apply ST_zr11 | exists N_zr12 ; apply ST_zr12 | exists N_zr3 ; apply ST_zr3 | exists N_zr4 ; apply ST_zr4 | exists N_zr6 ; apply ST_zr6 | exists N_zr8 ; apply ST_zr8 | exists N_zr9 ; apply ST_zr9 | exists N_zanet1 ; apply ST_zanet1 | exists N_zanet2 ; apply ST_zanet2 | exists N_zanonce ; apply ST_zanonce | exists N_zS0051 ; apply ST_zS0051 | exists N_zS0052 ; apply ST_zS0052 | exists N_zS0053 ; apply ST_zS0053 | exists N_zS0054 ; apply ST_zS0054 | exists N_zS0055 ; apply ST_zS0055 ]
   | |- State_N _ => solve [ exists T_zaziInters ; apply ST_zaziInters | exists T_zazzzzResult ; apply ST_zazzzzResult | exists T_zr0 ; apply ST_zr0 | exists T_zr1 ; apply ST_zr1 | exists T_zr10 ; apply ST_zr10 | exists T_zr11 ; apply ST_zr11 | exists T_zr12 ; apply ST_zr12 | exists T_zr3 ; apply ST_zr3 | exists T_zr4 ; apply ST_zr4 | exists T_zr6 ; apply ST_zr6 | exists T_zr8 ; apply ST_zr8 | exists T_zr9 ; apply ST_zr9 | exists T_zanet1 ; apply ST_zanet1 | exists T_zanet2 ; apply ST_zanet2 | exists T_zanonce ; apply ST_zanonce | exists T_zS0051 ; apply ST_zS0051 | exists T_zS0052 ; apply ST_zS0052 | exists T_zS0053 ; apply ST_zS0053 | exists T_zS0054 ; apply ST_zS0054 | exists T_zS0055 ; apply ST_zS0055 ]
   end .
Ltac apply_transitionsT_tac tac :=
   intros ; try assumption ; first [
    apply T_T_0 ; try assumption ; tac
  | apply T_T_1 ; try assumption ; tac
  | apply T_T_10 ; try assumption ; tac
  | apply T_T_100 ; try assumption ; tac
  | apply T_T_101 ; try assumption ; tac
  | apply T_T_102 ; try assumption ; tac
  | apply T_T_103 ; try assumption ; tac
  | apply T_T_104 ; try assumption ; tac
  | apply T_T_105 ; try assumption ; tac
  | apply T_T_106 ; try assumption ; tac
  | apply T_T_107 ; try assumption ; tac
  | apply T_T_108 ; try assumption ; tac
  | apply T_T_109 ; try assumption ; tac
  | apply T_T_11 ; try assumption ; tac
  | apply T_T_112 ; try assumption ; tac
  | apply T_T_113 ; try assumption ; tac
  | apply T_T_114 ; try assumption ; tac
  | apply T_T_115 ; try assumption ; tac
  | apply T_T_116 ; try assumption ; tac
  | apply T_T_12 ; try assumption ; tac
  | apply T_T_15 ; try assumption ; tac
  | apply T_T_16 ; try assumption ; tac
  | apply T_T_17 ; try assumption ; tac
  | apply T_T_18 ; try assumption ; tac
  | apply T_T_19 ; try assumption ; tac
  | apply T_T_20 ; try assumption ; tac
  | apply T_T_21 ; try assumption ; tac
  | apply T_T_22 ; try assumption ; tac
  | apply T_T_23 ; try assumption ; tac
  | apply T_T_24 ; try assumption ; tac
  | apply T_T_25 ; try assumption ; tac
  | apply T_T_26 ; try assumption ; tac
  | apply T_T_27 ; try assumption ; tac
  | apply T_T_28 ; try assumption ; tac
  | apply T_T_29 ; try assumption ; tac
  | apply T_T_3 ; try assumption ; tac
  | apply T_T_35 ; try assumption ; tac
  | apply T_T_36 ; try assumption ; tac
  | apply T_T_37 ; try assumption ; tac
  | apply T_T_38 ; try assumption ; tac
  | apply T_T_39 ; try assumption ; tac
  | apply T_T_4 ; try assumption ; tac
  | apply T_T_40 ; try assumption ; tac
  | apply T_T_41 ; try assumption ; tac
  | apply T_T_42 ; try assumption ; tac
  | apply T_T_43 ; try assumption ; tac
  | apply T_T_44 ; try assumption ; tac
  | apply T_T_45 ; try assumption ; tac
  | apply T_T_46 ; try assumption ; tac
  | apply T_T_47 ; try assumption ; tac
  | apply T_T_48 ; try assumption ; tac
  | apply T_T_49 ; try assumption ; tac
  | apply T_T_5 ; try assumption ; tac
  | apply T_T_50 ; try assumption ; tac
  | apply T_T_51 ; try assumption ; tac
  | apply T_T_52 ; try assumption ; tac
  | apply T_T_53 ; try assumption ; tac
  | apply T_T_54 ; try assumption ; tac
  | apply T_T_55 ; try assumption ; tac
  | apply T_T_56 ; try assumption ; tac
  | apply T_T_57 ; try assumption ; tac
  | apply T_T_58 ; try assumption ; tac
  | apply T_T_59 ; try assumption ; tac
  | apply T_T_6 ; try assumption ; tac
  | apply T_T_60 ; try assumption ; tac
  | apply T_T_61 ; try assumption ; tac
  | apply T_T_62 ; try assumption ; tac
  | apply T_T_63 ; try assumption ; tac
  | apply T_T_64 ; try assumption ; tac
  | apply T_T_65 ; try assumption ; tac
  | apply T_T_66 ; try assumption ; tac
  | apply T_T_67 ; try assumption ; tac
  | apply T_T_68 ; try assumption ; tac
  | apply T_T_69 ; try assumption ; tac
  | apply T_T_7 ; try assumption ; tac
  | apply T_T_70 ; try assumption ; tac
  | apply T_T_74 ; try assumption ; tac
  | apply T_T_75 ; try assumption ; tac
  | apply T_T_76 ; try assumption ; tac
  | apply T_T_77 ; try assumption ; tac
  | apply T_T_78 ; try assumption ; tac
  | apply T_T_79 ; try assumption ; tac
  | apply T_T_8 ; try assumption ; tac
  | apply T_T_80 ; try assumption ; tac
  | apply T_T_81 ; try assumption ; tac
  | apply T_T_82 ; try assumption ; tac
  | apply T_T_83 ; try assumption ; tac
  | apply T_T_84 ; try assumption ; tac
  | apply T_T_85 ; try assumption ; tac
  | apply T_T_86 ; try assumption ; tac
  | apply T_T_89 ; try assumption ; tac
  | apply T_T_9 ; try assumption ; tac
  | apply T_T_90 ; try assumption ; tac
  | apply T_T_91 ; try assumption ; tac
  | apply T_T_92 ; try assumption ; tac
  | apply T_T_93 ; try assumption ; tac
  | apply T_T_97 ; try assumption ; tac
  | apply T_T_98 ; try assumption ; tac
  | apply T_T_99 ; try assumption ; tac
    ] .
Ltac apply_transitionsT_once :=
   apply_transitionsT_tac fail .
Ltac apply_transitionsT_rec :=
   idtac ; apply_transitionsT_tac apply_transitionsT_rec .
Ltac apply_transitionsN_tac tac :=
   intros ; try assumption ; first [
    apply T_N_117 ; try assumption ; tac
  | apply T_N_118 ; try assumption ; tac
  | apply T_N_120 ; try assumption ; tac
  | apply T_N_121 ; try assumption ; tac
  | apply T_N_122 ; try assumption ; tac
  | apply T_N_123 ; try assumption ; tac
  | apply T_N_124 ; try assumption ; tac
  | apply T_N_125 ; try assumption ; tac
  | apply T_N_126 ; try assumption ; tac
  | apply T_N_127 ; try assumption ; tac
  | apply T_N_128 ; try assumption ; tac
  | apply T_N_129 ; try assumption ; tac
  | apply T_N_132 ; try assumption ; tac
  | apply T_N_133 ; try assumption ; tac
  | apply T_N_134 ; try assumption ; tac
  | apply T_N_135 ; try assumption ; tac
  | apply T_N_136 ; try assumption ; tac
  | apply T_N_137 ; try assumption ; tac
  | apply T_N_138 ; try assumption ; tac
  | apply T_N_139 ; try assumption ; tac
  | apply T_N_140 ; try assumption ; tac
  | apply T_N_141 ; try assumption ; tac
  | apply T_N_142 ; try assumption ; tac
  | apply T_N_143 ; try assumption ; tac
  | apply T_N_144 ; try assumption ; tac
  | apply T_N_145 ; try assumption ; tac
  | apply T_N_146 ; try assumption ; tac
  | apply T_N_152 ; try assumption ; tac
  | apply T_N_153 ; try assumption ; tac
  | apply T_N_154 ; try assumption ; tac
  | apply T_N_155 ; try assumption ; tac
  | apply T_N_156 ; try assumption ; tac
  | apply T_N_157 ; try assumption ; tac
  | apply T_N_158 ; try assumption ; tac
  | apply T_N_159 ; try assumption ; tac
  | apply T_N_160 ; try assumption ; tac
  | apply T_N_161 ; try assumption ; tac
  | apply T_N_162 ; try assumption ; tac
  | apply T_N_163 ; try assumption ; tac
  | apply T_N_164 ; try assumption ; tac
  | apply T_N_165 ; try assumption ; tac
  | apply T_N_166 ; try assumption ; tac
  | apply T_N_167 ; try assumption ; tac
  | apply T_N_168 ; try assumption ; tac
  | apply T_N_169 ; try assumption ; tac
  | apply T_N_170 ; try assumption ; tac
  | apply T_N_171 ; try assumption ; tac
  | apply T_N_172 ; try assumption ; tac
  | apply T_N_173 ; try assumption ; tac
  | apply T_N_174 ; try assumption ; tac
  | apply T_N_175 ; try assumption ; tac
  | apply T_N_176 ; try assumption ; tac
  | apply T_N_177 ; try assumption ; tac
  | apply T_N_178 ; try assumption ; tac
  | apply T_N_179 ; try assumption ; tac
  | apply T_N_180 ; try assumption ; tac
  | apply T_N_181 ; try assumption ; tac
  | apply T_N_182 ; try assumption ; tac
  | apply T_N_183 ; try assumption ; tac
  | apply T_N_184 ; try assumption ; tac
  | apply T_N_185 ; try assumption ; tac
  | apply T_N_186 ; try assumption ; tac
  | apply T_N_187 ; try assumption ; tac
  | apply T_N_191 ; try assumption ; tac
  | apply T_N_192 ; try assumption ; tac
  | apply T_N_193 ; try assumption ; tac
  | apply T_N_194 ; try assumption ; tac
  | apply T_N_195 ; try assumption ; tac
  | apply T_N_196 ; try assumption ; tac
  | apply T_N_197 ; try assumption ; tac
  | apply T_N_198 ; try assumption ; tac
  | apply T_N_199 ; try assumption ; tac
  | apply T_N_200 ; try assumption ; tac
  | apply T_N_201 ; try assumption ; tac
  | apply T_N_202 ; try assumption ; tac
  | apply T_N_203 ; try assumption ; tac
  | apply T_N_206 ; try assumption ; tac
  | apply T_N_207 ; try assumption ; tac
  | apply T_N_208 ; try assumption ; tac
  | apply T_N_209 ; try assumption ; tac
  | apply T_N_210 ; try assumption ; tac
  | apply T_N_214 ; try assumption ; tac
  | apply T_N_215 ; try assumption ; tac
  | apply T_N_216 ; try assumption ; tac
  | apply T_N_217 ; try assumption ; tac
  | apply T_N_218 ; try assumption ; tac
  | apply T_N_219 ; try assumption ; tac
  | apply T_N_220 ; try assumption ; tac
  | apply T_N_221 ; try assumption ; tac
  | apply T_N_222 ; try assumption ; tac
  | apply T_N_223 ; try assumption ; tac
  | apply T_N_224 ; try assumption ; tac
  | apply T_N_225 ; try assumption ; tac
  | apply T_N_226 ; try assumption ; tac
  | apply T_N_229 ; try assumption ; tac
  | apply T_N_230 ; try assumption ; tac
  | apply T_N_231 ; try assumption ; tac
  | apply T_N_232 ; try assumption ; tac
  | apply T_N_233 ; try assumption ; tac
    ] .
Ltac apply_transitionsN_once :=
   apply_transitionsN_tac fail .
Ltac apply_transitionsN_rec :=
   idtac ; apply_transitionsN_tac apply_transitionsN_rec .
Ltac decomposition_once :=
  match goal with
  | h : ?s (?f _) |- _ => inversion_clear h ; subst
  | h : ?s (?f _ _) |- _ => inversion_clear h ; subst
  (* Here ?x can be either a constant or a variable (representing a
     Label).  A constant could not match with ?s, so we try inversion. *)
  | h : ?s ?x |- _ => inversion h ; fail
  end .
Ltac decomposition := repeat decomposition_once .
Scheme
 Min_T_zaziInters := Minimality for T_zaziInters Sort Prop with
 Min_T_zazzzzResult := Minimality for T_zazzzzResult Sort Prop with
 Min_T_zr0 := Minimality for T_zr0 Sort Prop with
 Min_T_zr1 := Minimality for T_zr1 Sort Prop with
 Min_T_zr10 := Minimality for T_zr10 Sort Prop with
 Min_T_zr11 := Minimality for T_zr11 Sort Prop with
 Min_T_zr12 := Minimality for T_zr12 Sort Prop with
 Min_T_zr3 := Minimality for T_zr3 Sort Prop with
 Min_T_zr4 := Minimality for T_zr4 Sort Prop with
 Min_T_zr6 := Minimality for T_zr6 Sort Prop with
 Min_T_zr8 := Minimality for T_zr8 Sort Prop with
 Min_T_zr9 := Minimality for T_zr9 Sort Prop with
 Min_T_zanet1 := Minimality for T_zanet1 Sort Prop with
 Min_T_zanet2 := Minimality for T_zanet2 Sort Prop with
 Min_T_zanonce := Minimality for T_zanonce Sort Prop with
 Min_T_zS0051 := Minimality for T_zS0051 Sort Prop with
 Min_T_zS0052 := Minimality for T_zS0052 Sort Prop with
 Min_T_zS0053 := Minimality for T_zS0053 Sort Prop with
 Min_T_zS0054 := Minimality for T_zS0054 Sort Prop with
 Min_T_zS0055 := Minimality for T_zS0055 Sort Prop .
Scheme
 Min_N_zaziInters := Minimality for N_zaziInters Sort Prop with
 Min_N_zazzzzResult := Minimality for N_zazzzzResult Sort Prop with
 Min_N_zr0 := Minimality for N_zr0 Sort Prop with
 Min_N_zr1 := Minimality for N_zr1 Sort Prop with
 Min_N_zr10 := Minimality for N_zr10 Sort Prop with
 Min_N_zr11 := Minimality for N_zr11 Sort Prop with
 Min_N_zr12 := Minimality for N_zr12 Sort Prop with
 Min_N_zr3 := Minimality for N_zr3 Sort Prop with
 Min_N_zr4 := Minimality for N_zr4 Sort Prop with
 Min_N_zr6 := Minimality for N_zr6 Sort Prop with
 Min_N_zr8 := Minimality for N_zr8 Sort Prop with
 Min_N_zr9 := Minimality for N_zr9 Sort Prop with
 Min_N_zanet1 := Minimality for N_zanet1 Sort Prop with
 Min_N_zanet2 := Minimality for N_zanet2 Sort Prop with
 Min_N_zanonce := Minimality for N_zanonce Sort Prop with
 Min_N_zS0051 := Minimality for N_zS0051 Sort Prop with
 Min_N_zS0052 := Minimality for N_zS0052 Sort Prop with
 Min_N_zS0053 := Minimality for N_zS0053 Sort Prop with
 Min_N_zS0054 := Minimality for N_zS0054 Sort Prop with
 Min_N_zS0055 := Minimality for N_zS0055 Sort Prop .
Definition Min_sat_T_zaziInters := Min_T_zaziInters N_zaziInters .
Definition Min_sat_T_zazzzzResult := Min_T_zazzzzResult N_zazzzzResult .
Definition Min_sat_T_zr0 := Min_T_zr0 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zr1 := Min_T_zr1 N_zr1 .
Definition Min_sat_T_zr10 := Min_T_zr10 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zr11 := Min_T_zr11 N_zr11 .
Definition Min_sat_T_zr12 := Min_T_zr12 N_zr12 .
Definition Min_sat_T_zr3 := Min_T_zr3 N_zr3 .
Definition Min_sat_T_zr4 := Min_T_zr4 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zr6 := Min_T_zr6 N_zr6 .
Definition Min_sat_T_zr8 := Min_T_zr8 N_zr8 .
Definition Min_sat_T_zr9 := Min_T_zr9 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zanet1 := Min_T_zanet1 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zanet2 := Min_T_zanet2 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zanonce := Min_T_zanonce N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zS0051 := Min_T_zS0051 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zS0052 := Min_T_zS0052 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zS0053 := Min_T_zS0053 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zS0054 := Min_T_zS0054 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_T_zS0055 := Min_T_zS0055 N_zaziInters N_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr3 N_zr4 N_zr6 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zS0051 N_zS0052 N_zS0053 N_zS0054 N_zS0055 .
Definition Min_sat_N_zaziInters := Min_N_zaziInters T_zaziInters .
Definition Min_sat_N_zazzzzResult := Min_N_zazzzzResult T_zazzzzResult .
Definition Min_sat_N_zr0 := Min_N_zr0 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zr1 := Min_N_zr1 T_zr1 .
Definition Min_sat_N_zr10 := Min_N_zr10 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zr11 := Min_N_zr11 T_zr11 .
Definition Min_sat_N_zr12 := Min_N_zr12 T_zr12 .
Definition Min_sat_N_zr3 := Min_N_zr3 T_zr3 .
Definition Min_sat_N_zr4 := Min_N_zr4 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zr6 := Min_N_zr6 T_zr6 .
Definition Min_sat_N_zr8 := Min_N_zr8 T_zr8 .
Definition Min_sat_N_zr9 := Min_N_zr9 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zanet1 := Min_N_zanet1 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zanet2 := Min_N_zanet2 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zanonce := Min_N_zanonce T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zS0051 := Min_N_zS0051 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zS0052 := Min_N_zS0052 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zS0053 := Min_N_zS0053 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zS0054 := Min_N_zS0054 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
Definition Min_sat_N_zS0055 := Min_N_zS0055 T_zaziInters T_zazzzzResult T_zr0 T_zr1 T_zr10 T_zr11 T_zr12 T_zr3 T_zr4 T_zr6 T_zr8 T_zr9 T_zanet1 T_zanet2 T_zanonce T_zS0051 T_zS0052 T_zS0053 T_zS0054 T_zS0055 .
(* For the Rm_trans lemma, we simply apply all the N transitions.
   Of course, this fails when there is no correspondent N transition.
   Here, we intro the minimality Hps and use inversion on the N one,
   so that at least one term head appears. *)
Ltac RmAddTool apply_trans := 
   apply_trans || let x := fresh "x" in
                  let Hs_t := fresh "Hs_t" in
                  let Hs_n := fresh "Hs_n" in
                  intros x Hs_t Hs_n ;
                  inversion Hs_n ; 
                  apply_trans
.
Ltac RmAddTool_T_ := RmAddTool apply_transitionsT_once .
Lemma Add_trans : forall s_t s_n t, State s_t s_n -> s_n t -> s_t t .
Proof.
intros ; inversion H ; subst ;
 [ abstract (idtac "rmadd N_zaziInters" ; apply Min_sat_N_zaziInters ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zazzzzResult" ; apply Min_sat_N_zazzzzResult ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr0" ; apply Min_sat_N_zr0 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr1" ; apply Min_sat_N_zr1 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr10" ; apply Min_sat_N_zr10 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr11" ; apply Min_sat_N_zr11 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr12" ; apply Min_sat_N_zr12 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr3" ; apply Min_sat_N_zr3 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr4" ; apply Min_sat_N_zr4 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr6" ; apply Min_sat_N_zr6 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr8" ; apply Min_sat_N_zr8 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zr9" ; apply Min_sat_N_zr9 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zanet1" ; apply Min_sat_N_zanet1 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zanet2" ; apply Min_sat_N_zanet2 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zanonce" ; apply Min_sat_N_zanonce ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zS0051" ; apply Min_sat_N_zS0051 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zS0052" ; apply Min_sat_N_zS0052 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zS0053" ; apply Min_sat_N_zS0053 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zS0054" ; apply Min_sat_N_zS0054 ; RmAddTool_T_)
 | abstract (idtac "rmadd N_zS0055" ; apply Min_sat_N_zS0055 ; RmAddTool_T_)
 ] .
Save.
Ltac RmAddTool_N_ := RmAddTool apply_transitionsN_once .
Lemma Rm_trans : forall s_t s_n t, State s_t s_n -> s_t t -> s_n t .
Proof.
intros ; inversion H ; subst ;
 [ abstract (idtac "rmadd T_zaziInters" ; apply Min_sat_T_zaziInters ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zazzzzResult" ; apply Min_sat_T_zazzzzResult ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr0" ; apply Min_sat_T_zr0 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr1" ; apply Min_sat_T_zr1 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr10" ; apply Min_sat_T_zr10 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr11" ; apply Min_sat_T_zr11 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr12" ; apply Min_sat_T_zr12 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr3" ; apply Min_sat_T_zr3 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr4" ; apply Min_sat_T_zr4 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr6" ; apply Min_sat_T_zr6 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr8" ; apply Min_sat_T_zr8 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zr9" ; apply Min_sat_T_zr9 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zanet1" ; apply Min_sat_T_zanet1 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zanet2" ; apply Min_sat_T_zanet2 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zanonce" ; apply Min_sat_T_zanonce ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zS0051" ; apply Min_sat_T_zS0051 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zS0052" ; apply Min_sat_T_zS0052 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zS0053" ; apply Min_sat_T_zS0053 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zS0054" ; apply Min_sat_T_zS0054 ; RmAddTool_N_)
 | abstract (idtac "rmadd T_zS0055" ; apply Min_sat_T_zS0055 ; RmAddTool_N_)
 ] .
Save.
(****************************
  Rewriting Relation, _not_ closed under contexts
 ****************************)
Inductive R : term -> term -> Prop :=
 | R_1 :  R (h_zi (h_1))  (h_1)
 | R_2 :  forall V_X , R (h_zi (h_zi V_X))  V_X
 | R_3 :  forall V_X V_Y , R (h_zi (h_zt V_X V_Y))  (h_zt (h_zi V_X) (h_zi V_Y))
 | R_4 :  forall V_X , R (h_zt (h_1) V_X)  V_X
 | R_5 :  forall V_X V_Y V_Z , R (h_zt V_X (h_zt V_Y V_Z))  (h_zt (h_zt V_X V_Y) V_Z)
 | R_6 :  forall V_X V_Y , R (h_zt V_X V_Y)  (h_zt V_Y V_X)
 | R_7 :  forall V_X , R (h_zt V_X (h_zi V_X))  (h_1)
 | R_8 :  forall V_X , R (h_zc (h_1) V_X)  (h_1)
 | R_9 :  forall V_X , R (h_zc V_X (h_1))  V_X
 | R_10 :  forall V_X V_Y V_Z , R (h_zc (h_zc V_X V_Y) V_Z)  (h_zc V_X (h_zt V_Y V_Z))
 | R_11 :  forall V_X V_Y V_Z , R (h_zc (h_zt V_Y V_Z) V_X)  (h_zt (h_zc V_Y V_X) (h_zc V_Z V_X))
 | R_12 :  forall V_X V_Y , R (h_zc (h_zi V_X) V_Y)  (h_zi (h_zc V_X V_Y))
 | R_13 :  forall V_K V_M , R (h_dec (h_enc V_M V_K) V_K)  V_M
 | R_14 :  forall V_X V_Y , R (h_fst (h_cons V_X V_Y))  V_X
 | R_15 :  forall V_X V_Y , R (h_snd (h_cons V_X V_Y))  V_Y
(* Full rule handled later *)
.
Inductive disj : St -> St -> Prop :=
 | D_234 : disj N_zaziInters N_zazzzzResult
 | D_235 : disj N_zaziInters N_zr0
 | D_236 : disj N_zaziInters N_zr1
 | D_237 : disj N_zaziInters N_zr10
 | D_238 : disj N_zaziInters N_zr11
 | D_239 : disj N_zaziInters N_zr12
 | D_240 : disj N_zaziInters N_zr3
 | D_241 : disj N_zaziInters N_zr4
 | D_242 : disj N_zaziInters N_zr6
 | D_243 : disj N_zaziInters N_zr8
 | D_244 : disj N_zaziInters N_zr9
 | D_245 : disj N_zaziInters N_zanonce
 | D_246 : disj N_zaziInters N_zS0051
 | D_247 : disj N_zaziInters N_zS0052
 | D_248 : disj N_zaziInters N_zS0053
 | D_249 : disj N_zaziInters N_zS0054
 | D_250 : disj N_zaziInters N_zS0055
 | D_251 : disj N_zazzzzResult N_zazzzzResult
 | D_252 : disj N_zazzzzResult N_zr0
 | D_253 : disj N_zazzzzResult N_zr1
 | D_254 : disj N_zazzzzResult N_zr10
 | D_255 : disj N_zazzzzResult N_zr11
 | D_256 : disj N_zazzzzResult N_zr12
 | D_257 : disj N_zazzzzResult N_zr3
 | D_258 : disj N_zazzzzResult N_zr4
 | D_259 : disj N_zazzzzResult N_zr6
 | D_260 : disj N_zazzzzResult N_zr8
 | D_261 : disj N_zazzzzResult N_zr9
 | D_262 : disj N_zazzzzResult N_zanet1
 | D_263 : disj N_zazzzzResult N_zanet2
 | D_264 : disj N_zazzzzResult N_zanonce
 | D_265 : disj N_zazzzzResult N_zS0051
 | D_266 : disj N_zazzzzResult N_zS0052
 | D_267 : disj N_zazzzzResult N_zS0053
 | D_268 : disj N_zazzzzResult N_zS0054
 | D_269 : disj N_zazzzzResult N_zS0055
 | D_270 : disj N_zr0 N_zr1
 | D_271 : disj N_zr0 N_zr10
 | D_272 : disj N_zr0 N_zr11
 | D_273 : disj N_zr0 N_zr12
 | D_274 : disj N_zr0 N_zr3
 | D_275 : disj N_zr0 N_zr4
 | D_276 : disj N_zr0 N_zr6
 | D_277 : disj N_zr0 N_zr8
 | D_278 : disj N_zr0 N_zr9
 | D_279 : disj N_zr0 N_zanet1
 | D_280 : disj N_zr0 N_zanonce
 | D_281 : disj N_zr0 N_zS0051
 | D_282 : disj N_zr0 N_zS0052
 | D_283 : disj N_zr0 N_zS0053
 | D_284 : disj N_zr0 N_zS0054
 | D_285 : disj N_zr0 N_zS0055
 | D_286 : disj N_zr1 N_zr10
 | D_287 : disj N_zr1 N_zr11
 | D_288 : disj N_zr1 N_zr12
 | D_289 : disj N_zr1 N_zr3
 | D_290 : disj N_zr1 N_zr4
 | D_291 : disj N_zr1 N_zr6
 | D_292 : disj N_zr1 N_zr8
 | D_293 : disj N_zr1 N_zr9
 | D_294 : disj N_zr1 N_zanonce
 | D_295 : disj N_zr1 N_zS0051
 | D_296 : disj N_zr1 N_zS0052
 | D_297 : disj N_zr1 N_zS0053
 | D_298 : disj N_zr1 N_zS0054
 | D_299 : disj N_zr1 N_zS0055
 | D_300 : disj N_zr10 N_zr11
 | D_301 : disj N_zr10 N_zr12
 | D_302 : disj N_zr10 N_zr3
 | D_303 : disj N_zr10 N_zr6
 | D_304 : disj N_zr10 N_zr8
 | D_305 : disj N_zr10 N_zr9
 | D_306 : disj N_zr10 N_zanet1
 | D_307 : disj N_zr10 N_zanonce
 | D_308 : disj N_zr10 N_zS0051
 | D_309 : disj N_zr10 N_zS0052
 | D_310 : disj N_zr10 N_zS0053
 | D_311 : disj N_zr10 N_zS0054
 | D_312 : disj N_zr10 N_zS0055
 | D_313 : disj N_zr11 N_zr12
 | D_314 : disj N_zr11 N_zr3
 | D_315 : disj N_zr11 N_zr4
 | D_316 : disj N_zr11 N_zr6
 | D_317 : disj N_zr11 N_zr8
 | D_318 : disj N_zr11 N_zr9
 | D_319 : disj N_zr11 N_zanet1
 | D_320 : disj N_zr11 N_zanonce
 | D_321 : disj N_zr11 N_zS0051
 | D_322 : disj N_zr11 N_zS0052
 | D_323 : disj N_zr11 N_zS0053
 | D_324 : disj N_zr11 N_zS0054
 | D_325 : disj N_zr11 N_zS0055
 | D_326 : disj N_zr12 N_zr3
 | D_327 : disj N_zr12 N_zr4
 | D_328 : disj N_zr12 N_zr6
 | D_329 : disj N_zr12 N_zr8
 | D_330 : disj N_zr12 N_zr9
 | D_331 : disj N_zr12 N_zanet1
 | D_332 : disj N_zr12 N_zanet2
 | D_333 : disj N_zr12 N_zanonce
 | D_334 : disj N_zr12 N_zS0051
 | D_335 : disj N_zr12 N_zS0054
 | D_336 : disj N_zr12 N_zS0055
 | D_337 : disj N_zr3 N_zr4
 | D_338 : disj N_zr3 N_zr6
 | D_339 : disj N_zr3 N_zr8
 | D_340 : disj N_zr3 N_zr9
 | D_341 : disj N_zr3 N_zanet1
 | D_342 : disj N_zr3 N_zanonce
 | D_343 : disj N_zr3 N_zS0051
 | D_344 : disj N_zr3 N_zS0052
 | D_345 : disj N_zr3 N_zS0053
 | D_346 : disj N_zr3 N_zS0054
 | D_347 : disj N_zr3 N_zS0055
 | D_348 : disj N_zr4 N_zr6
 | D_349 : disj N_zr4 N_zr8
 | D_350 : disj N_zr4 N_zr9
 | D_351 : disj N_zr4 N_zanet1
 | D_352 : disj N_zr4 N_zanonce
 | D_353 : disj N_zr4 N_zS0051
 | D_354 : disj N_zr4 N_zS0052
 | D_355 : disj N_zr4 N_zS0053
 | D_356 : disj N_zr4 N_zS0054
 | D_357 : disj N_zr4 N_zS0055
 | D_358 : disj N_zr6 N_zr8
 | D_359 : disj N_zr6 N_zr9
 | D_360 : disj N_zr6 N_zanet1
 | D_361 : disj N_zr6 N_zanet2
 | D_362 : disj N_zr6 N_zanonce
 | D_363 : disj N_zr6 N_zS0051
 | D_364 : disj N_zr6 N_zS0052
 | D_365 : disj N_zr6 N_zS0053
 | D_366 : disj N_zr8 N_zr9
 | D_367 : disj N_zr8 N_zanet1
 | D_368 : disj N_zr8 N_zanet2
 | D_369 : disj N_zr8 N_zanonce
 | D_370 : disj N_zr8 N_zS0051
 | D_371 : disj N_zr8 N_zS0052
 | D_372 : disj N_zr8 N_zS0053
 | D_373 : disj N_zr8 N_zS0054
 | D_374 : disj N_zr8 N_zS0055
 | D_375 : disj N_zr9 N_zanet1
 | D_376 : disj N_zr9 N_zanet2
 | D_377 : disj N_zr9 N_zanonce
 | D_378 : disj N_zr9 N_zS0051
 | D_379 : disj N_zr9 N_zS0052
 | D_380 : disj N_zr9 N_zS0053
 | D_381 : disj N_zr9 N_zS0054
 | D_382 : disj N_zr9 N_zS0055
 | D_383 : disj N_zanet1 N_zS0051
 | D_384 : disj N_zanet1 N_zS0052
 | D_385 : disj N_zanet1 N_zS0053
 | D_386 : disj N_zanet1 N_zS0054
 | D_387 : disj N_zanet1 N_zS0055
 | D_388 : disj N_zanet2 N_zS0051
 | D_389 : disj N_zanet2 N_zS0052
 | D_390 : disj N_zanet2 N_zS0053
 | D_391 : disj N_zanet2 N_zS0054
 | D_392 : disj N_zanet2 N_zS0055
 | D_393 : disj N_zanonce N_zS0051
 | D_394 : disj N_zanonce N_zS0052
 | D_395 : disj N_zanonce N_zS0053
 | D_396 : disj N_zanonce N_zS0054
 | D_397 : disj N_zanonce N_zS0055
 | D_398 : disj N_zS0051 N_zS0052
 | D_399 : disj N_zS0051 N_zS0053
 | D_400 : disj N_zS0051 N_zS0054
 | D_401 : disj N_zS0051 N_zS0055
 | D_402 : disj N_zS0052 N_zS0054
 | D_403 : disj N_zS0052 N_zS0055
 | D_404 : disj N_zS0053 N_zS0054
 | D_405 : disj N_zS0053 N_zS0055
.
Ltac disj_table := first
 [ apply D_234
 | apply D_235
 | apply D_236
 | apply D_237
 | apply D_238
 | apply D_239
 | apply D_240
 | apply D_241
 | apply D_242
 | apply D_243
 | apply D_244
 | apply D_245
 | apply D_246
 | apply D_247
 | apply D_248
 | apply D_249
 | apply D_250
 | apply D_251
 | apply D_252
 | apply D_253
 | apply D_254
 | apply D_255
 | apply D_256
 | apply D_257
 | apply D_258
 | apply D_259
 | apply D_260
 | apply D_261
 | apply D_262
 | apply D_263
 | apply D_264
 | apply D_265
 | apply D_266
 | apply D_267
 | apply D_268
 | apply D_269
 | apply D_270
 | apply D_271
 | apply D_272
 | apply D_273
 | apply D_274
 | apply D_275
 | apply D_276
 | apply D_277
 | apply D_278
 | apply D_279
 | apply D_280
 | apply D_281
 | apply D_282
 | apply D_283
 | apply D_284
 | apply D_285
 | apply D_286
 | apply D_287
 | apply D_288
 | apply D_289
 | apply D_290
 | apply D_291
 | apply D_292
 | apply D_293
 | apply D_294
 | apply D_295
 | apply D_296
 | apply D_297
 | apply D_298
 | apply D_299
 | apply D_300
 | apply D_301
 | apply D_302
 | apply D_303
 | apply D_304
 | apply D_305
 | apply D_306
 | apply D_307
 | apply D_308
 | apply D_309
 | apply D_310
 | apply D_311
 | apply D_312
 | apply D_313
 | apply D_314
 | apply D_315
 | apply D_316
 | apply D_317
 | apply D_318
 | apply D_319
 | apply D_320
 | apply D_321
 | apply D_322
 | apply D_323
 | apply D_324
 | apply D_325
 | apply D_326
 | apply D_327
 | apply D_328
 | apply D_329
 | apply D_330
 | apply D_331
 | apply D_332
 | apply D_333
 | apply D_334
 | apply D_335
 | apply D_336
 | apply D_337
 | apply D_338
 | apply D_339
 | apply D_340
 | apply D_341
 | apply D_342
 | apply D_343
 | apply D_344
 | apply D_345
 | apply D_346
 | apply D_347
 | apply D_348
 | apply D_349
 | apply D_350
 | apply D_351
 | apply D_352
 | apply D_353
 | apply D_354
 | apply D_355
 | apply D_356
 | apply D_357
 | apply D_358
 | apply D_359
 | apply D_360
 | apply D_361
 | apply D_362
 | apply D_363
 | apply D_364
 | apply D_365
 | apply D_366
 | apply D_367
 | apply D_368
 | apply D_369
 | apply D_370
 | apply D_371
 | apply D_372
 | apply D_373
 | apply D_374
 | apply D_375
 | apply D_376
 | apply D_377
 | apply D_378
 | apply D_379
 | apply D_380
 | apply D_381
 | apply D_382
 | apply D_383
 | apply D_384
 | apply D_385
 | apply D_386
 | apply D_387
 | apply D_388
 | apply D_389
 | apply D_390
 | apply D_391
 | apply D_392
 | apply D_393
 | apply D_394
 | apply D_395
 | apply D_396
 | apply D_397
 | apply D_398
 | apply D_399
 | apply D_400
 | apply D_401
 | apply D_402
 | apply D_403
 | apply D_404
 | apply D_405
 ] .
Definition disjoint_on t :=
   forall s1 s2, disj s1 s2 -> s1 t -> s2 t -> False .
Ltac disj_app :=
   match goal with
   | h1 : ?s1 ?t , h2 : ?s2 ?t , h3 : disjoint_on ?t |- _ =>
        apply (h3 s1 s2) ;
         [ disj_table ; assumption
         | apply h1
         | apply h2
         ]
   end .
Lemma disjoint : forall t, disjoint_on t.
Proof.
intro t ; induction t ; intro s1 ; intro s2 ; intro H ; intros ;
  (* abstract here reduces proof size & check time *)
abstract (inversion H ; subst ;
abstract ((decomposition_once ; idtac "decomposed 1st") ;
abstract ((decomposition_once ; idtac "decomposed 2nd") ;
abstract disj_app ))) .
Save.
(* Change the goal to False *)
Ltac absurdum := cut False ; [ contradiction | idtac ] .
Ltac empty_intersection :=
   match goal with
   | h1 : ?s1 ?t , h2 : ?s2 ?t |- _ =>
        absurdum ; apply (disjoint t s1 s2) ;
          [ disj_table | try assumption | try assumption ]
   end .
(* After decomposition, for rewritings like f X => X, we might
   have to prove s1 t -> s2 t, which is not directly possible since
   we removed these transitions.  Here, we need just one more inversion *)
Ltac inversionVar :=
   match goal with
   | h : ?s ?t |- _ ?t => inversion h ; subst
   | _                 => idtac
   end .
Lemma Automaton_N_closed_under_R :
   forall s_n x y, State_N s_n -> s_n x -> R x y -> s_n y.
Proof.
intros ;
elim H ; intros ; inversion H2 ; subst ;
abstract ( inversion H1 ; subst ;
abstract ( decomposition ; inversionVar ;
abstract ( apply_transitionsN_rec || empty_intersection ))) .
Save.
Lemma Automaton_T_closed_under_R :
   forall s_t x y, State_T s_t -> s_t x -> R x y -> s_t y.
Proof.
intros ; elim H ; intro s_n ; intro ;
apply (Add_trans s_t s_n) ;
 [ assumption
 | apply (Automaton_N_closed_under_R s_n x y) ;
    [ exists s_t ; assumption
    | apply (Rm_trans s_t s_n) ; assumption
    | assumption
    ]
 ].
Save.
(****************************
  Rewriting Relation (closed under contexts and reflexivity).
 ****************************)
Inductive RC : term -> term -> Prop :=
 | RC_S : forall t, RC t t
 | RC_R : forall t u, R t u -> RC t u
 | RC_h_zi : forall t1 u1, RC t1 u1 ->  RC (h_zi t1) (h_zi u1)
 | RC_h_zt : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 ->  RC (h_zt t1 t2) (h_zt u1 u2)
 | RC_h_zc : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 ->  RC (h_zc t1 t2) (h_zc u1 u2)
 | RC_h_cons : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 ->  RC (h_cons t1 t2) (h_cons u1 u2)
 | RC_h_dec : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 ->  RC (h_dec t1 t2) (h_dec u1 u2)
 | RC_h_enc : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 ->  RC (h_enc t1 t2) (h_enc u1 u2)
 | RC_h_fst : forall t1 u1, RC t1 u1 ->  RC (h_fst t1) (h_fst u1)
 | RC_h_next : forall t1 u1, RC t1 u1 ->  RC (h_next t1) (h_next u1)
 | RC_h_snd : forall t1 u1, RC t1 u1 ->  RC (h_snd t1) (h_snd u1)
.
(****************************
  Rewriting Relation (closed under contexts and refl, trans).
 ****************************)
Inductive RCs : term -> term -> Prop :=
 | RCs_S : forall t, RCs t t
 | RCs_T  : forall t1 t2 t3, RCs t1 t2 -> RC t2 t3 -> RCs t1 t3
.
Scheme Min_RC := Minimality for RC Sort Prop .
Definition rew t u := forall s_n, State_N s_n -> s_n t -> s_n u .
(* When (RC t u), (rew t u) and (s t), add (s u) as Hp *)
Ltac RC_augment_once :=
   match goal with
   | h : rew ?t ?u , h2 : ?s ?t |- _ =>
         match goal with
         | h3 : s u |- _ => fail 1
         | _             => cut (s u) ; [ intro |
                            apply (h s) ; [ knownState | exact h2 ] ]
         end
   end .
Ltac RC_augment := repeat RC_augment_once .
Lemma Automaton_N_closed_ctx :
   forall t u, RC t u -> rew t u .
Proof.
intros t u H ; apply Min_RC ; solve 
 [ (* RC_S case *)
   intro ; intro ; intro ; assumption
   (* RC_R case : use closure lemma *)
 | intro t0 ; intros ; intro s_t ; intro ; intros ;
   apply (Automaton_N_closed_under_R s_t t0) ; assumption
   (* The actual contexts *)
 | intro ; intros ; intro s_t ;
   intro S  ; intros ; elim S ; intro s_n ; intro S1 ;
    inversion S1 ; subst ;
    decomposition ; RC_augment ; apply_transitionsN_once
    (* The Min base *)
 | assumption ] .
Save.
Lemma Automaton_N_closed_under_RC :
   forall s_n t u, State_N s_n -> s_n t -> RC t u -> s_n u.
Proof.
intro s_n ; intros ; cut (rew t u) ;
  [ intro Rew ; unfold rew in Rew ; apply (Rew s_n) ; assumption
  | apply Automaton_N_closed_ctx ; assumption
  ].
Save.
Lemma Automaton_N_closed_under_RCs :
   forall s_n t u, State_N s_n -> s_n t -> RCs t u -> s_n u.
Proof.
intros ; induction H1 ; [ assumption
  | apply (Automaton_N_closed_under_RC s_n t2 t3) ;
       [ assumption | auto | assumption ] ] .
Save.
Lemma Automaton_T_closed_under_RC :
   forall s_t t u, State_T s_t -> s_t t -> RC t u -> s_t u.
Proof.
intros s_t t u S ; elim S ; intro s_n ; intros ;
apply (Add_trans s_t s_n) ;
  [ assumption
  | apply (Automaton_N_closed_under_RC s_n t u) ;
     [ exists s_t ; assumption
     | apply (Rm_trans s_t s_n) ; assumption
     | assumption
     ]
  ].
Save.
Lemma Automaton_T_closed_under_RCs :
   forall s_t t u, State_T s_t -> s_t t -> RCs t u -> s_t u.
Proof.
intros ; induction H1 ; [ assumption
  | apply (Automaton_T_closed_under_RC s_t t2 t3) ;
       [ assumption | auto | assumption ] ] .
Save.
(* Intersection Constraints *)
Inductive intCon_N : St -> St -> St -> Prop :=
.
Lemma Automaton_N_satisfies_intersection_constraints :
   forall s1 s2 s3 t, intCon_N s1 s2 s3 -> s2 t -> s3 t -> s1 t .
Proof.
intros s1 s2 s3 t I S2 S3 ; inversion I ; subst ;
inversion S2 ; subst ; decomposition ;
(apply_transitionsN_once || empty_intersection).
Save.
(* TODO : Perhaps defining intCon_N from intCon_T would be better
   for the user, so that _N stuff can be entirely neglected. *)
Inductive intCon_T : St -> St -> St -> Prop :=
 | IntCon_T : forall s1_t s1_n s2_t s2_n s3_t s3_n,
     State s1_t s1_n -> State s2_t s2_n -> State s3_t s3_n ->
     intCon_N s1_n s2_n s3_n -> intCon_T s1_t s2_t s3_t
.
Lemma Automaton_T_satisfies_intersection_constraints :
   forall s1 s2 s3 t, State_T s1 ->
      intCon_T s1 s2 s3 -> s2 t -> s3 t -> s1 t .
Proof.
intros ; inversion H0 ; subst ;
apply (Add_trans s1 s1_n t) ; [ try assumption | idtac ] ;
apply (Automaton_N_satisfies_intersection_constraints s1_n s2_n s3_n) ;
   [ assumption
   | apply (Rm_trans s2 s2_n) ; assumption
   | apply (Rm_trans s3 s3_n) ; assumption
   ] .
Save.
(****************************
  The User Input Automaton
 ****************************)
Inductive O_zr0 : St :=
   | T_O_406 : forall x1 x2, O_zr1 x1 -> O_zr2 x2 -> O_zr0 (h_zc x1 x2)
   | T_O_407 : forall t1 t2 , O_zr0 t1 -> RCs t1 t2 -> O_zr0 t2
with O_zr1 : St :=
   | T_O_408 : O_zr1 h_g
   | T_O_409 : forall t1 t2 , O_zr1 t1 -> RCs t1 t2 -> O_zr1 t2
with O_zr10 : St :=
   | T_O_410 : forall x1 x2, O_zanet1 x1 -> O_zr11 x2 -> O_zr10 (h_dec x1 x2)
   | T_O_411 : forall t1 t2 , O_zr10 t1 -> RCs t1 t2 -> O_zr10 t2
with O_zr11 : St :=
   | T_O_412 : O_zr11 h_k2
   | T_O_413 : forall t1 t2 , O_zr11 t1 -> RCs t1 t2 -> O_zr11 t2
with O_zr12 : St :=
   | T_O_414 : O_zr12 h_a
   | T_O_415 : forall t1 t2 , O_zr12 t1 -> RCs t1 t2 -> O_zr12 t2
with O_zr2 : St :=
   | T_O_416 : O_zr2 h_a
   | T_O_417 : forall t1 t2 , O_zr2 t1 -> RCs t1 t2 -> O_zr2 t2
with O_zr3 : St :=
   | T_O_418 : O_zr3 h_k1
   | T_O_419 : forall t1 t2 , O_zr3 t1 -> RCs t1 t2 -> O_zr3 t2
with O_zr4 : St :=
   | T_O_420 : forall x1 x2, O_zr5 x1 -> O_zr6 x2 -> O_zr4 (h_zc x1 x2)
   | T_O_421 : forall t1 t2 , O_zr4 t1 -> RCs t1 t2 -> O_zr4 t2
with O_zr5 : St :=
   | T_O_422 : O_zr5 h_g
   | T_O_423 : forall t1 t2 , O_zr5 t1 -> RCs t1 t2 -> O_zr5 t2
with O_zr6 : St :=
   | T_O_424 : O_zr6 h_b
   | T_O_425 : forall t1 t2 , O_zr6 t1 -> RCs t1 t2 -> O_zr6 t2
with O_zr7 : St :=
   | T_O_426 : O_zr7 h_k2
   | T_O_427 : forall t1 t2 , O_zr7 t1 -> RCs t1 t2 -> O_zr7 t2
with O_zr8 : St :=
   | T_O_428 : O_zr8 h_m
   | T_O_429 : forall t1 t2 , O_zr8 t1 -> RCs t1 t2 -> O_zr8 t2
with O_zr9 : St :=
   | T_O_430 : forall x1 x2, O_zr10 x1 -> O_zr12 x2 -> O_zr9 (h_zc x1 x2)
   | T_O_431 : forall t1 t2 , O_zr9 t1 -> RCs t1 t2 -> O_zr9 t2
with O_zanet1 : St :=
   | T_O_432 : O_zanet1 h_1
   | T_O_433 : O_zanet1 h_g
   | T_O_434 : forall x1, O_zanonce x1 -> O_zanet1 x1
   | T_O_435 : forall x1 x2, O_zr0 x1 -> O_zr3 x2 -> O_zanet1 (h_enc x1 x2)
   | T_O_436 : forall x1 x2, O_zr4 x1 -> O_zr7 x2 -> O_zanet1 (h_enc x1 x2)
   | T_O_437 : forall x1 x2, O_zr8 x1 -> O_zr9 x2 -> O_zanet1 (h_enc x1 x2)
   | T_O_438 : forall x1 x2, O_zanet1 x1 -> O_zanet1 x2 -> O_zanet1 (h_zt x1 x2)
   | T_O_439 : forall x1 x2, O_zanet1 x1 -> O_zanet1 x2 -> O_zanet1 (h_zc x1 x2)
   | T_O_440 : forall x1, O_zanet1 x1 -> O_zanet1 (h_zi x1)
   | T_O_441 : forall x1 x2, O_zanet1 x1 -> O_zanet1 x2 -> O_zanet1 (h_enc x1 x2)
   | T_O_442 : forall x1 x2, O_zanet1 x1 -> O_zanet1 x2 -> O_zanet1 (h_dec x1 x2)
   | T_O_443 : forall x1 x2, O_zanet1 x1 -> O_zanet1 x2 -> O_zanet1 (h_cons x1 x2)
   | T_O_444 : forall x1, O_zanet1 x1 -> O_zanet1 (h_fst x1)
   | T_O_445 : forall x1, O_zanet1 x1 -> O_zanet1 (h_snd x1)
   | T_O_446 : forall t1 t2 , O_zanet1 t1 -> RCs t1 t2 -> O_zanet1 t2
with O_zanet2 : St :=
   | T_O_447 : forall x1, O_zanet1 x1 -> O_zanet2 x1
   | T_O_448 : O_zanet2 h_k1
   | T_O_449 : O_zanet2 h_k2
   | T_O_450 : forall x1 x2, O_zanet2 x1 -> O_zanet2 x2 -> O_zanet2 (h_zt x1 x2)
   | T_O_451 : forall x1 x2, O_zanet2 x1 -> O_zanet2 x2 -> O_zanet2 (h_zc x1 x2)
   | T_O_452 : forall x1, O_zanet2 x1 -> O_zanet2 (h_zi x1)
   | T_O_453 : forall x1 x2, O_zanet2 x1 -> O_zanet2 x2 -> O_zanet2 (h_enc x1 x2)
   | T_O_454 : forall x1 x2, O_zanet2 x1 -> O_zanet2 x2 -> O_zanet2 (h_dec x1 x2)
   | T_O_455 : forall x1 x2, O_zanet2 x1 -> O_zanet2 x2 -> O_zanet2 (h_cons x1 x2)
   | T_O_456 : forall x1, O_zanet2 x1 -> O_zanet2 (h_fst x1)
   | T_O_457 : forall x1, O_zanet2 x1 -> O_zanet2 (h_snd x1)
   | T_O_458 : forall t1 t2 , O_zanet2 t1 -> RCs t1 t2 -> O_zanet2 t2
with O_zanonce : St :=
   | T_O_459 : O_zanonce h_seed
   | T_O_460 : forall x1, O_zanonce x1 -> O_zanonce (h_next x1)
   | T_O_461 : forall t1 t2 , O_zanonce t1 -> RCs t1 t2 -> O_zanonce t2
with O_zazzzzResult : St :=
   | T_O_462 : forall t1 t2 , O_zazzzzResult t1 -> RCs t1 t2 -> O_zazzzzResult t2
.
Scheme
 Min_O_zr0 := Minimality for O_zr0 Sort Prop with
 Min_O_zr1 := Minimality for O_zr1 Sort Prop with
 Min_O_zr10 := Minimality for O_zr10 Sort Prop with
 Min_O_zr11 := Minimality for O_zr11 Sort Prop with
 Min_O_zr12 := Minimality for O_zr12 Sort Prop with
 Min_O_zr2 := Minimality for O_zr2 Sort Prop with
 Min_O_zr3 := Minimality for O_zr3 Sort Prop with
 Min_O_zr4 := Minimality for O_zr4 Sort Prop with
 Min_O_zr5 := Minimality for O_zr5 Sort Prop with
 Min_O_zr6 := Minimality for O_zr6 Sort Prop with
 Min_O_zr7 := Minimality for O_zr7 Sort Prop with
 Min_O_zr8 := Minimality for O_zr8 Sort Prop with
 Min_O_zr9 := Minimality for O_zr9 Sort Prop with
 Min_O_zanet1 := Minimality for O_zanet1 Sort Prop with
 Min_O_zanet2 := Minimality for O_zanet2 Sort Prop with
 Min_O_zanonce := Minimality for O_zanonce Sort Prop with
 Min_O_zazzzzResult := Minimality for O_zazzzzResult Sort Prop .
Definition Min_sat_O_zr0 := Min_O_zr0 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr1 := Min_O_zr1 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr10 := Min_O_zr10 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr11 := Min_O_zr11 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr12 := Min_O_zr12 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr2 := Min_O_zr2 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr3 := Min_O_zr3 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr4 := Min_O_zr4 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr5 := Min_O_zr5 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr6 := Min_O_zr6 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr7 := Min_O_zr7 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr8 := Min_O_zr8 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zr9 := Min_O_zr9 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zanet1 := Min_O_zanet1 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zanet2 := Min_O_zanet2 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zanonce := Min_O_zanonce N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
Definition Min_sat_O_zazzzzResult := Min_O_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr12 N_zr3 N_zr4 N_zr1 N_zr6 N_zr11 N_zr8 N_zr9 N_zanet1 N_zanet2 N_zanonce N_zazzzzResult .
(****************************
  The correspondent states of O and N.
  May not be the same state because of the Joins.
 ****************************)
Inductive incl_N : St -> St -> Prop :=
 | Incl_O_zr0 : incl_N O_zr0 N_zr0
 | Incl_O_zr1 : incl_N O_zr1 N_zr1
 | Incl_O_zr10 : incl_N O_zr10 N_zr10
 | Incl_O_zr11 : incl_N O_zr11 N_zr11
 | Incl_O_zr12 : incl_N O_zr12 N_zr12
 | Incl_O_zr2 : incl_N O_zr2 N_zr12
 | Incl_O_zr3 : incl_N O_zr3 N_zr3
 | Incl_O_zr4 : incl_N O_zr4 N_zr4
 | Incl_O_zr5 : incl_N O_zr5 N_zr1
 | Incl_O_zr6 : incl_N O_zr6 N_zr6
 | Incl_O_zr7 : incl_N O_zr7 N_zr11
 | Incl_O_zr8 : incl_N O_zr8 N_zr8
 | Incl_O_zr9 : incl_N O_zr9 N_zr9
 | Incl_O_zanet1 : incl_N O_zanet1 N_zanet1
 | Incl_O_zanet2 : incl_N O_zanet2 N_zanet2
 | Incl_O_zanonce : incl_N O_zanonce N_zanonce
 | Incl_O_zazzzzResult : incl_N O_zazzzzResult N_zazzzzResult
.
(* The transposition of the above to O and T *)
Inductive incl_T : St -> St -> Prop :=
 | Incl_T : forall s_o s_t s_n,
      State s_t s_n ->
      incl_N s_o s_n -> incl_T s_o s_t .
Ltac empty_zaziInters :=
   match goal with
   | h : N_zaziInters _ |- _ => inversion h ; fail
   end .
Ltac handle_intcon :=
   match goal with
   | h2 : ?s2 ?t , h3 : ?s3 ?t |- ?s1 ?t =>
      apply (Automaton_N_satisfies_intersection_constraints s1 s2 s3) ;
         [ solve [  idtac  ]
         | exact h2
         | exact h3
         ]
   end .
Ltac handle_rewrite :=
   match goal with
   | h1 : ?s ?t1 , h2 : RCs ?t1 ?t2 |- ?s ?t2 =>
      apply (Automaton_N_closed_under_RCs s t1 t2) ;
      [ knownState | exact h1 | exact h2 ] ; fail
   end .
Lemma Automaton_N_is_a_safe_overapproximation_of_automaton_O :
  forall s_o s_n t, incl_N s_o s_n -> s_o t -> s_n t .
Proof.
intros s_o s_n t H H0 ; inversion H ; subst ;
  [ apply Min_sat_O_zr0
  | apply Min_sat_O_zr1
  | apply Min_sat_O_zr10
  | apply Min_sat_O_zr11
  | apply Min_sat_O_zr12
  | apply Min_sat_O_zr2
  | apply Min_sat_O_zr3
  | apply Min_sat_O_zr4
  | apply Min_sat_O_zr5
  | apply Min_sat_O_zr6
  | apply Min_sat_O_zr7
  | apply Min_sat_O_zr8
  | apply Min_sat_O_zr9
  | apply Min_sat_O_zanet1
  | apply Min_sat_O_zanet2
  | apply Min_sat_O_zanonce
  | apply Min_sat_O_zazzzzResult
  ] ; intros ; 
solve [ (* the non-intersection-constraint case first *)
        try empty_zaziInters ;
        try apply_transitionsN_rec ;
        (* here we rely on inversionVar to pick the freshest H,
        i.e. the N one (not the O one) *)
        inversionVar ; try apply_transitionsN_once
      | (* intersection constraints *)
        handle_intcon
      | (* RCs closure *)
        handle_rewrite
      ] .
Save.
Lemma Automaton_T_is_a_safe_overapproximation_of_automaton_O :
  forall s_o s_t t, incl_T s_o s_t -> s_o t -> s_t t .
Proof.
intros s_o s_t t H H0 ; inversion H ; subst ;
apply (Add_trans s_t s_n) ; [ assumption |
  apply (Automaton_N_is_a_safe_overapproximation_of_automaton_O s_o) ;
    assumption ].
Save.
(* User Full Rule Facts (usually, the goal of the analysis) *)
Ltac Rm_trans_in h :=
   match type of h with
   | State ?s_t ?s_n =>
      match goal with
      | h1 : s_t ?t |- _ => cut (s_n t) ; 
         [ idtac | apply (Rm_trans s_t s_n) ; assumption ]
      end
   end .
Ltac full_rule_T s1_t s1_n s2_t s2_n s1_fact s2_fact FR_N :=
   (* Show State facts *)
   (cut (State s1_t s1_n) ; [ idtac | apply s1_fact ]);intro s1_f ;
   (cut (State s2_t s2_n) ; [ idtac | apply s2_fact ]);intro s2_f ;
   (* Show (s1_n t1) *)
   Rm_trans_in s1_f ; intro ;
   (* Reduce to (s2_n t2) *)
   apply (Add_trans s2_t s2_n) ; [ assumption | idtac ] ;
   (* Apply previous lemma *)
   apply FR_N ; assumption
.
Ltac does_not_belong_to_N FR :=
   (* intro negation *)
   intro ;
   (* Show (@zzResult !FAIL!) using FR *)
   cut (N_zazzzzResult h_ziFAILzi) ;
      [ idtac | apply FR ; assumption ] ;
   (* Derive a contradiction *)
   intro Fail_N ; inversion Fail_N
.
Ltac does_not_belong_to_T s_t s_n s_fact DNB_N :=
   (* intro negation *)
   intro H ;
   (* Show State fact *)
   cut (State s_t s_n) ; [ idtac | apply s_fact ] ; intro s_f ;
   (* Show (s_n t) *)
   Rm_trans_in s_f ; intro ;
   (* Apply previous lemma *)
   apply DNB_N ; assumption
.
Ltac elim_all_exists_once :=
   match goal with
   (* exists is Notation for (ex (fun x => _)) *)
   | h : ex _ |- _ => elim h ; clear h ; intro ; intro
   end .
Ltac elim_all_exists := repeat elim_all_exists_once .
Ltac add_useless_hypothesis name := cut True ; [ intro name | trivial ] .
Ltac unreachability s_o s_n t incl_s_o h :=
   cut (s_n t) ;
     [ clear h ; intro ; decomposition
     | apply (Automaton_N_is_a_safe_overapproximation_of_automaton_O s_o) ; 
         [ apply incl_s_o | assumption ]
     ] .
Ltac cut_on_RCs_snd s :=
   match goal with
   | h : RCs _ ?t |- _ => cut (s t)
   end .
Lemma FullRule_N_1 :
    N_zanet2 h_m -> N_zazzzzResult h_ziFAILzi .
Proof.
intros ; (apply_transitionsN_once || decomposition) .
Save.
Lemma FullRule_T_1 :
    T_zanet2 h_m -> T_zazzzzResult h_ziFAILzi .
Proof.
intros ;
full_rule_T T_zanet2 N_zanet2 T_zazzzzResult N_zazzzzResult ST_zanet2 ST_zazzzzResult (FullRule_N_1 ) .
Save.
Lemma Does_not_belong_to_N_1 :
     ~ N_zanet2 h_m .
Proof.
intros ;
does_not_belong_to_N (FullRule_N_1 ) .
Save.
Lemma Does_not_belong_to_T_1 :
     ~ T_zanet2 h_m .
Proof.
intros ;
does_not_belong_to_T T_zanet2 N_zanet2 ST_zanet2 (Does_not_belong_to_N_1 ) .
Save.
Lemma Unreachability_Alt_1 :
    ~( exists t, O_zanet2 t /\ RCs t h_m ) .
Proof.
intro H ; elim H ; clear H ; intro t ;
intro H ; elim_all_exists ;
(* elim and *)
elim H ; clear H ; intros ;
cut (T_zanet2 t) ;
  [ intros ; cut_on_RCs_snd T_zanet2 ;
    [ apply Does_not_belong_to_T_1 ; try assumption
    | apply (Automaton_T_closed_under_RCs T_zanet2 t) ;
      [ knownState | assumption | assumption ]
    ]
  | apply (Automaton_T_is_a_safe_overapproximation_of_automaton_O O_zanet2) ; 
      [ apply (Incl_T O_zanet2 T_zanet2 N_zanet2) ; [ apply ST_zanet2 | apply Incl_O_zanet2 ]
      | assumption
      ]
  ] .
Save.
Lemma Unreachability_1 :
    ~ O_zanet2 h_m .
Proof.
(* Hack: use names x, x0 so that new names start at x1 *)
add_useless_hypothesis x ; add_useless_hypothesis x0 ;
intro H ; elim_all_exists ;
unreachability O_zanet2 N_zanet2 h_m Incl_O_zanet2 H .
Save.