(**************************** 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_ziFAILzi : term | h_zp : term -> term -> term | h_0 : term | h_acc : term | h_cons : term -> term -> term | h_data : term | h_dec : term -> term -> term | h_enc : term -> term -> term | h_exp : term | h_exp1 : term | h_f1 : term -> term -> term -> term | h_f2 : term -> term -> term -> term | h_f3 : term -> term -> term -> term | h_f4 : term -> term -> term -> term | h_f5 : term -> term -> term | h_f6 : term -> term -> term | h_forbidden : term | h_fst : term -> term | h_h : term -> term -> term | h_imp : term | h_k3 : term | h_kek : term | h_kek2 : term | h_km : term | h_kp : term | h_p : term | h_pin : term | h_snd : term -> term . (* The type of the languages of the automaton states, i.e. a set of terms. *) Definition St := term -> Prop . (**************************** Completed Automaton, with direct transitions removed ****************************) Inductive N_zaziInters : St := with N_zazzzzResult : St := with N_zr0 : St := | T_N_0 : N_zr0 h_acc with N_zr1 : St := | T_N_1 : N_zr1 h_forbidden | T_N_2 : N_zr1 h_p with N_zr10 : St := | T_N_3 : forall x1 x2, N_zr11 x1 -> N_zr12 x2 -> N_zr10 (h_h x1 x2) with N_zr11 : St := | T_N_4 : N_zr11 h_imp with N_zr12 : St := | T_N_5 : N_zr12 h_kp with N_zr13 : St := | T_N_6 : N_zr13 h_forbidden | T_N_7 : N_zr13 h_km with N_zr14 : St := | T_N_8 : N_zr14 h_kek2 with N_zr15 : St := | T_N_9 : forall x1 x2, N_zr10 x1 -> N_zr13 x2 -> N_zr15 (h_h x1 x2) with N_zr21 : St := | T_N_10 : forall x1 x2, N_zr22 x1 -> N_zr13 x2 -> N_zr21 (h_h x1 x2) with N_zr22 : St := | T_N_11 : forall x1 x2, N_zr23 x1 -> N_zr12 x2 -> N_zr22 (h_h x1 x2) with N_zr23 : St := | T_N_12 : N_zr23 h_exp with N_zr26 : St := | T_N_13 : N_zr26 h_exp1 with N_zr27 : St := | T_N_14 : forall x1 x2, N_zr23 x1 -> N_zr13 x2 -> N_zr27 (h_h x1 x2) with N_zr3 : St := | T_N_15 : forall x1 x2, N_zr4 x1 -> N_zr5 x2 -> N_zr3 (h_h x1 x2) with N_zr4 : St := | T_N_16 : N_zr4 h_pin with N_zr5 : St := | T_N_17 : N_zr5 h_forbidden | T_N_18 : N_zr5 h_kek with N_zr6 : St := | T_N_19 : forall x1 x2, N_zr5 x1 -> N_zr8 x2 -> N_zr6 (h_zp x1 x2) | T_N_20 : forall x1 x2, N_zr8 x1 -> N_zr5 x2 -> N_zr6 (h_zp x1 x2) with N_zr8 : St := | T_N_21 : N_zr8 h_k3 with N_zaforbidden : St := | T_N_22 : forall x1 x2, N_zr0 x1 -> N_zr1 x2 -> N_zaforbidden (h_enc x1 x2) | T_N_23 : N_zaforbidden h_forbidden | T_N_24 : N_zaforbidden h_kek | T_N_25 : N_zaforbidden h_km | T_N_26 : N_zaforbidden h_p with N_zak : St := (* | T_N_27 : forall x1, N_zak x1 -> N_zak x1 *) (* | T_N_28 : forall x1, N_zapublic x1 -> N_zak x1 *) | T_N_29 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_zp x1 x2) | T_N_30 : N_zak h_0 | T_N_31 : N_zak h_acc | T_N_32 : N_zak h_data | T_N_33 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_dec x1 x2) | T_N_34 : forall x1 x2, N_zr1 x1 -> N_zr3 x2 -> N_zak (h_enc x1 x2) | T_N_35 : forall x1 x2, N_zr1 x1 -> N_zS0099 x2 -> N_zak (h_enc x1 x2) | T_N_36 : forall x1 x2, N_zr1 x1 -> N_zS0100 x2 -> N_zak (h_enc x1 x2) | T_N_37 : forall x1 x2, N_zr14 x1 -> N_zr15 x2 -> N_zak (h_enc x1 x2) | T_N_38 : forall x1 x2, N_zr14 x1 -> N_zr21 x2 -> N_zak (h_enc x1 x2) | T_N_39 : forall x1 x2, N_zr14 x1 -> N_zS0101 x2 -> N_zak (h_enc x1 x2) | T_N_40 : forall x1 x2, N_zr26 x1 -> N_zr27 x2 -> N_zak (h_enc x1 x2) | T_N_41 : forall x1 x2, N_zr6 x1 -> N_zr15 x2 -> N_zak (h_enc x1 x2) | T_N_42 : forall x1 x2, N_zr6 x1 -> N_zS0101 x2 -> N_zak (h_enc x1 x2) | T_N_43 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_enc x1 x2) | T_N_44 : forall x1 x2, N_zS0086 x1 -> N_zS0088 x2 -> N_zak (h_enc x1 x2) | T_N_45 : forall x1 x2, N_zS0086 x1 -> N_zS0098 x2 -> N_zak (h_enc x1 x2) | T_N_46 : forall x1 x2, N_zS0086 x1 -> N_zS0102 x2 -> N_zak (h_enc x1 x2) | T_N_47 : forall x1 x2, N_zS0086 x1 -> N_zS0103 x2 -> N_zak (h_enc x1 x2) | T_N_48 : forall x1 x2, N_zS0089 x1 -> N_zS0088 x2 -> N_zak (h_enc x1 x2) | T_N_49 : forall x1 x2, N_zS0089 x1 -> N_zS0098 x2 -> N_zak (h_enc x1 x2) | T_N_50 : forall x1 x2, N_zS0089 x1 -> N_zS0102 x2 -> N_zak (h_enc x1 x2) | T_N_51 : forall x1 x2, N_zS0089 x1 -> N_zS0103 x2 -> N_zak (h_enc x1 x2) | T_N_52 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zak (h_f1 x1 x2 x3) | T_N_53 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zak (h_f2 x1 x2 x3) | T_N_54 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zak (h_f3 x1 x2 x3) | T_N_55 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zak (h_f4 x1 x2 x3) | T_N_56 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_f5 x1 x2) | T_N_57 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_f6 x1 x2) | T_N_58 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zak (h_h x1 x2) | T_N_59 : N_zak h_imp | T_N_60 : N_zak h_k3 | T_N_61 : N_zak h_kp | T_N_62 : N_zak h_pin with N_zapublic : St := | T_N_63 : N_zapublic h_acc | T_N_64 : N_zapublic h_data | T_N_65 : N_zapublic h_imp | T_N_66 : N_zapublic h_k3 | T_N_67 : N_zapublic h_kp | T_N_68 : N_zapublic h_pin with N_zasecret : St := | T_N_69 : N_zasecret h_exp1 | T_N_70 : N_zasecret h_forbidden | T_N_71 : N_zasecret h_kek | T_N_72 : N_zasecret h_kek2 | T_N_73 : N_zasecret h_km | T_N_74 : N_zasecret h_p with N_zS0086 : St := (* | T_N_75 : forall x1, N_zr14 x1 -> N_zS0086 x1 *) (* | T_N_76 : forall x1, N_zS0086 x1 -> N_zS0086 x1 *) | T_N_77 : forall x1 x2, N_zr14 x1 -> N_zak x2 -> N_zS0086 (h_zp x1 x2) | T_N_78 : forall x1 x2, N_zak x1 -> N_zr14 x2 -> N_zS0086 (h_zp x1 x2) | T_N_79 : forall x1 x2, N_zak x1 -> N_zS0086 x2 -> N_zS0086 (h_zp x1 x2) | T_N_80 : forall x1 x2, N_zS0086 x1 -> N_zak x2 -> N_zS0086 (h_zp x1 x2) | T_N_81 : N_zS0086 h_kek2 with N_zS0087 : St := | T_N_82 : forall x1 x2, N_zr11 x1 -> N_zak x2 -> N_zS0087 (h_h x1 x2) with N_zS0088 : St := | T_N_83 : forall x1 x2, N_zS0087 x1 -> N_zr13 x2 -> N_zS0088 (h_h x1 x2) with N_zS0089 : St := (* | T_N_84 : forall x1, N_zr5 x1 -> N_zS0089 x1 *) (* | T_N_85 : forall x1, N_zr6 x1 -> N_zS0089 x1 *) (* | T_N_86 : forall x1, N_zS0089 x1 -> N_zS0089 x1 *) (* | T_N_87 : forall x1, N_zS0091 x1 -> N_zS0089 x1 *) | T_N_88 : forall x1 x2, N_zr5 x1 -> N_zr8 x2 -> N_zS0089 (h_zp x1 x2) | T_N_89 : forall x1 x2, N_zr5 x1 -> N_zak x2 -> N_zS0089 (h_zp x1 x2) | T_N_90 : forall x1 x2, N_zr5 x1 -> N_zS0090 x2 -> N_zS0089 (h_zp x1 x2) | T_N_91 : forall x1 x2, N_zr5 x1 -> N_zS0092 x2 -> N_zS0089 (h_zp x1 x2) | T_N_92 : forall x1 x2, N_zr6 x1 -> N_zr8 x2 -> N_zS0089 (h_zp x1 x2) | T_N_93 : forall x1 x2, N_zr6 x1 -> N_zak x2 -> N_zS0089 (h_zp x1 x2) | T_N_94 : forall x1 x2, N_zr6 x1 -> N_zS0090 x2 -> N_zS0089 (h_zp x1 x2) | T_N_95 : forall x1 x2, N_zr6 x1 -> N_zS0092 x2 -> N_zS0089 (h_zp x1 x2) | T_N_96 : forall x1 x2, N_zr8 x1 -> N_zr5 x2 -> N_zS0089 (h_zp x1 x2) | T_N_97 : forall x1 x2, N_zr8 x1 -> N_zr6 x2 -> N_zS0089 (h_zp x1 x2) | T_N_98 : forall x1 x2, N_zr8 x1 -> N_zS0089 x2 -> N_zS0089 (h_zp x1 x2) | T_N_99 : forall x1 x2, N_zr8 x1 -> N_zS0091 x2 -> N_zS0089 (h_zp x1 x2) | T_N_100 : forall x1 x2, N_zak x1 -> N_zr5 x2 -> N_zS0089 (h_zp x1 x2) | T_N_101 : forall x1 x2, N_zak x1 -> N_zr6 x2 -> N_zS0089 (h_zp x1 x2) | T_N_102 : forall x1 x2, N_zak x1 -> N_zS0089 x2 -> N_zS0089 (h_zp x1 x2) | T_N_103 : forall x1 x2, N_zak x1 -> N_zS0091 x2 -> N_zS0089 (h_zp x1 x2) | T_N_104 : forall x1 x2, N_zS0089 x1 -> N_zr8 x2 -> N_zS0089 (h_zp x1 x2) | T_N_105 : forall x1 x2, N_zS0089 x1 -> N_zak x2 -> N_zS0089 (h_zp x1 x2) | T_N_106 : forall x1 x2, N_zS0089 x1 -> N_zS0090 x2 -> N_zS0089 (h_zp x1 x2) | T_N_107 : forall x1 x2, N_zS0089 x1 -> N_zS0092 x2 -> N_zS0089 (h_zp x1 x2) | T_N_108 : forall x1 x2, N_zS0090 x1 -> N_zr5 x2 -> N_zS0089 (h_zp x1 x2) | T_N_109 : forall x1 x2, N_zS0090 x1 -> N_zr6 x2 -> N_zS0089 (h_zp x1 x2) | T_N_110 : forall x1 x2, N_zS0090 x1 -> N_zS0089 x2 -> N_zS0089 (h_zp x1 x2) | T_N_111 : forall x1 x2, N_zS0090 x1 -> N_zS0091 x2 -> N_zS0089 (h_zp x1 x2) | T_N_112 : forall x1 x2, N_zS0091 x1 -> N_zr8 x2 -> N_zS0089 (h_zp x1 x2) | T_N_113 : forall x1 x2, N_zS0091 x1 -> N_zak x2 -> N_zS0089 (h_zp x1 x2) | T_N_114 : forall x1 x2, N_zS0091 x1 -> N_zS0090 x2 -> N_zS0089 (h_zp x1 x2) | T_N_115 : forall x1 x2, N_zS0091 x1 -> N_zS0092 x2 -> N_zS0089 (h_zp x1 x2) | T_N_116 : forall x1 x2, N_zS0092 x1 -> N_zr5 x2 -> N_zS0089 (h_zp x1 x2) | T_N_117 : forall x1 x2, N_zS0092 x1 -> N_zr6 x2 -> N_zS0089 (h_zp x1 x2) | T_N_118 : forall x1 x2, N_zS0092 x1 -> N_zS0089 x2 -> N_zS0089 (h_zp x1 x2) | T_N_119 : forall x1 x2, N_zS0092 x1 -> N_zS0091 x2 -> N_zS0089 (h_zp x1 x2) | T_N_120 : N_zS0089 h_forbidden | T_N_121 : N_zS0089 h_kek with N_zS0090 : St := (* | T_N_122 : forall x1, N_zr8 x1 -> N_zS0090 x1 *) (* | T_N_123 : forall x1, N_zak x1 -> N_zS0090 x1 *) (* | T_N_124 : forall x1, N_zapublic x1 -> N_zS0090 x1 *) (* | T_N_125 : forall x1, N_zS0090 x1 -> N_zS0090 x1 *) (* | T_N_126 : forall x1, N_zS0092 x1 -> N_zS0090 x1 *) | T_N_127 : forall x1 x2, N_zr8 x1 -> N_zr8 x2 -> N_zS0090 (h_zp x1 x2) | T_N_128 : forall x1 x2, N_zr8 x1 -> N_zak x2 -> N_zS0090 (h_zp x1 x2) | T_N_129 : forall x1 x2, N_zr8 x1 -> N_zS0090 x2 -> N_zS0090 (h_zp x1 x2) | T_N_130 : forall x1 x2, N_zr8 x1 -> N_zS0092 x2 -> N_zS0090 (h_zp x1 x2) | T_N_131 : forall x1 x2, N_zak x1 -> N_zr8 x2 -> N_zS0090 (h_zp x1 x2) | T_N_132 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_zp x1 x2) | T_N_133 : forall x1 x2, N_zak x1 -> N_zS0090 x2 -> N_zS0090 (h_zp x1 x2) | T_N_134 : forall x1 x2, N_zak x1 -> N_zS0092 x2 -> N_zS0090 (h_zp x1 x2) | T_N_135 : forall x1 x2, N_zS0090 x1 -> N_zr8 x2 -> N_zS0090 (h_zp x1 x2) | T_N_136 : forall x1 x2, N_zS0090 x1 -> N_zak x2 -> N_zS0090 (h_zp x1 x2) | T_N_137 : forall x1 x2, N_zS0090 x1 -> N_zS0090 x2 -> N_zS0090 (h_zp x1 x2) | T_N_138 : forall x1 x2, N_zS0090 x1 -> N_zS0092 x2 -> N_zS0090 (h_zp x1 x2) | T_N_139 : forall x1 x2, N_zS0092 x1 -> N_zr8 x2 -> N_zS0090 (h_zp x1 x2) | T_N_140 : forall x1 x2, N_zS0092 x1 -> N_zak x2 -> N_zS0090 (h_zp x1 x2) | T_N_141 : forall x1 x2, N_zS0092 x1 -> N_zS0090 x2 -> N_zS0090 (h_zp x1 x2) | T_N_142 : forall x1 x2, N_zS0092 x1 -> N_zS0092 x2 -> N_zS0090 (h_zp x1 x2) | T_N_143 : N_zS0090 h_0 | T_N_144 : N_zS0090 h_acc | T_N_145 : N_zS0090 h_data | T_N_146 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_dec x1 x2) | T_N_147 : forall x1 x2, N_zr1 x1 -> N_zr3 x2 -> N_zS0090 (h_enc x1 x2) | T_N_148 : forall x1 x2, N_zr1 x1 -> N_zS0099 x2 -> N_zS0090 (h_enc x1 x2) | T_N_149 : forall x1 x2, N_zr1 x1 -> N_zS0100 x2 -> N_zS0090 (h_enc x1 x2) | T_N_150 : forall x1 x2, N_zr14 x1 -> N_zr15 x2 -> N_zS0090 (h_enc x1 x2) | T_N_151 : forall x1 x2, N_zr14 x1 -> N_zr21 x2 -> N_zS0090 (h_enc x1 x2) | T_N_152 : forall x1 x2, N_zr14 x1 -> N_zS0101 x2 -> N_zS0090 (h_enc x1 x2) | T_N_153 : forall x1 x2, N_zr26 x1 -> N_zr27 x2 -> N_zS0090 (h_enc x1 x2) | T_N_154 : forall x1 x2, N_zr6 x1 -> N_zr15 x2 -> N_zS0090 (h_enc x1 x2) | T_N_155 : forall x1 x2, N_zr6 x1 -> N_zS0101 x2 -> N_zS0090 (h_enc x1 x2) | T_N_156 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_enc x1 x2) | T_N_157 : forall x1 x2, N_zS0086 x1 -> N_zS0088 x2 -> N_zS0090 (h_enc x1 x2) | T_N_158 : forall x1 x2, N_zS0086 x1 -> N_zS0097 x2 -> N_zS0090 (h_enc x1 x2) | T_N_159 : forall x1 x2, N_zS0086 x1 -> N_zS0098 x2 -> N_zS0090 (h_enc x1 x2) | T_N_160 : forall x1 x2, N_zS0086 x1 -> N_zS0102 x2 -> N_zS0090 (h_enc x1 x2) | T_N_161 : forall x1 x2, N_zS0086 x1 -> N_zS0103 x2 -> N_zS0090 (h_enc x1 x2) | T_N_162 : forall x1 x2, N_zS0089 x1 -> N_zS0088 x2 -> N_zS0090 (h_enc x1 x2) | T_N_163 : forall x1 x2, N_zS0089 x1 -> N_zS0097 x2 -> N_zS0090 (h_enc x1 x2) | T_N_164 : forall x1 x2, N_zS0089 x1 -> N_zS0098 x2 -> N_zS0090 (h_enc x1 x2) | T_N_165 : forall x1 x2, N_zS0089 x1 -> N_zS0102 x2 -> N_zS0090 (h_enc x1 x2) | T_N_166 : forall x1 x2, N_zS0089 x1 -> N_zS0103 x2 -> N_zS0090 (h_enc x1 x2) | T_N_167 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zS0090 (h_f1 x1 x2 x3) | T_N_168 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zS0090 (h_f2 x1 x2 x3) | T_N_169 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zS0090 (h_f3 x1 x2 x3) | T_N_170 : forall x1 x2 x3, N_zak x1 -> N_zak x2 -> N_zak x3 -> N_zS0090 (h_f4 x1 x2 x3) | T_N_171 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_f5 x1 x2) | T_N_172 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_f6 x1 x2) | T_N_173 : forall x1 x2, N_zak x1 -> N_zak x2 -> N_zS0090 (h_h x1 x2) | T_N_174 : N_zS0090 h_imp | T_N_175 : N_zS0090 h_k3 | T_N_176 : N_zS0090 h_kp | T_N_177 : N_zS0090 h_pin with N_zS0091 : St := (* | T_N_178 : forall x1, N_zr5 x1 -> N_zS0091 x1 *) (* | T_N_179 : forall x1, N_zS0091 x1 -> N_zS0091 x1 *) | T_N_180 : forall x1 x2, N_zr5 x1 -> N_zak x2 -> N_zS0091 (h_zp x1 x2) | T_N_181 : forall x1 x2, N_zak x1 -> N_zr5 x2 -> N_zS0091 (h_zp x1 x2) | T_N_182 : forall x1 x2, N_zak x1 -> N_zS0091 x2 -> N_zS0091 (h_zp x1 x2) | T_N_183 : forall x1 x2, N_zS0091 x1 -> N_zak x2 -> N_zS0091 (h_zp x1 x2) | T_N_184 : N_zS0091 h_forbidden | T_N_185 : N_zS0091 h_kek with N_zS0092 : St := | T_N_186 : forall x1 x2, N_zr8 x1 -> N_zr8 x2 -> N_zS0092 (h_zp x1 x2) | T_N_187 : N_zS0092 h_0 with N_zS0096 : St := | T_N_188 : forall x1 x2, N_zr11 x1 -> N_zS0090 x2 -> N_zS0096 (h_h x1 x2) with N_zS0097 : St := | T_N_189 : forall x1 x2, N_zS0096 x1 -> N_zr13 x2 -> N_zS0097 (h_h x1 x2) with N_zS0098 : St := | T_N_190 : forall x1 x2, N_zr11 x1 -> N_zr13 x2 -> N_zS0098 (h_h x1 x2) with N_zS0099 : St := | T_N_191 : forall x1 x2, N_zr4 x1 -> N_zr13 x2 -> N_zS0099 (h_h x1 x2) with N_zS0100 : St := | T_N_192 : forall x1 x2, N_zr4 x1 -> N_zr26 x2 -> N_zS0100 (h_h x1 x2) with N_zS0101 : St := | T_N_193 : forall x1 x2, N_zr10 x1 -> N_zr26 x2 -> N_zS0101 (h_h x1 x2) with N_zS0102 : St := | T_N_194 : forall x1 x2, N_zS0087 x1 -> N_zr26 x2 -> N_zS0102 (h_h x1 x2) with N_zS0103 : St := | T_N_195 : forall x1 x2, N_zr11 x1 -> N_zr26 x2 -> N_zS0103 (h_h x1 x2) . (* Table of the states of both automata *) Inductive State_N : St -> Prop := | ST_zaziInters : State_N N_zaziInters | ST_zazzzzResult : State_N N_zazzzzResult | ST_zr0 : State_N N_zr0 | ST_zr1 : State_N N_zr1 | ST_zr10 : State_N N_zr10 | ST_zr11 : State_N N_zr11 | ST_zr12 : State_N N_zr12 | ST_zr13 : State_N N_zr13 | ST_zr14 : State_N N_zr14 | ST_zr15 : State_N N_zr15 | ST_zr21 : State_N N_zr21 | ST_zr22 : State_N N_zr22 | ST_zr23 : State_N N_zr23 | ST_zr26 : State_N N_zr26 | ST_zr27 : State_N N_zr27 | ST_zr3 : State_N N_zr3 | ST_zr4 : State_N N_zr4 | ST_zr5 : State_N N_zr5 | ST_zr6 : State_N N_zr6 | ST_zr8 : State_N N_zr8 | ST_zaforbidden : State_N N_zaforbidden | ST_zak : State_N N_zak | ST_zapublic : State_N N_zapublic | ST_zasecret : State_N N_zasecret | ST_zS0086 : State_N N_zS0086 | ST_zS0087 : State_N N_zS0087 | ST_zS0088 : State_N N_zS0088 | ST_zS0089 : State_N N_zS0089 | ST_zS0090 : State_N N_zS0090 | ST_zS0091 : State_N N_zS0091 | ST_zS0092 : State_N N_zS0092 | ST_zS0096 : State_N N_zS0096 | ST_zS0097 : State_N N_zS0097 | ST_zS0098 : State_N N_zS0098 | ST_zS0099 : State_N N_zS0099 | ST_zS0100 : State_N N_zS0100 | ST_zS0101 : State_N N_zS0101 | ST_zS0102 : State_N N_zS0102 | ST_zS0103 : State_N N_zS0103 . Ltac knownState := match goal with | |- State_N _ => solve [ apply ST_zaziInters | apply ST_zazzzzResult | apply ST_zr0 | apply ST_zr1 | apply ST_zr10 | apply ST_zr11 | apply ST_zr12 | apply ST_zr13 | apply ST_zr14 | apply ST_zr15 | apply ST_zr21 | apply ST_zr22 | apply ST_zr23 | apply ST_zr26 | apply ST_zr27 | apply ST_zr3 | apply ST_zr4 | apply ST_zr5 | apply ST_zr6 | apply ST_zr8 | apply ST_zaforbidden | apply ST_zak | apply ST_zapublic | apply ST_zasecret | apply ST_zS0086 | apply ST_zS0087 | apply ST_zS0088 | apply ST_zS0089 | apply ST_zS0090 | apply ST_zS0091 | apply ST_zS0092 | apply ST_zS0096 | apply ST_zS0097 | apply ST_zS0098 | apply ST_zS0099 | apply ST_zS0100 | apply ST_zS0101 | apply ST_zS0102 | apply ST_zS0103 ] end . Ltac apply_transitionsN_tac tac := intros ; try assumption ; first [ apply T_N_0 ; try assumption ; tac | apply T_N_1 ; try assumption ; tac | apply T_N_10 ; try assumption ; tac | apply T_N_100 ; try assumption ; tac | apply T_N_101 ; try assumption ; tac | apply T_N_102 ; try assumption ; tac | apply T_N_103 ; try assumption ; tac | apply T_N_104 ; try assumption ; tac | apply T_N_105 ; try assumption ; tac | apply T_N_106 ; try assumption ; tac | apply T_N_107 ; try assumption ; tac | apply T_N_108 ; try assumption ; tac | apply T_N_109 ; try assumption ; tac | apply T_N_11 ; try assumption ; tac | apply T_N_110 ; try assumption ; tac | apply T_N_111 ; try assumption ; tac | apply T_N_112 ; try assumption ; tac | apply T_N_113 ; try assumption ; tac | apply T_N_114 ; try assumption ; tac | apply T_N_115 ; try assumption ; tac | apply T_N_116 ; try assumption ; tac | apply T_N_117 ; try assumption ; tac | apply T_N_118 ; try assumption ; tac | apply T_N_119 ; try assumption ; tac | apply T_N_12 ; try assumption ; tac | apply T_N_120 ; try assumption ; tac | apply T_N_121 ; 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_13 ; try assumption ; tac | apply T_N_130 ; try assumption ; tac | apply T_N_131 ; 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_14 ; 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_147 ; try assumption ; tac | apply T_N_148 ; try assumption ; tac | apply T_N_149 ; try assumption ; tac | apply T_N_15 ; try assumption ; tac | apply T_N_150 ; try assumption ; tac | apply T_N_151 ; 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_16 ; 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_17 ; 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_18 ; 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_188 ; try assumption ; tac | apply T_N_189 ; try assumption ; tac | apply T_N_19 ; try assumption ; tac | apply T_N_190 ; 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_2 ; try assumption ; tac | apply T_N_20 ; try assumption ; tac | apply T_N_21 ; try assumption ; tac | apply T_N_22 ; try assumption ; tac | apply T_N_23 ; try assumption ; tac | apply T_N_24 ; try assumption ; tac | apply T_N_25 ; try assumption ; tac | apply T_N_26 ; try assumption ; tac | apply T_N_29 ; try assumption ; tac | apply T_N_3 ; try assumption ; tac | apply T_N_30 ; try assumption ; tac | apply T_N_31 ; try assumption ; tac | apply T_N_32 ; try assumption ; tac | apply T_N_33 ; try assumption ; tac | apply T_N_34 ; try assumption ; tac | apply T_N_35 ; try assumption ; tac | apply T_N_36 ; try assumption ; tac | apply T_N_37 ; try assumption ; tac | apply T_N_38 ; try assumption ; tac | apply T_N_39 ; try assumption ; tac | apply T_N_4 ; try assumption ; tac | apply T_N_40 ; try assumption ; tac | apply T_N_41 ; try assumption ; tac | apply T_N_42 ; try assumption ; tac | apply T_N_43 ; try assumption ; tac | apply T_N_44 ; try assumption ; tac | apply T_N_45 ; try assumption ; tac | apply T_N_46 ; try assumption ; tac | apply T_N_47 ; try assumption ; tac | apply T_N_48 ; try assumption ; tac | apply T_N_49 ; try assumption ; tac | apply T_N_5 ; try assumption ; tac | apply T_N_50 ; try assumption ; tac | apply T_N_51 ; try assumption ; tac | apply T_N_52 ; try assumption ; tac | apply T_N_53 ; try assumption ; tac | apply T_N_54 ; try assumption ; tac | apply T_N_55 ; try assumption ; tac | apply T_N_56 ; try assumption ; tac | apply T_N_57 ; try assumption ; tac | apply T_N_58 ; try assumption ; tac | apply T_N_59 ; try assumption ; tac | apply T_N_6 ; try assumption ; tac | apply T_N_60 ; try assumption ; tac | apply T_N_61 ; try assumption ; tac | apply T_N_62 ; try assumption ; tac | apply T_N_63 ; try assumption ; tac | apply T_N_64 ; try assumption ; tac | apply T_N_65 ; try assumption ; tac | apply T_N_66 ; try assumption ; tac | apply T_N_67 ; try assumption ; tac | apply T_N_68 ; try assumption ; tac | apply T_N_69 ; try assumption ; tac | apply T_N_7 ; try assumption ; tac | apply T_N_70 ; try assumption ; tac | apply T_N_71 ; try assumption ; tac | apply T_N_72 ; try assumption ; tac | apply T_N_73 ; try assumption ; tac | apply T_N_74 ; try assumption ; tac | apply T_N_77 ; try assumption ; tac | apply T_N_78 ; try assumption ; tac | apply T_N_79 ; try assumption ; tac | apply T_N_8 ; try assumption ; tac | apply T_N_80 ; try assumption ; tac | apply T_N_81 ; try assumption ; tac | apply T_N_82 ; try assumption ; tac | apply T_N_83 ; try assumption ; tac | apply T_N_88 ; try assumption ; tac | apply T_N_89 ; try assumption ; tac | apply T_N_9 ; try assumption ; tac | apply T_N_90 ; try assumption ; tac | apply T_N_91 ; try assumption ; tac | apply T_N_92 ; try assumption ; tac | apply T_N_93 ; try assumption ; tac | apply T_N_94 ; try assumption ; tac | apply T_N_95 ; try assumption ; tac | apply T_N_96 ; try assumption ; tac | apply T_N_97 ; try assumption ; tac | apply T_N_98 ; try assumption ; tac | apply T_N_99 ; 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 | 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 . (**************************** Rewriting Relation, _not_ closed under contexts ****************************) Inductive R : term -> term -> Prop := | R_1 : forall V_K V_M , R (h_dec (h_enc V_M V_K) V_K) V_M | R_2 : forall V_X V_Y , R (h_zp V_X V_Y) (h_zp V_Y V_X) | R_3 : forall V_X V_Y V_Z , R (h_zp (h_zp V_X V_Y) V_Z) (h_zp V_X (h_zp V_Y V_Z)) | R_4 : forall V_X , R (h_zp (h_0) V_X) V_X | R_5 : forall V_X , R (h_zp V_X V_X) (h_0) | R_6 : forall V_X V_Y V_Z , R (h_f1 V_X V_Y (h_enc V_Z (h_h (h_h V_X (h_kp)) (h_km)))) (h_enc (h_zp V_Z V_Y) (h_h (h_h V_X (h_kp)) (h_km))) | R_7 : forall V_X V_Y V_Z , R (h_f2 V_X V_Y (h_enc V_Z (h_h (h_h V_X (h_kp)) (h_km)))) (h_enc (h_zp V_Z V_Y) (h_h V_X (h_km))) | R_8 : forall V_K V_T V_X , R (h_f3 V_T (h_enc V_K (h_h (h_imp) (h_km))) (h_enc V_X (h_h V_T V_K))) (h_enc V_X (h_h V_T (h_km))) | R_9 : forall V_K V_T V_X , R (h_f4 V_T (h_enc V_K (h_h (h_exp) (h_km))) (h_enc V_X (h_h V_T (h_km)))) (h_enc V_X (h_h V_T V_K)) | R_10 : forall V_K V_X , R (h_f5 V_X (h_enc V_K (h_h (h_data) (h_km)))) (h_enc V_X V_K) | R_11 : forall V_K V_X , R (h_f6 (h_enc V_X V_K) (h_enc V_K (h_h (h_data) (h_km)))) V_X | R_12 : R (h_kek) (h_forbidden) | R_13 : R (h_km) (h_forbidden) | R_14 : R (h_p) (h_forbidden) | R_15 : R (h_enc (h_acc) (h_p)) (h_forbidden) (* Full rule handled later *) . Inductive disj : St -> St -> Prop := | D_196 : disj N_zaziInters N_zazzzzResult | D_197 : disj N_zaziInters N_zr0 | D_198 : disj N_zaziInters N_zr1 | D_199 : disj N_zaziInters N_zr10 | D_200 : disj N_zaziInters N_zr11 | D_201 : disj N_zaziInters N_zr12 | D_202 : disj N_zaziInters N_zr13 | D_203 : disj N_zaziInters N_zr14 | D_204 : disj N_zaziInters N_zr15 | D_205 : disj N_zaziInters N_zr21 | D_206 : disj N_zaziInters N_zr22 | D_207 : disj N_zaziInters N_zr23 | D_208 : disj N_zaziInters N_zr26 | D_209 : disj N_zaziInters N_zr27 | D_210 : disj N_zaziInters N_zr3 | D_211 : disj N_zaziInters N_zr4 | D_212 : disj N_zaziInters N_zr5 | D_213 : disj N_zaziInters N_zr6 | D_214 : disj N_zaziInters N_zr8 | D_215 : disj N_zaziInters N_zaforbidden | D_216 : disj N_zaziInters N_zak | D_217 : disj N_zaziInters N_zapublic | D_218 : disj N_zaziInters N_zasecret | D_219 : disj N_zaziInters N_zS0086 | D_220 : disj N_zaziInters N_zS0087 | D_221 : disj N_zaziInters N_zS0088 | D_222 : disj N_zaziInters N_zS0089 | D_223 : disj N_zaziInters N_zS0090 | D_224 : disj N_zaziInters N_zS0091 | D_225 : disj N_zaziInters N_zS0092 | D_226 : disj N_zaziInters N_zS0096 | D_227 : disj N_zaziInters N_zS0097 | D_228 : disj N_zaziInters N_zS0098 | D_229 : disj N_zaziInters N_zS0099 | D_230 : disj N_zaziInters N_zS0100 | D_231 : disj N_zaziInters N_zS0101 | D_232 : disj N_zaziInters N_zS0102 | D_233 : disj N_zaziInters N_zS0103 | D_234 : disj N_zazzzzResult N_zazzzzResult | D_235 : disj N_zazzzzResult N_zr0 | D_236 : disj N_zazzzzResult N_zr1 | D_237 : disj N_zazzzzResult N_zr10 | D_238 : disj N_zazzzzResult N_zr11 | D_239 : disj N_zazzzzResult N_zr12 | D_240 : disj N_zazzzzResult N_zr13 | D_241 : disj N_zazzzzResult N_zr14 | D_242 : disj N_zazzzzResult N_zr15 | D_243 : disj N_zazzzzResult N_zr21 | D_244 : disj N_zazzzzResult N_zr22 | D_245 : disj N_zazzzzResult N_zr23 | D_246 : disj N_zazzzzResult N_zr26 | D_247 : disj N_zazzzzResult N_zr27 | D_248 : disj N_zazzzzResult N_zr3 | D_249 : disj N_zazzzzResult N_zr4 | D_250 : disj N_zazzzzResult N_zr5 | D_251 : disj N_zazzzzResult N_zr6 | D_252 : disj N_zazzzzResult N_zr8 | D_253 : disj N_zazzzzResult N_zaforbidden | D_254 : disj N_zazzzzResult N_zak | D_255 : disj N_zazzzzResult N_zapublic | D_256 : disj N_zazzzzResult N_zasecret | D_257 : disj N_zazzzzResult N_zS0086 | D_258 : disj N_zazzzzResult N_zS0087 | D_259 : disj N_zazzzzResult N_zS0088 | D_260 : disj N_zazzzzResult N_zS0089 | D_261 : disj N_zazzzzResult N_zS0090 | D_262 : disj N_zazzzzResult N_zS0091 | D_263 : disj N_zazzzzResult N_zS0092 | D_264 : disj N_zazzzzResult N_zS0096 | D_265 : disj N_zazzzzResult N_zS0097 | D_266 : disj N_zazzzzResult N_zS0098 | D_267 : disj N_zazzzzResult N_zS0099 | D_268 : disj N_zazzzzResult N_zS0100 | D_269 : disj N_zazzzzResult N_zS0101 | D_270 : disj N_zazzzzResult N_zS0102 | D_271 : disj N_zazzzzResult N_zS0103 | D_272 : disj N_zr0 N_zr1 | D_273 : disj N_zr0 N_zr10 | D_274 : disj N_zr0 N_zr11 | D_275 : disj N_zr0 N_zr12 | D_276 : disj N_zr0 N_zr13 | D_277 : disj N_zr0 N_zr14 | D_278 : disj N_zr0 N_zr15 | D_279 : disj N_zr0 N_zr21 | D_280 : disj N_zr0 N_zr22 | D_281 : disj N_zr0 N_zr23 | D_282 : disj N_zr0 N_zr26 | D_283 : disj N_zr0 N_zr27 | D_284 : disj N_zr0 N_zr3 | D_285 : disj N_zr0 N_zr4 | D_286 : disj N_zr0 N_zr5 | D_287 : disj N_zr0 N_zr6 | D_288 : disj N_zr0 N_zr8 | D_289 : disj N_zr0 N_zaforbidden | D_290 : disj N_zr0 N_zasecret | D_291 : disj N_zr0 N_zS0086 | D_292 : disj N_zr0 N_zS0087 | D_293 : disj N_zr0 N_zS0088 | D_294 : disj N_zr0 N_zS0089 | D_295 : disj N_zr0 N_zS0091 | D_296 : disj N_zr0 N_zS0092 | D_297 : disj N_zr0 N_zS0096 | D_298 : disj N_zr0 N_zS0097 | D_299 : disj N_zr0 N_zS0098 | D_300 : disj N_zr0 N_zS0099 | D_301 : disj N_zr0 N_zS0100 | D_302 : disj N_zr0 N_zS0101 | D_303 : disj N_zr0 N_zS0102 | D_304 : disj N_zr0 N_zS0103 | D_305 : disj N_zr1 N_zr10 | D_306 : disj N_zr1 N_zr11 | D_307 : disj N_zr1 N_zr12 | D_308 : disj N_zr1 N_zr14 | D_309 : disj N_zr1 N_zr15 | D_310 : disj N_zr1 N_zr21 | D_311 : disj N_zr1 N_zr22 | D_312 : disj N_zr1 N_zr23 | D_313 : disj N_zr1 N_zr26 | D_314 : disj N_zr1 N_zr27 | D_315 : disj N_zr1 N_zr3 | D_316 : disj N_zr1 N_zr4 | D_317 : disj N_zr1 N_zr6 | D_318 : disj N_zr1 N_zr8 | D_319 : disj N_zr1 N_zak | D_320 : disj N_zr1 N_zapublic | D_321 : disj N_zr1 N_zS0086 | D_322 : disj N_zr1 N_zS0087 | D_323 : disj N_zr1 N_zS0088 | D_324 : disj N_zr1 N_zS0090 | D_325 : disj N_zr1 N_zS0092 | D_326 : disj N_zr1 N_zS0096 | D_327 : disj N_zr1 N_zS0097 | D_328 : disj N_zr1 N_zS0098 | D_329 : disj N_zr1 N_zS0099 | D_330 : disj N_zr1 N_zS0100 | D_331 : disj N_zr1 N_zS0101 | D_332 : disj N_zr1 N_zS0102 | D_333 : disj N_zr1 N_zS0103 | D_334 : disj N_zr10 N_zr11 | D_335 : disj N_zr10 N_zr12 | D_336 : disj N_zr10 N_zr13 | D_337 : disj N_zr10 N_zr14 | D_338 : disj N_zr10 N_zr15 | D_339 : disj N_zr10 N_zr21 | D_340 : disj N_zr10 N_zr22 | D_341 : disj N_zr10 N_zr23 | D_342 : disj N_zr10 N_zr26 | D_343 : disj N_zr10 N_zr27 | D_344 : disj N_zr10 N_zr3 | D_345 : disj N_zr10 N_zr4 | D_346 : disj N_zr10 N_zr5 | D_347 : disj N_zr10 N_zr6 | D_348 : disj N_zr10 N_zr8 | D_349 : disj N_zr10 N_zaforbidden | D_350 : disj N_zr10 N_zapublic | D_351 : disj N_zr10 N_zasecret | D_352 : disj N_zr10 N_zS0086 | D_353 : disj N_zr10 N_zS0088 | D_354 : disj N_zr10 N_zS0089 | D_355 : disj N_zr10 N_zS0091 | D_356 : disj N_zr10 N_zS0092 | D_357 : disj N_zr10 N_zS0097 | D_358 : disj N_zr10 N_zS0098 | D_359 : disj N_zr10 N_zS0099 | D_360 : disj N_zr10 N_zS0100 | D_361 : disj N_zr10 N_zS0101 | D_362 : disj N_zr10 N_zS0102 | D_363 : disj N_zr10 N_zS0103 | D_364 : disj N_zr11 N_zr12 | D_365 : disj N_zr11 N_zr13 | D_366 : disj N_zr11 N_zr14 | D_367 : disj N_zr11 N_zr15 | D_368 : disj N_zr11 N_zr21 | D_369 : disj N_zr11 N_zr22 | D_370 : disj N_zr11 N_zr23 | D_371 : disj N_zr11 N_zr26 | D_372 : disj N_zr11 N_zr27 | D_373 : disj N_zr11 N_zr3 | D_374 : disj N_zr11 N_zr4 | D_375 : disj N_zr11 N_zr5 | D_376 : disj N_zr11 N_zr6 | D_377 : disj N_zr11 N_zr8 | D_378 : disj N_zr11 N_zaforbidden | D_379 : disj N_zr11 N_zasecret | D_380 : disj N_zr11 N_zS0086 | D_381 : disj N_zr11 N_zS0087 | D_382 : disj N_zr11 N_zS0088 | D_383 : disj N_zr11 N_zS0089 | D_384 : disj N_zr11 N_zS0091 | D_385 : disj N_zr11 N_zS0092 | D_386 : disj N_zr11 N_zS0096 | D_387 : disj N_zr11 N_zS0097 | D_388 : disj N_zr11 N_zS0098 | D_389 : disj N_zr11 N_zS0099 | D_390 : disj N_zr11 N_zS0100 | D_391 : disj N_zr11 N_zS0101 | D_392 : disj N_zr11 N_zS0102 | D_393 : disj N_zr11 N_zS0103 | D_394 : disj N_zr12 N_zr13 | D_395 : disj N_zr12 N_zr14 | D_396 : disj N_zr12 N_zr15 | D_397 : disj N_zr12 N_zr21 | D_398 : disj N_zr12 N_zr22 | D_399 : disj N_zr12 N_zr23 | D_400 : disj N_zr12 N_zr26 | D_401 : disj N_zr12 N_zr27 | D_402 : disj N_zr12 N_zr3 | D_403 : disj N_zr12 N_zr4 | D_404 : disj N_zr12 N_zr5 | D_405 : disj N_zr12 N_zr6 | D_406 : disj N_zr12 N_zr8 | D_407 : disj N_zr12 N_zaforbidden | D_408 : disj N_zr12 N_zasecret | D_409 : disj N_zr12 N_zS0086 | D_410 : disj N_zr12 N_zS0087 | D_411 : disj N_zr12 N_zS0088 | D_412 : disj N_zr12 N_zS0089 | D_413 : disj N_zr12 N_zS0091 | D_414 : disj N_zr12 N_zS0092 | D_415 : disj N_zr12 N_zS0096 | D_416 : disj N_zr12 N_zS0097 | D_417 : disj N_zr12 N_zS0098 | D_418 : disj N_zr12 N_zS0099 | D_419 : disj N_zr12 N_zS0100 | D_420 : disj N_zr12 N_zS0101 | D_421 : disj N_zr12 N_zS0102 | D_422 : disj N_zr12 N_zS0103 | D_423 : disj N_zr13 N_zr14 | D_424 : disj N_zr13 N_zr15 | D_425 : disj N_zr13 N_zr21 | D_426 : disj N_zr13 N_zr22 | D_427 : disj N_zr13 N_zr23 | D_428 : disj N_zr13 N_zr26 | D_429 : disj N_zr13 N_zr27 | D_430 : disj N_zr13 N_zr3 | D_431 : disj N_zr13 N_zr4 | D_432 : disj N_zr13 N_zr6 | D_433 : disj N_zr13 N_zr8 | D_434 : disj N_zr13 N_zak | D_435 : disj N_zr13 N_zapublic | D_436 : disj N_zr13 N_zS0086 | D_437 : disj N_zr13 N_zS0087 | D_438 : disj N_zr13 N_zS0088 | D_439 : disj N_zr13 N_zS0090 | D_440 : disj N_zr13 N_zS0092 | D_441 : disj N_zr13 N_zS0096 | D_442 : disj N_zr13 N_zS0097 | D_443 : disj N_zr13 N_zS0098 | D_444 : disj N_zr13 N_zS0099 | D_445 : disj N_zr13 N_zS0100 | D_446 : disj N_zr13 N_zS0101 | D_447 : disj N_zr13 N_zS0102 | D_448 : disj N_zr13 N_zS0103 | D_449 : disj N_zr14 N_zr15 | D_450 : disj N_zr14 N_zr21 | D_451 : disj N_zr14 N_zr22 | D_452 : disj N_zr14 N_zr23 | D_453 : disj N_zr14 N_zr26 | D_454 : disj N_zr14 N_zr27 | D_455 : disj N_zr14 N_zr3 | D_456 : disj N_zr14 N_zr4 | D_457 : disj N_zr14 N_zr5 | D_458 : disj N_zr14 N_zr6 | D_459 : disj N_zr14 N_zr8 | D_460 : disj N_zr14 N_zaforbidden | D_461 : disj N_zr14 N_zak | D_462 : disj N_zr14 N_zapublic | D_463 : disj N_zr14 N_zS0087 | D_464 : disj N_zr14 N_zS0088 | D_465 : disj N_zr14 N_zS0089 | D_466 : disj N_zr14 N_zS0090 | D_467 : disj N_zr14 N_zS0091 | D_468 : disj N_zr14 N_zS0092 | D_469 : disj N_zr14 N_zS0096 | D_470 : disj N_zr14 N_zS0097 | D_471 : disj N_zr14 N_zS0098 | D_472 : disj N_zr14 N_zS0099 | D_473 : disj N_zr14 N_zS0100 | D_474 : disj N_zr14 N_zS0101 | D_475 : disj N_zr14 N_zS0102 | D_476 : disj N_zr14 N_zS0103 | D_477 : disj N_zr15 N_zr21 | D_478 : disj N_zr15 N_zr22 | D_479 : disj N_zr15 N_zr23 | D_480 : disj N_zr15 N_zr26 | D_481 : disj N_zr15 N_zr27 | D_482 : disj N_zr15 N_zr3 | D_483 : disj N_zr15 N_zr4 | D_484 : disj N_zr15 N_zr5 | D_485 : disj N_zr15 N_zr6 | D_486 : disj N_zr15 N_zr8 | D_487 : disj N_zr15 N_zaforbidden | D_488 : disj N_zr15 N_zak | D_489 : disj N_zr15 N_zapublic | D_490 : disj N_zr15 N_zasecret | D_491 : disj N_zr15 N_zS0086 | D_492 : disj N_zr15 N_zS0087 | D_493 : disj N_zr15 N_zS0089 | D_494 : disj N_zr15 N_zS0090 | D_495 : disj N_zr15 N_zS0091 | D_496 : disj N_zr15 N_zS0092 | D_497 : disj N_zr15 N_zS0096 | D_498 : disj N_zr15 N_zS0098 | D_499 : disj N_zr15 N_zS0099 | D_500 : disj N_zr15 N_zS0100 | D_501 : disj N_zr15 N_zS0101 | D_502 : disj N_zr15 N_zS0102 | D_503 : disj N_zr15 N_zS0103 | D_504 : disj N_zr21 N_zr22 | D_505 : disj N_zr21 N_zr23 | D_506 : disj N_zr21 N_zr26 | D_507 : disj N_zr21 N_zr27 | D_508 : disj N_zr21 N_zr3 | D_509 : disj N_zr21 N_zr4 | D_510 : disj N_zr21 N_zr5 | D_511 : disj N_zr21 N_zr6 | D_512 : disj N_zr21 N_zr8 | D_513 : disj N_zr21 N_zaforbidden | D_514 : disj N_zr21 N_zak | D_515 : disj N_zr21 N_zapublic | D_516 : disj N_zr21 N_zasecret | D_517 : disj N_zr21 N_zS0086 | D_518 : disj N_zr21 N_zS0087 | D_519 : disj N_zr21 N_zS0088 | D_520 : disj N_zr21 N_zS0089 | D_521 : disj N_zr21 N_zS0090 | D_522 : disj N_zr21 N_zS0091 | D_523 : disj N_zr21 N_zS0092 | D_524 : disj N_zr21 N_zS0096 | D_525 : disj N_zr21 N_zS0097 | D_526 : disj N_zr21 N_zS0098 | D_527 : disj N_zr21 N_zS0099 | D_528 : disj N_zr21 N_zS0100 | D_529 : disj N_zr21 N_zS0101 | D_530 : disj N_zr21 N_zS0102 | D_531 : disj N_zr21 N_zS0103 | D_532 : disj N_zr22 N_zr23 | D_533 : disj N_zr22 N_zr26 | D_534 : disj N_zr22 N_zr27 | D_535 : disj N_zr22 N_zr3 | D_536 : disj N_zr22 N_zr4 | D_537 : disj N_zr22 N_zr5 | D_538 : disj N_zr22 N_zr6 | D_539 : disj N_zr22 N_zr8 | D_540 : disj N_zr22 N_zaforbidden | D_541 : disj N_zr22 N_zak | D_542 : disj N_zr22 N_zapublic | D_543 : disj N_zr22 N_zasecret | D_544 : disj N_zr22 N_zS0086 | D_545 : disj N_zr22 N_zS0087 | D_546 : disj N_zr22 N_zS0088 | D_547 : disj N_zr22 N_zS0089 | D_548 : disj N_zr22 N_zS0090 | D_549 : disj N_zr22 N_zS0091 | D_550 : disj N_zr22 N_zS0092 | D_551 : disj N_zr22 N_zS0096 | D_552 : disj N_zr22 N_zS0097 | D_553 : disj N_zr22 N_zS0098 | D_554 : disj N_zr22 N_zS0099 | D_555 : disj N_zr22 N_zS0100 | D_556 : disj N_zr22 N_zS0101 | D_557 : disj N_zr22 N_zS0102 | D_558 : disj N_zr22 N_zS0103 | D_559 : disj N_zr23 N_zr26 | D_560 : disj N_zr23 N_zr27 | D_561 : disj N_zr23 N_zr3 | D_562 : disj N_zr23 N_zr4 | D_563 : disj N_zr23 N_zr5 | D_564 : disj N_zr23 N_zr6 | D_565 : disj N_zr23 N_zr8 | D_566 : disj N_zr23 N_zaforbidden | D_567 : disj N_zr23 N_zak | D_568 : disj N_zr23 N_zapublic | D_569 : disj N_zr23 N_zasecret | D_570 : disj N_zr23 N_zS0086 | D_571 : disj N_zr23 N_zS0087 | D_572 : disj N_zr23 N_zS0088 | D_573 : disj N_zr23 N_zS0089 | D_574 : disj N_zr23 N_zS0090 | D_575 : disj N_zr23 N_zS0091 | D_576 : disj N_zr23 N_zS0092 | D_577 : disj N_zr23 N_zS0096 | D_578 : disj N_zr23 N_zS0097 | D_579 : disj N_zr23 N_zS0098 | D_580 : disj N_zr23 N_zS0099 | D_581 : disj N_zr23 N_zS0100 | D_582 : disj N_zr23 N_zS0101 | D_583 : disj N_zr23 N_zS0102 | D_584 : disj N_zr23 N_zS0103 | D_585 : disj N_zr26 N_zr27 | D_586 : disj N_zr26 N_zr3 | D_587 : disj N_zr26 N_zr4 | D_588 : disj N_zr26 N_zr5 | D_589 : disj N_zr26 N_zr6 | D_590 : disj N_zr26 N_zr8 | D_591 : disj N_zr26 N_zaforbidden | D_592 : disj N_zr26 N_zak | D_593 : disj N_zr26 N_zapublic | D_594 : disj N_zr26 N_zS0086 | D_595 : disj N_zr26 N_zS0087 | D_596 : disj N_zr26 N_zS0088 | D_597 : disj N_zr26 N_zS0089 | D_598 : disj N_zr26 N_zS0090 | D_599 : disj N_zr26 N_zS0091 | D_600 : disj N_zr26 N_zS0092 | D_601 : disj N_zr26 N_zS0096 | D_602 : disj N_zr26 N_zS0097 | D_603 : disj N_zr26 N_zS0098 | D_604 : disj N_zr26 N_zS0099 | D_605 : disj N_zr26 N_zS0100 | D_606 : disj N_zr26 N_zS0101 | D_607 : disj N_zr26 N_zS0102 | D_608 : disj N_zr26 N_zS0103 | D_609 : disj N_zr27 N_zr3 | D_610 : disj N_zr27 N_zr4 | D_611 : disj N_zr27 N_zr5 | D_612 : disj N_zr27 N_zr6 | D_613 : disj N_zr27 N_zr8 | D_614 : disj N_zr27 N_zaforbidden | D_615 : disj N_zr27 N_zak | D_616 : disj N_zr27 N_zapublic | D_617 : disj N_zr27 N_zasecret | D_618 : disj N_zr27 N_zS0086 | D_619 : disj N_zr27 N_zS0087 | D_620 : disj N_zr27 N_zS0088 | D_621 : disj N_zr27 N_zS0089 | D_622 : disj N_zr27 N_zS0090 | D_623 : disj N_zr27 N_zS0091 | D_624 : disj N_zr27 N_zS0092 | D_625 : disj N_zr27 N_zS0096 | D_626 : disj N_zr27 N_zS0097 | D_627 : disj N_zr27 N_zS0098 | D_628 : disj N_zr27 N_zS0099 | D_629 : disj N_zr27 N_zS0100 | D_630 : disj N_zr27 N_zS0101 | D_631 : disj N_zr27 N_zS0102 | D_632 : disj N_zr27 N_zS0103 | D_633 : disj N_zr3 N_zr4 | D_634 : disj N_zr3 N_zr5 | D_635 : disj N_zr3 N_zr6 | D_636 : disj N_zr3 N_zr8 | D_637 : disj N_zr3 N_zaforbidden | D_638 : disj N_zr3 N_zak | D_639 : disj N_zr3 N_zapublic | D_640 : disj N_zr3 N_zasecret | D_641 : disj N_zr3 N_zS0086 | D_642 : disj N_zr3 N_zS0087 | D_643 : disj N_zr3 N_zS0088 | D_644 : disj N_zr3 N_zS0089 | D_645 : disj N_zr3 N_zS0090 | D_646 : disj N_zr3 N_zS0091 | D_647 : disj N_zr3 N_zS0092 | D_648 : disj N_zr3 N_zS0096 | D_649 : disj N_zr3 N_zS0097 | D_650 : disj N_zr3 N_zS0098 | D_651 : disj N_zr3 N_zS0100 | D_652 : disj N_zr3 N_zS0101 | D_653 : disj N_zr3 N_zS0102 | D_654 : disj N_zr3 N_zS0103 | D_655 : disj N_zr4 N_zr5 | D_656 : disj N_zr4 N_zr6 | D_657 : disj N_zr4 N_zr8 | D_658 : disj N_zr4 N_zaforbidden | D_659 : disj N_zr4 N_zasecret | D_660 : disj N_zr4 N_zS0086 | D_661 : disj N_zr4 N_zS0087 | D_662 : disj N_zr4 N_zS0088 | D_663 : disj N_zr4 N_zS0089 | D_664 : disj N_zr4 N_zS0091 | D_665 : disj N_zr4 N_zS0092 | D_666 : disj N_zr4 N_zS0096 | D_667 : disj N_zr4 N_zS0097 | D_668 : disj N_zr4 N_zS0098 | D_669 : disj N_zr4 N_zS0099 | D_670 : disj N_zr4 N_zS0100 | D_671 : disj N_zr4 N_zS0101 | D_672 : disj N_zr4 N_zS0102 | D_673 : disj N_zr4 N_zS0103 | D_674 : disj N_zr5 N_zr6 | D_675 : disj N_zr5 N_zr8 | D_676 : disj N_zr5 N_zak | D_677 : disj N_zr5 N_zapublic | D_678 : disj N_zr5 N_zS0086 | D_679 : disj N_zr5 N_zS0087 | D_680 : disj N_zr5 N_zS0088 | D_681 : disj N_zr5 N_zS0090 | D_682 : disj N_zr5 N_zS0092 | D_683 : disj N_zr5 N_zS0096 | D_684 : disj N_zr5 N_zS0097 | D_685 : disj N_zr5 N_zS0098 | D_686 : disj N_zr5 N_zS0099 | D_687 : disj N_zr5 N_zS0100 | D_688 : disj N_zr5 N_zS0101 | D_689 : disj N_zr5 N_zS0102 | D_690 : disj N_zr5 N_zS0103 | D_691 : disj N_zr6 N_zr8 | D_692 : disj N_zr6 N_zaforbidden | D_693 : disj N_zr6 N_zak | D_694 : disj N_zr6 N_zapublic | D_695 : disj N_zr6 N_zasecret | D_696 : disj N_zr6 N_zS0086 | D_697 : disj N_zr6 N_zS0087 | D_698 : disj N_zr6 N_zS0088 | D_699 : disj N_zr6 N_zS0090 | D_700 : disj N_zr6 N_zS0092 | D_701 : disj N_zr6 N_zS0096 | D_702 : disj N_zr6 N_zS0097 | D_703 : disj N_zr6 N_zS0098 | D_704 : disj N_zr6 N_zS0099 | D_705 : disj N_zr6 N_zS0100 | D_706 : disj N_zr6 N_zS0101 | D_707 : disj N_zr6 N_zS0102 | D_708 : disj N_zr6 N_zS0103 | D_709 : disj N_zr8 N_zaforbidden | D_710 : disj N_zr8 N_zasecret | D_711 : disj N_zr8 N_zS0086 | D_712 : disj N_zr8 N_zS0087 | D_713 : disj N_zr8 N_zS0088 | D_714 : disj N_zr8 N_zS0089 | D_715 : disj N_zr8 N_zS0091 | D_716 : disj N_zr8 N_zS0092 | D_717 : disj N_zr8 N_zS0096 | D_718 : disj N_zr8 N_zS0097 | D_719 : disj N_zr8 N_zS0098 | D_720 : disj N_zr8 N_zS0099 | D_721 : disj N_zr8 N_zS0100 | D_722 : disj N_zr8 N_zS0101 | D_723 : disj N_zr8 N_zS0102 | D_724 : disj N_zr8 N_zS0103 | D_725 : disj N_zaforbidden N_zak | D_726 : disj N_zaforbidden N_zapublic | D_727 : disj N_zaforbidden N_zS0086 | D_728 : disj N_zaforbidden N_zS0087 | D_729 : disj N_zaforbidden N_zS0088 | D_730 : disj N_zaforbidden N_zS0090 | D_731 : disj N_zaforbidden N_zS0092 | D_732 : disj N_zaforbidden N_zS0096 | D_733 : disj N_zaforbidden N_zS0097 | D_734 : disj N_zaforbidden N_zS0098 | D_735 : disj N_zaforbidden N_zS0099 | D_736 : disj N_zaforbidden N_zS0100 | D_737 : disj N_zaforbidden N_zS0101 | D_738 : disj N_zaforbidden N_zS0102 | D_739 : disj N_zaforbidden N_zS0103 | D_740 : disj N_zak N_zasecret | D_741 : disj N_zak N_zS0086 | D_742 : disj N_zak N_zS0088 | D_743 : disj N_zak N_zS0089 | D_744 : disj N_zak N_zS0091 | D_745 : disj N_zak N_zS0097 | D_746 : disj N_zak N_zS0098 | D_747 : disj N_zak N_zS0099 | D_748 : disj N_zak N_zS0100 | D_749 : disj N_zak N_zS0101 | D_750 : disj N_zak N_zS0102 | D_751 : disj N_zak N_zS0103 | D_752 : disj N_zapublic N_zasecret | D_753 : disj N_zapublic N_zS0086 | D_754 : disj N_zapublic N_zS0087 | D_755 : disj N_zapublic N_zS0088 | D_756 : disj N_zapublic N_zS0089 | D_757 : disj N_zapublic N_zS0091 | D_758 : disj N_zapublic N_zS0092 | D_759 : disj N_zapublic N_zS0096 | D_760 : disj N_zapublic N_zS0097 | D_761 : disj N_zapublic N_zS0098 | D_762 : disj N_zapublic N_zS0099 | D_763 : disj N_zapublic N_zS0100 | D_764 : disj N_zapublic N_zS0101 | D_765 : disj N_zapublic N_zS0102 | D_766 : disj N_zapublic N_zS0103 | D_767 : disj N_zasecret N_zS0087 | D_768 : disj N_zasecret N_zS0088 | D_769 : disj N_zasecret N_zS0090 | D_770 : disj N_zasecret N_zS0092 | D_771 : disj N_zasecret N_zS0096 | D_772 : disj N_zasecret N_zS0097 | D_773 : disj N_zasecret N_zS0098 | D_774 : disj N_zasecret N_zS0099 | D_775 : disj N_zasecret N_zS0100 | D_776 : disj N_zasecret N_zS0101 | D_777 : disj N_zasecret N_zS0102 | D_778 : disj N_zasecret N_zS0103 | D_779 : disj N_zS0086 N_zS0087 | D_780 : disj N_zS0086 N_zS0088 | D_781 : disj N_zS0086 N_zS0089 | D_782 : disj N_zS0086 N_zS0090 | D_783 : disj N_zS0086 N_zS0091 | D_784 : disj N_zS0086 N_zS0092 | D_785 : disj N_zS0086 N_zS0096 | D_786 : disj N_zS0086 N_zS0097 | D_787 : disj N_zS0086 N_zS0098 | D_788 : disj N_zS0086 N_zS0099 | D_789 : disj N_zS0086 N_zS0100 | D_790 : disj N_zS0086 N_zS0101 | D_791 : disj N_zS0086 N_zS0102 | D_792 : disj N_zS0086 N_zS0103 | D_793 : disj N_zS0087 N_zS0088 | D_794 : disj N_zS0087 N_zS0089 | D_795 : disj N_zS0087 N_zS0091 | D_796 : disj N_zS0087 N_zS0092 | D_797 : disj N_zS0087 N_zS0097 | D_798 : disj N_zS0087 N_zS0098 | D_799 : disj N_zS0087 N_zS0099 | D_800 : disj N_zS0087 N_zS0100 | D_801 : disj N_zS0087 N_zS0101 | D_802 : disj N_zS0087 N_zS0102 | D_803 : disj N_zS0087 N_zS0103 | D_804 : disj N_zS0088 N_zS0089 | D_805 : disj N_zS0088 N_zS0090 | D_806 : disj N_zS0088 N_zS0091 | D_807 : disj N_zS0088 N_zS0092 | D_808 : disj N_zS0088 N_zS0096 | D_809 : disj N_zS0088 N_zS0098 | D_810 : disj N_zS0088 N_zS0099 | D_811 : disj N_zS0088 N_zS0100 | D_812 : disj N_zS0088 N_zS0101 | D_813 : disj N_zS0088 N_zS0102 | D_814 : disj N_zS0088 N_zS0103 | D_815 : disj N_zS0089 N_zS0090 | D_816 : disj N_zS0089 N_zS0092 | D_817 : disj N_zS0089 N_zS0096 | D_818 : disj N_zS0089 N_zS0097 | D_819 : disj N_zS0089 N_zS0098 | D_820 : disj N_zS0089 N_zS0099 | D_821 : disj N_zS0089 N_zS0100 | D_822 : disj N_zS0089 N_zS0101 | D_823 : disj N_zS0089 N_zS0102 | D_824 : disj N_zS0089 N_zS0103 | D_825 : disj N_zS0090 N_zS0091 | D_826 : disj N_zS0090 N_zS0097 | D_827 : disj N_zS0090 N_zS0098 | D_828 : disj N_zS0090 N_zS0099 | D_829 : disj N_zS0090 N_zS0100 | D_830 : disj N_zS0090 N_zS0101 | D_831 : disj N_zS0090 N_zS0102 | D_832 : disj N_zS0090 N_zS0103 | D_833 : disj N_zS0091 N_zS0092 | D_834 : disj N_zS0091 N_zS0096 | D_835 : disj N_zS0091 N_zS0097 | D_836 : disj N_zS0091 N_zS0098 | D_837 : disj N_zS0091 N_zS0099 | D_838 : disj N_zS0091 N_zS0100 | D_839 : disj N_zS0091 N_zS0101 | D_840 : disj N_zS0091 N_zS0102 | D_841 : disj N_zS0091 N_zS0103 | D_842 : disj N_zS0092 N_zS0096 | D_843 : disj N_zS0092 N_zS0097 | D_844 : disj N_zS0092 N_zS0098 | D_845 : disj N_zS0092 N_zS0099 | D_846 : disj N_zS0092 N_zS0100 | D_847 : disj N_zS0092 N_zS0101 | D_848 : disj N_zS0092 N_zS0102 | D_849 : disj N_zS0092 N_zS0103 | D_850 : disj N_zS0096 N_zS0097 | D_851 : disj N_zS0096 N_zS0098 | D_852 : disj N_zS0096 N_zS0099 | D_853 : disj N_zS0096 N_zS0100 | D_854 : disj N_zS0096 N_zS0101 | D_855 : disj N_zS0096 N_zS0102 | D_856 : disj N_zS0096 N_zS0103 | D_857 : disj N_zS0097 N_zS0098 | D_858 : disj N_zS0097 N_zS0099 | D_859 : disj N_zS0097 N_zS0100 | D_860 : disj N_zS0097 N_zS0101 | D_861 : disj N_zS0097 N_zS0102 | D_862 : disj N_zS0097 N_zS0103 | D_863 : disj N_zS0098 N_zS0099 | D_864 : disj N_zS0098 N_zS0100 | D_865 : disj N_zS0098 N_zS0101 | D_866 : disj N_zS0098 N_zS0102 | D_867 : disj N_zS0098 N_zS0103 | D_868 : disj N_zS0099 N_zS0100 | D_869 : disj N_zS0099 N_zS0101 | D_870 : disj N_zS0099 N_zS0102 | D_871 : disj N_zS0099 N_zS0103 | D_872 : disj N_zS0100 N_zS0101 | D_873 : disj N_zS0100 N_zS0102 | D_874 : disj N_zS0100 N_zS0103 | D_875 : disj N_zS0101 N_zS0103 | D_876 : disj N_zS0102 N_zS0103 . Ltac disj_table := first [ apply D_196 | apply D_197 | apply D_198 | apply D_199 | apply D_200 | apply D_201 | apply D_202 | apply D_203 | apply D_204 | apply D_205 | apply D_206 | apply D_207 | apply D_208 | apply D_209 | apply D_210 | apply D_211 | apply D_212 | apply D_213 | apply D_214 | apply D_215 | apply D_216 | apply D_217 | apply D_218 | apply D_219 | apply D_220 | apply D_221 | apply D_222 | apply D_223 | apply D_224 | apply D_225 | apply D_226 | apply D_227 | apply D_228 | apply D_229 | apply D_230 | apply D_231 | apply D_232 | apply D_233 | 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 | apply D_406 | apply D_407 | apply D_408 | apply D_409 | apply D_410 | apply D_411 | apply D_412 | apply D_413 | apply D_414 | apply D_415 | apply D_416 | apply D_417 | apply D_418 | apply D_419 | apply D_420 | apply D_421 | apply D_422 | apply D_423 | apply D_424 | apply D_425 | apply D_426 | apply D_427 | apply D_428 | apply D_429 | apply D_430 | apply D_431 | apply D_432 | apply D_433 | apply D_434 | apply D_435 | apply D_436 | apply D_437 | apply D_438 | apply D_439 | apply D_440 | apply D_441 | apply D_442 | apply D_443 | apply D_444 | apply D_445 | apply D_446 | apply D_447 | apply D_448 | apply D_449 | apply D_450 | apply D_451 | apply D_452 | apply D_453 | apply D_454 | apply D_455 | apply D_456 | apply D_457 | apply D_458 | apply D_459 | apply D_460 | apply D_461 | apply D_462 | apply D_463 | apply D_464 | apply D_465 | apply D_466 | apply D_467 | apply D_468 | apply D_469 | apply D_470 | apply D_471 | apply D_472 | apply D_473 | apply D_474 | apply D_475 | apply D_476 | apply D_477 | apply D_478 | apply D_479 | apply D_480 | apply D_481 | apply D_482 | apply D_483 | apply D_484 | apply D_485 | apply D_486 | apply D_487 | apply D_488 | apply D_489 | apply D_490 | apply D_491 | apply D_492 | apply D_493 | apply D_494 | apply D_495 | apply D_496 | apply D_497 | apply D_498 | apply D_499 | apply D_500 | apply D_501 | apply D_502 | apply D_503 | apply D_504 | apply D_505 | apply D_506 | apply D_507 | apply D_508 | apply D_509 | apply D_510 | apply D_511 | apply D_512 | apply D_513 | apply D_514 | apply D_515 | apply D_516 | apply D_517 | apply D_518 | apply D_519 | apply D_520 | apply D_521 | apply D_522 | apply D_523 | apply D_524 | apply D_525 | apply D_526 | apply D_527 | apply D_528 | apply D_529 | apply D_530 | apply D_531 | apply D_532 | apply D_533 | apply D_534 | apply D_535 | apply D_536 | apply D_537 | apply D_538 | apply D_539 | apply D_540 | apply D_541 | apply D_542 | apply D_543 | apply D_544 | apply D_545 | apply D_546 | apply D_547 | apply D_548 | apply D_549 | apply D_550 | apply D_551 | apply D_552 | apply D_553 | apply D_554 | apply D_555 | apply D_556 | apply D_557 | apply D_558 | apply D_559 | apply D_560 | apply D_561 | apply D_562 | apply D_563 | apply D_564 | apply D_565 | apply D_566 | apply D_567 | apply D_568 | apply D_569 | apply D_570 | apply D_571 | apply D_572 | apply D_573 | apply D_574 | apply D_575 | apply D_576 | apply D_577 | apply D_578 | apply D_579 | apply D_580 | apply D_581 | apply D_582 | apply D_583 | apply D_584 | apply D_585 | apply D_586 | apply D_587 | apply D_588 | apply D_589 | apply D_590 | apply D_591 | apply D_592 | apply D_593 | apply D_594 | apply D_595 | apply D_596 | apply D_597 | apply D_598 | apply D_599 | apply D_600 | apply D_601 | apply D_602 | apply D_603 | apply D_604 | apply D_605 | apply D_606 | apply D_607 | apply D_608 | apply D_609 | apply D_610 | apply D_611 | apply D_612 | apply D_613 | apply D_614 | apply D_615 | apply D_616 | apply D_617 | apply D_618 | apply D_619 | apply D_620 | apply D_621 | apply D_622 | apply D_623 | apply D_624 | apply D_625 | apply D_626 | apply D_627 | apply D_628 | apply D_629 | apply D_630 | apply D_631 | apply D_632 | apply D_633 | apply D_634 | apply D_635 | apply D_636 | apply D_637 | apply D_638 | apply D_639 | apply D_640 | apply D_641 | apply D_642 | apply D_643 | apply D_644 | apply D_645 | apply D_646 | apply D_647 | apply D_648 | apply D_649 | apply D_650 | apply D_651 | apply D_652 | apply D_653 | apply D_654 | apply D_655 | apply D_656 | apply D_657 | apply D_658 | apply D_659 | apply D_660 | apply D_661 | apply D_662 | apply D_663 | apply D_664 | apply D_665 | apply D_666 | apply D_667 | apply D_668 | apply D_669 | apply D_670 | apply D_671 | apply D_672 | apply D_673 | apply D_674 | apply D_675 | apply D_676 | apply D_677 | apply D_678 | apply D_679 | apply D_680 | apply D_681 | apply D_682 | apply D_683 | apply D_684 | apply D_685 | apply D_686 | apply D_687 | apply D_688 | apply D_689 | apply D_690 | apply D_691 | apply D_692 | apply D_693 | apply D_694 | apply D_695 | apply D_696 | apply D_697 | apply D_698 | apply D_699 | apply D_700 | apply D_701 | apply D_702 | apply D_703 | apply D_704 | apply D_705 | apply D_706 | apply D_707 | apply D_708 | apply D_709 | apply D_710 | apply D_711 | apply D_712 | apply D_713 | apply D_714 | apply D_715 | apply D_716 | apply D_717 | apply D_718 | apply D_719 | apply D_720 | apply D_721 | apply D_722 | apply D_723 | apply D_724 | apply D_725 | apply D_726 | apply D_727 | apply D_728 | apply D_729 | apply D_730 | apply D_731 | apply D_732 | apply D_733 | apply D_734 | apply D_735 | apply D_736 | apply D_737 | apply D_738 | apply D_739 | apply D_740 | apply D_741 | apply D_742 | apply D_743 | apply D_744 | apply D_745 | apply D_746 | apply D_747 | apply D_748 | apply D_749 | apply D_750 | apply D_751 | apply D_752 | apply D_753 | apply D_754 | apply D_755 | apply D_756 | apply D_757 | apply D_758 | apply D_759 | apply D_760 | apply D_761 | apply D_762 | apply D_763 | apply D_764 | apply D_765 | apply D_766 | apply D_767 | apply D_768 | apply D_769 | apply D_770 | apply D_771 | apply D_772 | apply D_773 | apply D_774 | apply D_775 | apply D_776 | apply D_777 | apply D_778 | apply D_779 | apply D_780 | apply D_781 | apply D_782 | apply D_783 | apply D_784 | apply D_785 | apply D_786 | apply D_787 | apply D_788 | apply D_789 | apply D_790 | apply D_791 | apply D_792 | apply D_793 | apply D_794 | apply D_795 | apply D_796 | apply D_797 | apply D_798 | apply D_799 | apply D_800 | apply D_801 | apply D_802 | apply D_803 | apply D_804 | apply D_805 | apply D_806 | apply D_807 | apply D_808 | apply D_809 | apply D_810 | apply D_811 | apply D_812 | apply D_813 | apply D_814 | apply D_815 | apply D_816 | apply D_817 | apply D_818 | apply D_819 | apply D_820 | apply D_821 | apply D_822 | apply D_823 | apply D_824 | apply D_825 | apply D_826 | apply D_827 | apply D_828 | apply D_829 | apply D_830 | apply D_831 | apply D_832 | apply D_833 | apply D_834 | apply D_835 | apply D_836 | apply D_837 | apply D_838 | apply D_839 | apply D_840 | apply D_841 | apply D_842 | apply D_843 | apply D_844 | apply D_845 | apply D_846 | apply D_847 | apply D_848 | apply D_849 | apply D_850 | apply D_851 | apply D_852 | apply D_853 | apply D_854 | apply D_855 | apply D_856 | apply D_857 | apply D_858 | apply D_859 | apply D_860 | apply D_861 | apply D_862 | apply D_863 | apply D_864 | apply D_865 | apply D_866 | apply D_867 | apply D_868 | apply D_869 | apply D_870 | apply D_871 | apply D_872 | apply D_873 | apply D_874 | apply D_875 | apply D_876 ] . 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 ; inversion H ; subst ; abstract ( inversion H1 ; subst ; abstract ( decomposition ; inversionVar ; abstract ( apply_transitionsN_rec || empty_intersection ))) . 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_zp : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 -> RC (h_zp t1 t2) (h_zp 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_f1 : forall t1 t2 t3 u1 u2 u3, RC t1 u1 -> RC t2 u2 -> RC t3 u3 -> RC (h_f1 t1 t2 t3) (h_f1 u1 u2 u3) | RC_h_f2 : forall t1 t2 t3 u1 u2 u3, RC t1 u1 -> RC t2 u2 -> RC t3 u3 -> RC (h_f2 t1 t2 t3) (h_f2 u1 u2 u3) | RC_h_f3 : forall t1 t2 t3 u1 u2 u3, RC t1 u1 -> RC t2 u2 -> RC t3 u3 -> RC (h_f3 t1 t2 t3) (h_f3 u1 u2 u3) | RC_h_f4 : forall t1 t2 t3 u1 u2 u3, RC t1 u1 -> RC t2 u2 -> RC t3 u3 -> RC (h_f4 t1 t2 t3) (h_f4 u1 u2 u3) | RC_h_f5 : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 -> RC (h_f5 t1 t2) (h_f5 u1 u2) | RC_h_f6 : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 -> RC (h_f6 t1 t2) (h_f6 u1 u2) | RC_h_fst : forall t1 u1, RC t1 u1 -> RC (h_fst t1) (h_fst u1) | RC_h_h : forall t1 t2 u1 u2, RC t1 u1 -> RC t2 u2 -> RC (h_h t1 t2) (h_h u1 u2) | 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 S1 ; intros ; 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. (* 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. (**************************** The User Input Automaton ****************************) Inductive O_zr0 : St := | T_O_877 : O_zr0 h_acc | T_O_878 : forall t1 t2 , O_zr0 t1 -> RCs t1 t2 -> O_zr0 t2 with O_zr1 : St := | T_O_879 : O_zr1 h_p | T_O_880 : forall t1 t2 , O_zr1 t1 -> RCs t1 t2 -> O_zr1 t2 with O_zr10 : St := | T_O_881 : forall x1 x2, O_zr11 x1 -> O_zr12 x2 -> O_zr10 (h_h x1 x2) | T_O_882 : forall t1 t2 , O_zr10 t1 -> RCs t1 t2 -> O_zr10 t2 with O_zr11 : St := | T_O_883 : O_zr11 h_imp | T_O_884 : forall t1 t2 , O_zr11 t1 -> RCs t1 t2 -> O_zr11 t2 with O_zr12 : St := | T_O_885 : O_zr12 h_kp | T_O_886 : forall t1 t2 , O_zr12 t1 -> RCs t1 t2 -> O_zr12 t2 with O_zr13 : St := | T_O_887 : O_zr13 h_km | T_O_888 : forall t1 t2 , O_zr13 t1 -> RCs t1 t2 -> O_zr13 t2 with O_zr14 : St := | T_O_889 : O_zr14 h_kek2 | T_O_890 : forall t1 t2 , O_zr14 t1 -> RCs t1 t2 -> O_zr14 t2 with O_zr15 : St := | T_O_891 : forall x1 x2, O_zr16 x1 -> O_zr19 x2 -> O_zr15 (h_h x1 x2) | T_O_892 : forall t1 t2 , O_zr15 t1 -> RCs t1 t2 -> O_zr15 t2 with O_zr16 : St := | T_O_893 : forall x1 x2, O_zr17 x1 -> O_zr18 x2 -> O_zr16 (h_h x1 x2) | T_O_894 : forall t1 t2 , O_zr16 t1 -> RCs t1 t2 -> O_zr16 t2 with O_zr17 : St := | T_O_895 : O_zr17 h_imp | T_O_896 : forall t1 t2 , O_zr17 t1 -> RCs t1 t2 -> O_zr17 t2 with O_zr18 : St := | T_O_897 : O_zr18 h_kp | T_O_898 : forall t1 t2 , O_zr18 t1 -> RCs t1 t2 -> O_zr18 t2 with O_zr19 : St := | T_O_899 : O_zr19 h_km | T_O_900 : forall t1 t2 , O_zr19 t1 -> RCs t1 t2 -> O_zr19 t2 with O_zr2 : St := | T_O_901 : O_zr2 h_p | T_O_902 : forall t1 t2 , O_zr2 t1 -> RCs t1 t2 -> O_zr2 t2 with O_zr20 : St := | T_O_903 : O_zr20 h_kek2 | T_O_904 : forall t1 t2 , O_zr20 t1 -> RCs t1 t2 -> O_zr20 t2 with O_zr21 : St := | T_O_905 : forall x1 x2, O_zr22 x1 -> O_zr25 x2 -> O_zr21 (h_h x1 x2) | T_O_906 : forall t1 t2 , O_zr21 t1 -> RCs t1 t2 -> O_zr21 t2 with O_zr22 : St := | T_O_907 : forall x1 x2, O_zr23 x1 -> O_zr24 x2 -> O_zr22 (h_h x1 x2) | T_O_908 : forall t1 t2 , O_zr22 t1 -> RCs t1 t2 -> O_zr22 t2 with O_zr23 : St := | T_O_909 : O_zr23 h_exp | T_O_910 : forall t1 t2 , O_zr23 t1 -> RCs t1 t2 -> O_zr23 t2 with O_zr24 : St := | T_O_911 : O_zr24 h_kp | T_O_912 : forall t1 t2 , O_zr24 t1 -> RCs t1 t2 -> O_zr24 t2 with O_zr25 : St := | T_O_913 : O_zr25 h_km | T_O_914 : forall t1 t2 , O_zr25 t1 -> RCs t1 t2 -> O_zr25 t2 with O_zr26 : St := | T_O_915 : O_zr26 h_exp1 | T_O_916 : forall t1 t2 , O_zr26 t1 -> RCs t1 t2 -> O_zr26 t2 with O_zr27 : St := | T_O_917 : forall x1 x2, O_zr28 x1 -> O_zr29 x2 -> O_zr27 (h_h x1 x2) | T_O_918 : forall t1 t2 , O_zr27 t1 -> RCs t1 t2 -> O_zr27 t2 with O_zr28 : St := | T_O_919 : O_zr28 h_exp | T_O_920 : forall t1 t2 , O_zr28 t1 -> RCs t1 t2 -> O_zr28 t2 with O_zr29 : St := | T_O_921 : O_zr29 h_km | T_O_922 : forall t1 t2 , O_zr29 t1 -> RCs t1 t2 -> O_zr29 t2 with O_zr3 : St := | T_O_923 : forall x1 x2, O_zr4 x1 -> O_zr5 x2 -> O_zr3 (h_h x1 x2) | T_O_924 : forall t1 t2 , O_zr3 t1 -> RCs t1 t2 -> O_zr3 t2 with O_zr4 : St := | T_O_925 : O_zr4 h_pin | T_O_926 : forall t1 t2 , O_zr4 t1 -> RCs t1 t2 -> O_zr4 t2 with O_zr5 : St := | T_O_927 : O_zr5 h_kek | T_O_928 : forall t1 t2 , O_zr5 t1 -> RCs t1 t2 -> O_zr5 t2 with O_zr6 : St := | T_O_929 : forall x1 x2, O_zr7 x1 -> O_zr8 x2 -> O_zr6 (h_zp x1 x2) | T_O_930 : forall t1 t2 , O_zr6 t1 -> RCs t1 t2 -> O_zr6 t2 with O_zr7 : St := | T_O_931 : O_zr7 h_kek | T_O_932 : forall t1 t2 , O_zr7 t1 -> RCs t1 t2 -> O_zr7 t2 with O_zr8 : St := | T_O_933 : O_zr8 h_k3 | T_O_934 : forall t1 t2 , O_zr8 t1 -> RCs t1 t2 -> O_zr8 t2 with O_zr9 : St := | T_O_935 : forall x1 x2, O_zr10 x1 -> O_zr13 x2 -> O_zr9 (h_h x1 x2) | T_O_936 : forall t1 t2 , O_zr9 t1 -> RCs t1 t2 -> O_zr9 t2 with O_zaforbidden : St := | T_O_937 : O_zaforbidden h_kek | T_O_938 : O_zaforbidden h_km | T_O_939 : O_zaforbidden h_p | T_O_940 : forall x1 x2, O_zr0 x1 -> O_zr1 x2 -> O_zaforbidden (h_enc x1 x2) | T_O_941 : forall t1 t2 , O_zaforbidden t1 -> RCs t1 t2 -> O_zaforbidden t2 with O_zak : St := | T_O_942 : O_zak h_0 | T_O_943 : forall x1, O_zapublic x1 -> O_zak x1 | T_O_944 : forall x1 x2, O_zr2 x1 -> O_zr3 x2 -> O_zak (h_enc x1 x2) | T_O_945 : forall x1 x2, O_zr6 x1 -> O_zr9 x2 -> O_zak (h_enc x1 x2) | T_O_946 : forall x1 x2, O_zr14 x1 -> O_zr15 x2 -> O_zak (h_enc x1 x2) | T_O_947 : forall x1 x2, O_zr20 x1 -> O_zr21 x2 -> O_zak (h_enc x1 x2) | T_O_948 : forall x1 x2, O_zr26 x1 -> O_zr27 x2 -> O_zak (h_enc x1 x2) | T_O_949 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_zp x1 x2) | T_O_950 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_h x1 x2) | T_O_951 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_enc x1 x2) | T_O_952 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_dec x1 x2) | T_O_953 : forall x1 x2 x3, O_zak x1 -> O_zak x2 -> O_zak x3 -> O_zak (h_f1 x1 x2 x3) | T_O_954 : forall x1 x2 x3, O_zak x1 -> O_zak x2 -> O_zak x3 -> O_zak (h_f2 x1 x2 x3) | T_O_955 : forall x1 x2 x3, O_zak x1 -> O_zak x2 -> O_zak x3 -> O_zak (h_f3 x1 x2 x3) | T_O_956 : forall x1 x2 x3, O_zak x1 -> O_zak x2 -> O_zak x3 -> O_zak (h_f4 x1 x2 x3) | T_O_957 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_f5 x1 x2) | T_O_958 : forall x1 x2, O_zak x1 -> O_zak x2 -> O_zak (h_f6 x1 x2) | T_O_959 : forall t1 t2 , O_zak t1 -> RCs t1 t2 -> O_zak t2 with O_zapublic : St := | T_O_960 : O_zapublic h_data | T_O_961 : O_zapublic h_pin | T_O_962 : O_zapublic h_imp | T_O_963 : O_zapublic h_k3 | T_O_964 : O_zapublic h_acc | T_O_965 : O_zapublic h_kp | T_O_966 : forall t1 t2 , O_zapublic t1 -> RCs t1 t2 -> O_zapublic t2 with O_zasecret : St := | T_O_967 : O_zasecret h_km | T_O_968 : O_zasecret h_kek | T_O_969 : O_zasecret h_p | T_O_970 : O_zasecret h_kek2 | T_O_971 : O_zasecret h_exp1 | T_O_972 : forall t1 t2 , O_zasecret t1 -> RCs t1 t2 -> O_zasecret t2 with O_zazzzzResult : St := | T_O_973 : 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_zr13 := Minimality for O_zr13 Sort Prop with Min_O_zr14 := Minimality for O_zr14 Sort Prop with Min_O_zr15 := Minimality for O_zr15 Sort Prop with Min_O_zr16 := Minimality for O_zr16 Sort Prop with Min_O_zr17 := Minimality for O_zr17 Sort Prop with Min_O_zr18 := Minimality for O_zr18 Sort Prop with Min_O_zr19 := Minimality for O_zr19 Sort Prop with Min_O_zr2 := Minimality for O_zr2 Sort Prop with Min_O_zr20 := Minimality for O_zr20 Sort Prop with Min_O_zr21 := Minimality for O_zr21 Sort Prop with Min_O_zr22 := Minimality for O_zr22 Sort Prop with Min_O_zr23 := Minimality for O_zr23 Sort Prop with Min_O_zr24 := Minimality for O_zr24 Sort Prop with Min_O_zr25 := Minimality for O_zr25 Sort Prop with Min_O_zr26 := Minimality for O_zr26 Sort Prop with Min_O_zr27 := Minimality for O_zr27 Sort Prop with Min_O_zr28 := Minimality for O_zr28 Sort Prop with Min_O_zr29 := Minimality for O_zr29 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_zaforbidden := Minimality for O_zaforbidden Sort Prop with Min_O_zak := Minimality for O_zak Sort Prop with Min_O_zapublic := Minimality for O_zapublic Sort Prop with Min_O_zasecret := Minimality for O_zasecret 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_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr1 := Min_O_zr1 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr10 := Min_O_zr10 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr11 := Min_O_zr11 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr12 := Min_O_zr12 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr13 := Min_O_zr13 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr14 := Min_O_zr14 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr15 := Min_O_zr15 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr16 := Min_O_zr16 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr17 := Min_O_zr17 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr18 := Min_O_zr18 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr19 := Min_O_zr19 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr2 := Min_O_zr2 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr20 := Min_O_zr20 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr21 := Min_O_zr21 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr22 := Min_O_zr22 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr23 := Min_O_zr23 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr24 := Min_O_zr24 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr25 := Min_O_zr25 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr26 := Min_O_zr26 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr27 := Min_O_zr27 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr28 := Min_O_zr28 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr29 := Min_O_zr29 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr3 := Min_O_zr3 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr4 := Min_O_zr4 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr5 := Min_O_zr5 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr6 := Min_O_zr6 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr7 := Min_O_zr7 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr8 := Min_O_zr8 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zr9 := Min_O_zr9 N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zaforbidden := Min_O_zaforbidden N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zak := Min_O_zak N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zapublic := Min_O_zapublic N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zasecret := Min_O_zasecret N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret N_zazzzzResult . Definition Min_sat_O_zazzzzResult := Min_O_zazzzzResult N_zr0 N_zr1 N_zr10 N_zr11 N_zr12 N_zr13 N_zr14 N_zr15 N_zr10 N_zr11 N_zr12 N_zr13 N_zr1 N_zr14 N_zr21 N_zr22 N_zr23 N_zr12 N_zr13 N_zr26 N_zr27 N_zr23 N_zr13 N_zr3 N_zr4 N_zr5 N_zr6 N_zr5 N_zr8 N_zr15 N_zaforbidden N_zak N_zapublic N_zasecret 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_zr13 : incl_N O_zr13 N_zr13 | Incl_O_zr14 : incl_N O_zr14 N_zr14 | Incl_O_zr15 : incl_N O_zr15 N_zr15 | Incl_O_zr16 : incl_N O_zr16 N_zr10 | Incl_O_zr17 : incl_N O_zr17 N_zr11 | Incl_O_zr18 : incl_N O_zr18 N_zr12 | Incl_O_zr19 : incl_N O_zr19 N_zr13 | Incl_O_zr2 : incl_N O_zr2 N_zr1 | Incl_O_zr20 : incl_N O_zr20 N_zr14 | Incl_O_zr21 : incl_N O_zr21 N_zr21 | Incl_O_zr22 : incl_N O_zr22 N_zr22 | Incl_O_zr23 : incl_N O_zr23 N_zr23 | Incl_O_zr24 : incl_N O_zr24 N_zr12 | Incl_O_zr25 : incl_N O_zr25 N_zr13 | Incl_O_zr26 : incl_N O_zr26 N_zr26 | Incl_O_zr27 : incl_N O_zr27 N_zr27 | Incl_O_zr28 : incl_N O_zr28 N_zr23 | Incl_O_zr29 : incl_N O_zr29 N_zr13 | 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_zr5 | Incl_O_zr6 : incl_N O_zr6 N_zr6 | Incl_O_zr7 : incl_N O_zr7 N_zr5 | Incl_O_zr8 : incl_N O_zr8 N_zr8 | Incl_O_zr9 : incl_N O_zr9 N_zr15 | Incl_O_zaforbidden : incl_N O_zaforbidden N_zaforbidden | Incl_O_zak : incl_N O_zak N_zak | Incl_O_zapublic : incl_N O_zapublic N_zapublic | Incl_O_zasecret : incl_N O_zasecret N_zasecret | Incl_O_zazzzzResult : incl_N O_zazzzzResult N_zazzzzResult . 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_zr13 | apply Min_sat_O_zr14 | apply Min_sat_O_zr15 | apply Min_sat_O_zr16 | apply Min_sat_O_zr17 | apply Min_sat_O_zr18 | apply Min_sat_O_zr19 | apply Min_sat_O_zr2 | apply Min_sat_O_zr20 | apply Min_sat_O_zr21 | apply Min_sat_O_zr22 | apply Min_sat_O_zr23 | apply Min_sat_O_zr24 | apply Min_sat_O_zr25 | apply Min_sat_O_zr26 | apply Min_sat_O_zr27 | apply Min_sat_O_zr28 | apply Min_sat_O_zr29 | 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_zaforbidden | apply Min_sat_O_zak | apply Min_sat_O_zapublic | apply Min_sat_O_zasecret | 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. (* User Full Rule Facts (usually, the goal of the analysis) *) 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 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_zak h_forbidden -> N_zazzzzResult h_ziFAILzi . Proof. intros ; (apply_transitionsN_once || decomposition) . Save. Lemma Unreachability_1 : ~ O_zak h_forbidden . 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_zak N_zak h_forbidden Incl_O_zak H . Save.