src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
child 67399 eab6ce8368fa
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     1 (*  Title:      HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
     2     Author:     Nik Sultana, Cambridge University Computer Laboratory
     3 
     4 Unit tests for proof reconstruction module.
     5 *)
     6 
     7 theory TPTP_Proof_Reconstruction_Test_Units
     8 imports TPTP_Test TPTP_Proof_Reconstruction
     9 begin
    10 
    11 declare [[ML_exception_trace, ML_print_depth = 200]]
    12 
    13 declare [[tptp_trace_reconstruction = true]]
    14 
    15 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
    16 apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
    17 oops
    18 
    19 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
    20 apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
    21 apply (rule allI)+
    22 apply (tactic \<open>nominal_inst_parametermatch_tac @{context} @{thm allE} 1\<close>)+
    23 oops
    24 
    25 (*Could test bind_tac further with NUM667^1 inode43*)
    26 
    27 (*
    28   (* SEU581^2.p_nux *)
    29      (* (Annotated_step ("inode1", "bind"), *)
    30 lemma "\<forall>(SV5::TPTP_Interpret.ind \<Rightarrow> bool)
    31             SV6::TPTP_Interpret.ind.
    32             (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    33               (bnd_powerset bnd_sK1_A) =
    34              bnd_in (bnd_dsetconstr SV6 SV5)
    35               (bnd_powerset SV6)) =
    36             False \<Longrightarrow>
    37          (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    38            (bnd_powerset bnd_sK1_A) =
    39           bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    40            (bnd_powerset bnd_sK1_A)) =
    41          False"
    42 ML_prf {*
    43 open TPTP_Syntax;
    44 open TPTP_Proof;
    45 
    46 
    47 val binds =
    48 [Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))), Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))])))]
    49 (* |> TPTP_Reconstruct.permute *)
    50 
    51 (*
    52 val binds =
    53 [Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))),
    54 Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))
    55 ]
    56 *)
    57 
    58 val tec =
    59 (*
    60   map (bind_tac @{context} (hd prob_names)) binds
    61   |> FIRST
    62 *)
    63   bind_tac @{context} (hd prob_names) binds
    64 *}
    65 apply (tactic {*tec*})
    66 done
    67 
    68      (* (Annotated_step ("inode2", "bind"), *)
    69 lemma "\<forall>(SV7::TPTP_Interpret.ind) SV8::TPTP_Interpret.ind.
    70             (bnd_subset SV8 SV7 =
    71              bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    72               bnd_sK1_A) =
    73             False \<or>
    74             bnd_in SV8 (bnd_powerset SV7) = False \<Longrightarrow>
    75          (bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    76            bnd_sK1_A =
    77           bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    78            bnd_sK1_A) =
    79          False \<or>
    80          bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15)
    81           (bnd_powerset bnd_sK1_A) =
    82          False"
    83 ML_prf {*
    84 open TPTP_Syntax;
    85 open TPTP_Proof;
    86 
    87 
    88 val binds =
    89 [Bind ("SV8", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "dsetconstr", []))), Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))]), Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK2_SY15", []))), Atom (THF_Atom_term (Term_Var "SX0"))]))])), Bind ("SV7", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", []))))]
    90 (* |> TPTP_Reconstruct.permute *)
    91 
    92 val tec =
    93 (*
    94   map (bind_tac @{context} (hd prob_names)) binds
    95   |> FIRST
    96 *)
    97   bind_tac @{context} (hd prob_names) binds
    98 *}
    99 apply (tactic {*tec*})
   100 done
   101 *)
   102 
   103 (*
   104 from SEU897^5
   105 lemma "
   106 \<forall>SV9 SV10 SV11 SV12 SV13 SV14.
   107    (((((bnd_sK5_SY14 SV14 SV13 SV12 = SV11) = False \<or>
   108        (bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 SV11)) =
   109        False) \<or>
   110       bnd_cR SV14 = False) \<or>
   111      (SV12 = SV13 SV14) = False) \<or>
   112     bnd_cR SV9 = False) \<or>
   113    (SV11 = SV10 SV9) = False \<Longrightarrow>
   114 \<forall>SV14 SV13 SV12 SV10 SV9.
   115    (((((bnd_sK5_SY14 SV14 SV13 SV12 =
   116         bnd_sK5_SY14 SV14 SV13 SV12) =
   117        False \<or>
   118        (bnd_sK4_SX0 =
   119         SV10
   120          (bnd_sK5_SY14 SV9 SV10
   121            (bnd_sK5_SY14 SV14 SV13 SV12))) =
   122        False) \<or>
   123       bnd_cR SV14 = False) \<or>
   124      (SV12 = SV13 SV14) = False) \<or>
   125     bnd_cR SV9 = False) \<or>
   126    (bnd_sK5_SY14 SV14 SV13 SV12 = SV10 SV9) = False"
   127 ML_prf {*
   128 open TPTP_Syntax;
   129 open TPTP_Proof;
   130 
   131 val binds =
   132 [Bind ("SV11", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [Atom (THF_Atom_term (Term_Func (Uninterpreted "sK5_SY14", []))), Atom (THF_Atom_term (Term_Var "SV14"))]), Atom (THF_Atom_term (Term_Var "SV13"))]), Atom (THF_Atom_term (Term_Var "SV12"))]))]
   133 
   134 val tec = bind_tac @{context} (hd prob_names) binds
   135 *}
   136 apply (tactic {*tec*})
   137 done
   138 *)
   139 
   140 
   141 subsection "Interpreting the inferences"
   142 
   143 (*from SET598^5
   144 lemma "(bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
   145    ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
   146     (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   147    (\<forall>SY27.
   148        (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
   149        (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
   150        (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30))) =
   151   False \<Longrightarrow>
   152   (\<not> (bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17) \<longrightarrow>
   153       ((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
   154        (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   155       (\<forall>SY27.
   156           (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
   157           (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
   158           (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)))) =
   159   True"
   160 apply (tactic {*polarity_switch_tac @{context}*})
   161 done
   162 lemma "
   163   (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
   164     (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   165    (\<forall>SY27.
   166        (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
   167        (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
   168        (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
   169    bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17)) =
   170   False \<Longrightarrow>
   171   (\<not> (((\<forall>SY25. bnd_sK1_X SY25 \<longrightarrow> bnd_sK2_Y SY25) \<and>
   172        (\<forall>SY26. bnd_sK1_X SY26 \<longrightarrow> bnd_sK3_Z SY26)) \<and>
   173       (\<forall>SY27.
   174           (\<forall>SY21. SY27 SY21 \<longrightarrow> bnd_sK2_Y SY21) \<and>
   175           (\<forall>SY15. SY27 SY15 \<longrightarrow> bnd_sK3_Z SY15) \<longrightarrow>
   176           (\<forall>SY30. SY27 SY30 \<longrightarrow> bnd_sK1_X SY30)) \<longrightarrow>
   177       bnd_sK1_X = (\<lambda>SY17. bnd_sK2_Y SY17 \<and> bnd_sK3_Z SY17))) =
   178   True"
   179 apply (tactic {*polarity_switch_tac @{context}*})
   180 done
   181 *)
   182 
   183 (* beware lack of type annotations
   184 (* lemma "!!x. (A x = B x) = False ==> (B x = A x) = False" *)
   185 (* lemma "!!x. (A x = B x) = True ==> (B x = A x) = True" *)
   186 (* lemma "((A x) = (B x)) = True ==> ((B x) = (A x)) = True" *)
   187 lemma "(A = B) = True ==> (B = A) = True"
   188 *)
   189 lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False"
   190 apply (tactic \<open>expander_animal @{context} 1\<close>)
   191 oops
   192 
   193 lemma "(A & B) ==> ~(~A | ~B)"
   194 by (tactic \<open>expander_animal @{context} 1\<close>)
   195 
   196 lemma "(A | B) ==> ~(~A & ~B)"
   197 by (tactic \<open>expander_animal @{context} 1\<close>)
   198 
   199 lemma "(A | B) | C ==> A | (B | C)"
   200 by (tactic \<open>expander_animal @{context} 1\<close>)
   201 
   202 lemma "(~~A) = B ==> A = B"
   203 by (tactic \<open>expander_animal @{context} 1\<close>)
   204 
   205 lemma "~ ~ (A = True) ==> A = True"
   206 by (tactic \<open>expander_animal @{context} 1\<close>)
   207 
   208 (*This might not be a goal which might realistically arise:
   209 lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *)
   210 lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))"
   211 apply (tactic \<open>expander_animal @{context} 1\<close>)+
   212 apply (rule conjI)
   213 apply assumption
   214 apply (rule sym, assumption)
   215 done
   216 
   217 lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))"
   218 by (tactic \<open>expander_animal @{context} 1\<close>)+
   219 
   220 (*some lemmas assume constants in the signature of PUZ114^5*)
   221 consts
   222   PUZ114_5_bnd_sK1 :: "TPTP_Interpret.ind"
   223   PUZ114_5_bnd_sK2 :: "TPTP_Interpret.ind"
   224   PUZ114_5_bnd_sK3 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
   225   PUZ114_5_bnd_sK4 :: "(TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
   226   PUZ114_5_bnd_sK5 :: "(TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
   227   PUZ114_5_bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
   228   PUZ114_5_bnd_c1 :: TPTP_Interpret.ind
   229 
   230 (*testing logical expansion*)
   231 lemma "!! SY30. (SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1 \<and>
   232        (\<forall>Xj Xk.
   233            SY30 Xj Xk \<longrightarrow>
   234            SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
   235            SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)) \<longrightarrow>
   236        SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2)
   237 ==> (
   238        (~ SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1)
   239      | (~ (\<forall>Xj Xk.
   240            SY30 Xj Xk \<longrightarrow>
   241            SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk \<and>
   242            SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)))
   243      | SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2
   244 )"
   245 by (tactic \<open>expander_animal @{context} 1\<close>)+
   246 
   247 (*
   248 extcnf_forall_pos:
   249 
   250      (! X. L1) | ... | Ln
   251  ----------------------------   X' fresh
   252   ! X'. (L1[X'/X] | ... | Ln)
   253 
   254 After elimination rule has been applied we'll have a subgoal which looks like this:
   255             (! X. L1)
   256  ----------------------------   X' fresh
   257   ! X'. (L1[X'/X] | ... | Ln)
   258 and we need to transform it so that, in Isabelle, we go from
   259  (! X. L1) ==> ! X'. (L1[X'/X] | ... | Ln)
   260 to
   261  \<And> X'. L1[X'/X] ==> (L1[X'/X] | ... | Ln)
   262 (where X' is fresh, or renamings are done suitably).*)
   263 
   264 lemma "A | B \<Longrightarrow> A | B | C"
   265 apply (tactic \<open>flip_conclusion_tac @{context} 1\<close>)+
   266 apply (tactic \<open>break_hypotheses 1\<close>)+
   267 oops
   268 
   269 consts
   270   CSR122_1_bnd_lBill_THFTYPE_i :: TPTP_Interpret.ind
   271   CSR122_1_bnd_lMary_THFTYPE_i :: TPTP_Interpret.ind
   272   CSR122_1_bnd_lSue_THFTYPE_i :: TPTP_Interpret.ind
   273   CSR122_1_bnd_n2009_THFTYPE_i :: TPTP_Interpret.ind
   274   CSR122_1_bnd_lYearFn_THFTYPE_IiiI :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
   275   CSR122_1_bnd_holdsDuring_THFTYPE_IiooI ::
   276     "TPTP_Interpret.ind \<Rightarrow> bool \<Rightarrow> bool"
   277   CSR122_1_bnd_likes_THFTYPE_IiioI ::
   278     "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
   279 
   280 lemma "\<forall>SV2. (CSR122_1_bnd_holdsDuring_THFTYPE_IiooI
   281                  (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i)
   282                  (\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
   283                         CSR122_1_bnd_lMary_THFTYPE_i
   284                         CSR122_1_bnd_lBill_THFTYPE_i \<or>
   285                      \<not> CSR122_1_bnd_likes_THFTYPE_IiioI
   286                         CSR122_1_bnd_lSue_THFTYPE_i
   287                         CSR122_1_bnd_lBill_THFTYPE_i)) =
   288                 CSR122_1_bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
   289                False \<Longrightarrow>
   290          \<forall>SV2. (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i =
   291                 SV2) =
   292                False \<or>
   293                ((\<not> (\<not> CSR122_1_bnd_likes_THFTYPE_IiioI
   294                        CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i \<or>
   295                     \<not> CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i
   296                        CSR122_1_bnd_lBill_THFTYPE_i)) =
   297                 True) =
   298                False"
   299 apply (rule allI, erule_tac x = "SV2" in allE)
   300 apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
   301 done
   302 
   303 (*SEU882^5*)
   304 (*
   305 lemma
   306  "\<forall>(SV2::TPTP_Interpret.ind)
   307         SV1::TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind.
   308         (SV1 SV2 = bnd_sK1_Xy) =
   309         False
   310    \<Longrightarrow>
   311    \<forall>SV2::TPTP_Interpret.ind.
   312             (bnd_sK1_Xy = bnd_sK1_Xy) =
   313             False"
   314 ML_prf {*
   315 open TPTP_Syntax;
   316 open TPTP_Proof;
   317 
   318 val binds =
   319 [Bind ("SV1", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term_Func (TypeSymbol Type_Ind, []))))))], Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_Xy", [])))))]
   320 
   321 val tec = bind_tac @{context} (hd prob_names) binds
   322 *}
   323 (*
   324 apply (tactic {*strip_qtfrs
   325                 (* THEN tec *)*})
   326 *)
   327 apply (tactic {*tec*})
   328 done
   329 *)
   330 
   331 lemma "A | B \<Longrightarrow> C1 | A | C2 | B | C3"
   332 apply (erule disjE)
   333 apply (tactic \<open>clause_breaker 1\<close>)
   334 apply (tactic \<open>clause_breaker 1\<close>)
   335 done
   336 
   337 lemma "A \<Longrightarrow> A"
   338 apply (tactic \<open>clause_breaker 1\<close>)
   339 done
   340 
   341 typedecl NUM667_1_bnd_nat
   342 consts
   343   NUM667_1_bnd_less :: "NUM667_1_bnd_nat \<Rightarrow> NUM667_1_bnd_nat \<Rightarrow> bool"
   344   NUM667_1_bnd_x :: NUM667_1_bnd_nat
   345   NUM667_1_bnd_y :: NUM667_1_bnd_nat
   346 
   347 (*NUM667^1 node 302 -- dec*)
   348 lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
   349        ((((NUM667_1_bnd_less SV12 SV13 = NUM667_1_bnd_less SV11 SV10) = False \<or>
   350           (SV14 = SV13) = False) \<or>
   351          NUM667_1_bnd_less SV12 SV14 = False) \<or>
   352         NUM667_1_bnd_less SV9 SV10 = True) \<or>
   353        (SV9 = SV11) =
   354        False \<Longrightarrow>
   355        \<forall>SV9 SV14 SV10 SV13 SV11 SV12.
   356        (((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
   357           (SV14 = SV13) = False) \<or>
   358          NUM667_1_bnd_less SV12 SV14 = False) \<or>
   359         NUM667_1_bnd_less SV9 SV10 = True) \<or>
   360        (SV9 = SV11) =
   361        False"
   362 apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
   363 apply (tactic \<open>break_hypotheses 1\<close>)
   364 apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
   365 apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
   366 done
   367 
   368 ML \<open>
   369 extuni_dec_n @{context} 2;
   370 \<close>
   371 
   372 (*NUM667^1, node 202*)
   373 lemma "\<forall>SV9 SV10 SV11.
   374        ((((SV9 = SV11) = (NUM667_1_bnd_x = NUM667_1_bnd_y)) = False \<or>
   375          NUM667_1_bnd_less SV11 SV10 = False) \<or>
   376         NUM667_1_bnd_less SV9 SV10 = True) \<or>
   377        NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
   378        True \<Longrightarrow>
   379        \<forall>SV10 SV9 SV11.
   380        ((((SV11 = NUM667_1_bnd_x) = False \<or> (SV9 = NUM667_1_bnd_y) = False) \<or>
   381          NUM667_1_bnd_less SV11 SV10 = False) \<or>
   382         NUM667_1_bnd_less SV9 SV10 = True) \<or>
   383        NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
   384        True"
   385 apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
   386 apply (tactic \<open>break_hypotheses 1\<close>)
   387 apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
   388 apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
   389 done
   390 
   391 (*NUM667^1 node 141*)
   392 (*
   393 lemma "((bnd_x = bnd_x) = False \<or> (bnd_y = bnd_z) = False) \<or>
   394          bnd_less bnd_x bnd_y = True \<Longrightarrow>
   395          (bnd_y = bnd_z) = False \<or> bnd_less bnd_x bnd_y = True"
   396 apply (tactic {*strip_qtfrs*})
   397 apply (tactic {*break_hypotheses 1*})
   398 apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
   399 apply (erule extuni_triv)
   400 done
   401 *)
   402 
   403 ML \<open>
   404 fun full_extcnf_combined_tac ctxt =
   405   extcnf_combined_tac ctxt NONE
   406    [ConstsDiff,
   407     StripQuantifiers,
   408     Flip_Conclusion,
   409     Loop [
   410      Close_Branch,
   411      ConjI,
   412      King_Cong,
   413      Break_Hypotheses,
   414      Existential_Free,
   415      Existential_Var,
   416      Universal,
   417      RemoveRedundantQuantifications],
   418     CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates],
   419     AbsorbSkolemDefs]
   420    []
   421 \<close>
   422 
   423 ML \<open>
   424 fun nonfull_extcnf_combined_tac ctxt feats =
   425   extcnf_combined_tac ctxt NONE
   426    [ConstsDiff,
   427     StripQuantifiers,
   428     InnerLoopOnce (Break_Hypotheses :: feats),
   429     AbsorbSkolemDefs]
   430    []
   431 \<close>
   432 
   433 consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind
   434 lemma
   435   "\<forall>SV2. (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False \<Longrightarrow>
   436    (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False"
   437 (* apply (erule_tac x = "(@X. False)" in allE) *)
   438 (* apply (tactic {*remove_redundant_quantification 1*}) *)
   439 (* apply assumption *)
   440 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]\<close>)
   441 
   442 (*NUM667^1*)
   443 (*
   444      (* (Annotated_step ("153", "extuni_triv"), *)
   445 lemma "((bnd_y = bnd_x) = False \<or> (bnd_z = bnd_z) = False) \<or>
   446          (bnd_y = bnd_z) = True \<Longrightarrow>
   447          (bnd_y = bnd_x) = False \<or> (bnd_y = bnd_z) = True"
   448 apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
   449 done
   450      (* (Annotated_step ("162", "extuni_triv"), *)
   451 lemma "((bnd_y = bnd_x) = False \<or> (bnd_z = bnd_z) = False) \<or>
   452          bnd_less bnd_y bnd_z = True \<Longrightarrow>
   453          (bnd_y = bnd_x) = False \<or> bnd_less bnd_y bnd_z = True"
   454 apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*})
   455 done
   456 *)
   457 
   458 (* SEU602^2 *)
   459 consts
   460   SEU602_2_bnd_sK7_E :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
   461   SEU602_2_bnd_sK2_SY17 :: TPTP_Interpret.ind
   462   SEU602_2_bnd_in :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
   463 
   464      (* (Annotated_step ("113", "extuni_func"), *)
   465 lemma "\<forall>SV49::TPTP_Interpret.ind \<Rightarrow> bool.
   466             (SV49 =
   467              (\<lambda>SY23::TPTP_Interpret.ind.
   468                  \<not> SEU602_2_bnd_in SY23 SEU602_2_bnd_sK2_SY17)) =
   469             False \<Longrightarrow>
   470          \<forall>SV49::TPTP_Interpret.ind \<Rightarrow> bool.
   471             (SV49 (SEU602_2_bnd_sK7_E SV49) =
   472              (\<not> SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
   473             False"
   474 (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
   475 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]\<close>)
   476 
   477 consts
   478   SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
   479   SEV405_5_bnd_cA :: bool
   480 
   481 lemma "\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
   482             (\<forall>SY2::TPTP_Interpret.ind.
   483                 \<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
   484                    \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
   485             False \<Longrightarrow>
   486          \<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
   487             (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
   488                 \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
   489             False"
   490 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
   491 (*
   492 strip quantifiers -- creating a space of permutations; from shallowest to deepest (iterative deepening)
   493 flip the conclusion -- giving us branch
   494 apply some collection of rules, in some order, until the space has been explored completely. advantage of not having extcnf_combined: search space is shallow -- particularly if the collection of rules is small.
   495 *)
   496 
   497 consts
   498   SEU581_2_bnd_sK1 :: "TPTP_Interpret.ind"
   499   SEU581_2_bnd_sK2 :: "TPTP_Interpret.ind \<Rightarrow> bool"
   500   SEU581_2_bnd_subset :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> HOL.bool"
   501   SEU581_2_bnd_dsetconstr ::  "TPTP_Interpret.ind \<Rightarrow> (TPTP_Interpret.ind \<Rightarrow> HOL.bool) \<Rightarrow> TPTP_Interpret.ind"
   502 
   503 (*testing parameters*)
   504 lemma "! X :: TPTP_Interpret.ind . (\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
   505 \<Longrightarrow> ! X :: TPTP_Interpret.ind . (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
   506 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   507 
   508 lemma "(A & B) = True ==> (A | B) = True"
   509 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   510 
   511 lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
   512 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   513 
   514 (*testing goals with parameters*)
   515 lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> ! X. (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
   516 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   517 
   518 lemma "(A & B) = True ==> (B & A) = True"
   519 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   520 
   521 (*appreciating differences between THEN, REPEAT, and APPEND*)
   522 lemma "A & B ==> B & A"
   523 apply (tactic \<open>
   524   TRY (etac @{thm conjE} 1)
   525   THEN TRY (rtac @{thm conjI} 1)\<close>)
   526 by assumption+
   527 
   528 lemma "A & B ==> B & A"
   529 by (tactic \<open>
   530   etac @{thm conjE} 1
   531   THEN rtac @{thm conjI} 1
   532   THEN REPEAT (atac 1)\<close>)
   533 
   534 lemma "A & B ==> B & A"
   535 apply (tactic \<open>
   536   rtac @{thm conjI} 1
   537   APPEND etac @{thm conjE} 1\<close>)+
   538 back
   539 by assumption+
   540 
   541 consts
   542   SEU581_2_bnd_sK3 :: "TPTP_Interpret.ind"
   543   SEU581_2_bnd_sK4 :: "TPTP_Interpret.ind"
   544   SEU581_2_bnd_sK5 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
   545   SEU581_2_bnd_powerset :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
   546   SEU581_2_bnd_in :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
   547 
   548 consts
   549   bnd_c1 :: TPTP_Interpret.ind
   550   bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
   551 
   552 lemma "(\<forall>SX0. (\<not> (\<not> SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \<or>
   553               \<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
   554                     (PUZ114_5_bnd_sK5 SX0) \<or>
   555                  \<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
   556                     (bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
   557            \<not> SX0 bnd_c1 bnd_c1) \<or>
   558           SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
   559    True ==> \<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
   560               \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
   561                     (PUZ114_5_bnd_sK5 SV1) \<or>
   562                  \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
   563                     (bnd_s (PUZ114_5_bnd_sK5 SV1)))) \<or>
   564            \<not> SV1 bnd_c1 bnd_c1) \<or>
   565           SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
   566          True"
   567 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   568 
   569 lemma "(\<not> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = True \<Longrightarrow> (SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = False"
   570 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   571 
   572 (*testing repeated application of simulator*)
   573 lemma "(\<not> \<not> False) = True \<Longrightarrow>
   574     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
   575     False = True \<or> False = True \<or> False = True"
   576 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   577 
   578 (*Testing non-normal conclusion. Ideally we should be able to apply
   579   the tactic to arbitrary chains of extcnf steps -- where it's not
   580   generally the case that the conclusions are normal.*)
   581 lemma "(\<not> \<not> False) = True \<Longrightarrow>
   582     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
   583     (\<not> False) = False"
   584 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   585 
   586 (*testing repeated application of simulator, involving different extcnf rules*)
   587 lemma "(\<not> \<not> (False | False)) = True \<Longrightarrow>
   588     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
   589     False = True \<or> False = True \<or> False = True"
   590 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   591 
   592 (*testing logical expansion*)
   593 lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
   594 \<Longrightarrow> (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
   595 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   596 
   597 (*testing extcnf_forall_pos*)
   598 lemma "(\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True \<Longrightarrow> \<forall>SV1. (\<forall>SY14.
   599              SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14)
   600               (SEU581_2_bnd_powerset SV1)) = True"
   601 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   602 
   603 lemma "((\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True) | ((~ False) = False) \<Longrightarrow>
   604 \<forall>SV1. ((\<forall>SY14. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True) | ((~ False) = False)"
   605 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   606 
   607 (*testing parameters*)
   608 lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
   609 \<Longrightarrow> ! X. (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
   610 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   611 
   612 lemma "((? A .P1 A) = False) | P2 = True \<Longrightarrow> !X. ((P1 X) = False | P2 = True)"
   613 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   614 
   615 lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) \<Longrightarrow> !X. (P1a X = True | P1b X = True | P2 = True)"
   616 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   617 
   618 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
   619 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   620 
   621 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
   622 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   623 
   624 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
   625 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   626 
   627 consts dud_bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
   628 
   629 (*this lemma kills blast*)
   630 lemma "(\<not> (\<forall>SX0 SX1.
   631           \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or> PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SX0)) SX1) \<or>
   632     \<not> (\<forall>SX0 SX1.
   633           \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
   634           PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
   635    False \<Longrightarrow> (\<not> (\<forall>SX0 SX1.
   636           \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
   637           PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
   638    False"
   639 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   640 
   641 (*testing logical expansion -- this should be done by blast*)
   642 lemma "(\<forall>A B. bnd_in B (bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
   643 \<Longrightarrow> (\<forall>A B. \<not> bnd_in B (bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
   644 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   645 
   646 (*testing related to PUZ114^5.p.out*)
   647 lemma "\<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
   648                     \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
   649                           (PUZ114_5_bnd_sK5 SV1) \<or>
   650                        \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
   651                           (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
   652                 True \<or>
   653                 (\<not> SV1 bnd_c1 bnd_c1) = True) \<or>
   654                SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True \<Longrightarrow>
   655          \<forall>SV1. (SV1 bnd_c1 bnd_c1 = False \<or>
   656                 (\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
   657                     \<not> (\<not> SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1)))
   658                           (PUZ114_5_bnd_sK5 SV1) \<or>
   659                        \<not> SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1))
   660                           (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
   661                 True) \<or>
   662                SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True"
   663 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   664 
   665 lemma "\<forall>SV2. (\<forall>SY41.
   666                    \<not> PUZ114_5_bnd_sK3 SV2 SY41 \<or>
   667                    PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SY41) =
   668                True \<Longrightarrow>
   669          \<forall>SV4 SV2.
   670             (\<not> PUZ114_5_bnd_sK3 SV2 SV4 \<or>
   671              PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) =
   672             True"
   673 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   674 
   675 lemma "\<forall>SV3. (\<forall>SY42.
   676                    \<not> PUZ114_5_bnd_sK3 SV3 SY42 \<or>
   677                    PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SY42)) =
   678                True \<Longrightarrow>
   679          \<forall>SV5 SV3.
   680             (\<not> PUZ114_5_bnd_sK3 SV3 SV5 \<or>
   681              PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) =
   682             True"
   683 by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
   684 
   685 
   686 subsection "unfold_def"
   687      (* (Annotated_step ("9", "unfold_def"), *)
   688 lemma "bnd_kpairiskpair =
   689              (ALL Xx Xy.
   690                  bnd_iskpair
   691                   (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   692                     (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
   693                       bnd_emptyset))) &
   694              bnd_kpair =
   695              (%Xx Xy.
   696                  bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   697                   (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
   698                     bnd_emptyset)) &
   699              bnd_iskpair =
   700              (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
   701                          (EX Xy. bnd_in Xy (bnd_setunion A) &
   702                                  A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   703                                       (bnd_setadjoin
   704                                         (bnd_setadjoin Xx
   705 (bnd_setadjoin Xy bnd_emptyset))
   706                                         bnd_emptyset))) &
   707              (~ (ALL SY0 SY1.
   708                     EX SY3.
   709                        bnd_in SY3
   710                         (bnd_setunion
   711                           (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
   712                             (bnd_setadjoin
   713                               (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
   714                               bnd_emptyset))) &
   715                        (EX SY4.
   716                            bnd_in SY4
   717                             (bnd_setunion
   718                               (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
   719                                 (bnd_setadjoin
   720                                   (bnd_setadjoin SY0
   721                                     (bnd_setadjoin SY1 bnd_emptyset))
   722                                   bnd_emptyset))) &
   723                            bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
   724                             (bnd_setadjoin
   725                               (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
   726                               bnd_emptyset) =
   727                            bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset)
   728                             (bnd_setadjoin
   729                               (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
   730                               bnd_emptyset)))) =
   731              True
   732              ==> (~ (ALL SX0 SX1.
   733                         ~ (ALL SX2.
   734                               ~ ~ (~ bnd_in SX2
   735                                       (bnd_setunion
   736                                         (bnd_setadjoin
   737 (bnd_setadjoin SX0 bnd_emptyset)
   738 (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) |
   739                                    ~ ~ (ALL SX3.
   740  ~ ~ (~ bnd_in SX3
   741          (bnd_setunion
   742            (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
   743              (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
   744                bnd_emptyset))) |
   745       bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
   746        (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
   747          bnd_emptyset) ~=
   748       bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
   749        (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
   750          bnd_emptyset))))))) =
   751                  True"
   752 by (tactic \<open>unfold_def_tac @{context} []\<close>)
   753 
   754      (* (Annotated_step ("10", "unfold_def"), *)
   755 lemma "bnd_kpairiskpair =
   756              (ALL Xx Xy.
   757                  bnd_iskpair
   758                   (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   759                     (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
   760                       bnd_emptyset))) &
   761              bnd_kpair =
   762              (%Xx Xy.
   763                  bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   764                   (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset))
   765                     bnd_emptyset)) &
   766              bnd_iskpair =
   767              (%A. EX Xx. bnd_in Xx (bnd_setunion A) &
   768                          (EX Xy. bnd_in Xy (bnd_setunion A) &
   769                                  A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
   770                                       (bnd_setadjoin
   771                                         (bnd_setadjoin Xx
   772 (bnd_setadjoin Xy bnd_emptyset))
   773                                         bnd_emptyset))) &
   774              (ALL SY5 SY6.
   775                  EX SY7.
   776                     bnd_in SY7
   777                      (bnd_setunion
   778                        (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
   779                          (bnd_setadjoin
   780                            (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
   781                            bnd_emptyset))) &
   782                     (EX SY8.
   783                         bnd_in SY8
   784                          (bnd_setunion
   785                            (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
   786                              (bnd_setadjoin
   787                                (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
   788                                bnd_emptyset))) &
   789                         bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
   790                          (bnd_setadjoin
   791                            (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
   792                            bnd_emptyset) =
   793                         bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset)
   794                          (bnd_setadjoin
   795                            (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset))
   796                            bnd_emptyset))) =
   797              True
   798              ==> (ALL SX0 SX1.
   799                      ~ (ALL SX2.
   800                            ~ ~ (~ bnd_in SX2
   801                                    (bnd_setunion
   802                                      (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
   803                                        (bnd_setadjoin
   804                                          (bnd_setadjoin SX0
   805  (bnd_setadjoin SX1 bnd_emptyset))
   806                                          bnd_emptyset))) |
   807                                 ~ ~ (ALL SX3.
   808                                         ~ ~ (~ bnd_in SX3
   809       (bnd_setunion
   810         (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
   811           (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
   812             bnd_emptyset))) |
   813    bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset)
   814     (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset))
   815       bnd_emptyset) ~=
   816    bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset)
   817     (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
   818       bnd_emptyset)))))) =
   819                  True"
   820 by (tactic \<open>unfold_def_tac @{context} []\<close>)
   821 
   822      (* (Annotated_step ("12", "unfold_def"), *)
   823 lemma "bnd_cCKB6_BLACK =
   824          (\<lambda>Xu Xv.
   825              \<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
   826                   (\<forall>Xj Xk.
   827                       Xw Xj Xk \<longrightarrow>
   828                       Xw (bnd_s (bnd_s Xj)) Xk \<and>
   829                       Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
   830                   Xw Xu Xv) \<and>
   831          ((((\<forall>SY36 SY37.
   832                 \<not> PUZ114_5_bnd_sK3 SY36 SY37 \<or>
   833                 PUZ114_5_bnd_sK3 (bnd_s (bnd_s SY36)) SY37) \<and>
   834             (\<forall>SY38 SY39.
   835                 \<not> PUZ114_5_bnd_sK3 SY38 SY39 \<or>
   836                 PUZ114_5_bnd_sK3 (bnd_s SY38) (bnd_s SY39))) \<and>
   837            PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<and>
   838           \<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
   839              (bnd_s PUZ114_5_bnd_sK2)) =
   840          True \<Longrightarrow>
   841          (\<not> (\<not> \<not> (\<not> \<not> (\<not> (\<forall>SX0 SX1.
   842                              \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
   843                              PUZ114_5_bnd_sK3 (bnd_s (bnd_s SX0)) SX1) \<or>
   844                        \<not> (\<forall>SX0 SX1.
   845                              \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
   846                              PUZ114_5_bnd_sK3 (bnd_s SX0) (bnd_s SX1))) \<or>
   847                   \<not> PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) \<or>
   848              \<not> \<not> PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1)))
   849                   (bnd_s PUZ114_5_bnd_sK2))) =
   850          True"
   851 (*
   852 apply (erule conjE)+
   853 apply (erule subst)+
   854 apply (tactic {*log_expander 1*})+
   855 apply (rule refl)
   856 *)
   857 by (tactic \<open>unfold_def_tac @{context} []\<close>)
   858 
   859      (* (Annotated_step ("13", "unfold_def"), *)
   860 lemma "bnd_cCKB6_BLACK =
   861          (\<lambda>Xu Xv.
   862              \<forall>Xw. Xw bnd_c1 bnd_c1 \<and>
   863                   (\<forall>Xj Xk.
   864                       Xw Xj Xk \<longrightarrow>
   865                       Xw (bnd_s (bnd_s Xj)) Xk \<and>
   866                       Xw (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
   867                   Xw Xu Xv) \<and>
   868          (\<forall>SY30.
   869              (SY30 (PUZ114_5_bnd_sK4 SY30) (PUZ114_5_bnd_sK5 SY30) \<and>
   870               (\<not> SY30 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SY30)))
   871                   (PUZ114_5_bnd_sK5 SY30) \<or>
   872                \<not> SY30 (bnd_s (PUZ114_5_bnd_sK4 SY30))
   873                   (bnd_s (PUZ114_5_bnd_sK5 SY30))) \<or>
   874               \<not> SY30 bnd_c1 bnd_c1) \<or>
   875              SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
   876          True \<Longrightarrow>
   877          (\<forall>SX0. (\<not> (\<not> SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) \<or>
   878                     \<not> (\<not> SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0)))
   879                           (PUZ114_5_bnd_sK5 SX0) \<or>
   880                        \<not> SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0))
   881                           (bnd_s (PUZ114_5_bnd_sK5 SX0)))) \<or>
   882                  \<not> SX0 bnd_c1 bnd_c1) \<or>
   883                 SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
   884          True"
   885 (*
   886 apply (erule conjE)+
   887 apply (tactic {*expander_animal 1*})+
   888 apply assumption
   889 *)
   890 by (tactic \<open>unfold_def_tac @{context} []\<close>)
   891 
   892 (*FIXME move this heuristic elsewhere*)
   893 ML \<open>
   894 (*Other than the list (which must not be empty) this function
   895   expects a parameter indicating the smallest integer.
   896   (Using Int.minInt isn't always viable).*)
   897 fun max_int_floored min l =
   898   if null l then raise List.Empty
   899   else fold (curry Int.max) l min;
   900 
   901 val _ = @{assert} (max_int_floored ~101002 [1]  = 1)
   902 val _ = @{assert} (max_int_floored 0 [1, 3, 5] = 5)
   903 
   904 fun max_index_floored min l =
   905   let
   906     val max = max_int_floored min l
   907   in find_index (pair max #> op =) l end
   908 \<close>
   909 
   910 ML \<open>
   911 max_index_floored 0 [1, 3, 5]
   912 \<close>
   913 
   914 ML \<open>
   915 (*
   916 Given argument ([h_1, ..., h_n], conc),
   917 obtained from term of form
   918   h_1 ==> ... ==> h_n ==> conclusion,
   919 this function indicates which h_i is biggest,
   920 or NONE if h_n = 0.
   921 *)
   922 fun biggest_hypothesis (hypos, _) =
   923   if null hypos then NONE
   924   else
   925     map size_of_term hypos
   926     |> max_index_floored 0
   927     |> SOME
   928 \<close>
   929 
   930 ML \<open>
   931 fun biggest_hyp_first_tac i = fn st =>
   932   let
   933     val results = TERMFUN biggest_hypothesis (SOME i) st
   934 val _ = tracing ("result=" ^ @{make_string} results)
   935   in
   936     if null results then no_tac st
   937     else
   938       let
   939         val result = the_single results
   940       in
   941         case result of
   942             NONE => no_tac st
   943           | SOME n =>
   944               if n > 0 then rotate_tac n i st else no_tac st
   945       end
   946   end
   947 \<close>
   948 
   949      (* (Annotated_step ("6", "unfold_def"), *)
   950 lemma  "(\<not> (\<exists>U :: TPTP_Interpret.ind \<Rightarrow> bool. \<forall>V. U V = SEV405_5_bnd_cA)) = True \<Longrightarrow>
   951          (\<not> \<not> (\<forall>SX0 :: TPTP_Interpret.ind \<Rightarrow> bool. \<not> (\<forall>SX1. \<not> (\<not> (\<not> SX0 SX1 \<or> SEV405_5_bnd_cA) \<or>
   952  \<not> (\<not> SEV405_5_bnd_cA \<or> SX0 SX1))))) =
   953          True"
   954 (* by (tactic {*unfold_def_tac []*}) *)
   955 oops
   956 
   957 subsection "Using leo2_tac"
   958 (*these require PUZ114^5's proof to be loaded
   959 
   960 ML {*leo2_tac @{context} (hd prob_names) "50"*}
   961 
   962 ML {*leo2_tac @{context} (hd prob_names) "4"*}
   963 
   964 ML {*leo2_tac @{context} (hd prob_names) "9"*}
   965 
   966      (* (Annotated_step ("9", "extcnf_combined"), *)
   967 lemma "(\<forall>SY30.
   968              SY30 bnd_c1 bnd_c1 \<and>
   969              (\<forall>Xj Xk.
   970                  SY30 Xj Xk \<longrightarrow>
   971                  SY30 (bnd_s (bnd_s Xj)) Xk \<and>
   972                  SY30 (bnd_s Xj) (bnd_s Xk)) \<longrightarrow>
   973              SY30 bnd_sK1 bnd_sK2) =
   974          True \<Longrightarrow>
   975          (\<forall>SY30.
   976              (SY30 (bnd_sK4 SY30) (bnd_sK5 SY30) \<and>
   977               (\<not> SY30 (bnd_s (bnd_s (bnd_sK4 SY30)))
   978                   (bnd_sK5 SY30) \<or>
   979                \<not> SY30 (bnd_s (bnd_sK4 SY30))
   980                   (bnd_s (bnd_sK5 SY30))) \<or>
   981               \<not> SY30 bnd_c1 bnd_c1) \<or>
   982              SY30 bnd_sK1 bnd_sK2) =
   983          True"
   984 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
   985 *)
   986 
   987 
   988 
   989 typedecl GEG007_1_bnd_reg
   990 consts
   991   GEG007_1_bnd_sK7_SX2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> GEG007_1_bnd_reg"
   992   GEG007_1_bnd_sK6_SX2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> GEG007_1_bnd_reg"
   993   GEG007_1_bnd_a :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
   994   GEG007_1_bnd_catalunya  :: "GEG007_1_bnd_reg"
   995   GEG007_1_bnd_spain :: "GEG007_1_bnd_reg"
   996   GEG007_1_bnd_c :: "GEG007_1_bnd_reg \<Rightarrow> GEG007_1_bnd_reg \<Rightarrow> bool"
   997 
   998      (* (Annotated_step ("147", "extcnf_forall_neg"), *)
   999 lemma "\<forall>SV13 SV6.
  1000             (\<forall>SX2. \<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
  1001                    GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya) =
  1002             False \<or>
  1003             GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
  1004          \<forall>SV6 SV13.
  1005             (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_spain \<or>
  1006              GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) =
  1007             False \<or>
  1008             GEG007_1_bnd_a SV6 SV13 = False"
  1009 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
  1010 
  1011      (* (Annotated_step ("116", "extcnf_forall_neg"), *)
  1012 lemma "\<forall>SV13 SV6.
  1013             (\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya \<or>
  1014                              \<not> \<not> \<not> (\<forall>SX3.
  1015        \<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
  1016             \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
  1017                      GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
  1018                         \<not> \<not> (\<not> GEG007_1_bnd_c SX2 GEG007_1_bnd_spain \<or>
  1019                              \<not> \<not> \<not> (\<forall>SX3.
  1020        \<not> \<not> (\<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or> GEG007_1_bnd_c SX4 SX2) \<or>
  1021             \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SX3 \<or>
  1022                      GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
  1023             False \<or>
  1024             GEG007_1_bnd_a SV6 SV13 = False \<Longrightarrow>
  1025          \<forall>SV6 SV13.
  1026             (\<not> \<not> (\<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
  1027                           GEG007_1_bnd_catalunya \<or>
  1028                        \<not> \<not> \<not> (\<forall>SY68.
  1029  \<not> \<not> (\<not> (\<forall>SY69.
  1030             \<not> GEG007_1_bnd_c SY69 SY68 \<or>
  1031             GEG007_1_bnd_c SY69 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
  1032       \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY68 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) \<or>
  1033                   \<not> \<not> (\<not> GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6)
  1034                           GEG007_1_bnd_spain \<or>
  1035                        \<not> \<not> \<not> (\<forall>SY71.
  1036  \<not> \<not> (\<not> (\<forall>SY72.
  1037             \<not> GEG007_1_bnd_c SY72 SY71 \<or>
  1038             GEG007_1_bnd_c SY72 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) \<or>
  1039       \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY71 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
  1040             False \<or>
  1041             GEG007_1_bnd_a SV6 SV13 = False"
  1042 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
  1043 
  1044 consts PUZ107_5_bnd_sK1_SX0 ::
  1045   "TPTP_Interpret.ind
  1046       \<Rightarrow> TPTP_Interpret.ind
  1047         \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1048 
  1049 lemma "\<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
  1050    (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
  1051    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
  1052    ((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
  1053    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
  1054 \<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
  1055    (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
  1056    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
  1057    ((SV1 = SV3) = True \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
  1058    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
  1059 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Not_neg]\<close>)
  1060 
  1061 lemma "
  1062 \<forall>(SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind)
  1063    (SV4::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
  1064    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
  1065    ((SV1 \<noteq> SV3 \<or> SV2 \<noteq> SV4) = False \<or>
  1066     PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
  1067    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False \<Longrightarrow>
  1068 \<forall>(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind)
  1069    (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind)
  1070    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
  1071    ((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
  1072    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
  1073 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Or_neg]\<close>)
  1074 
  1075 consts
  1076   NUM016_5_bnd_a :: TPTP_Interpret.ind
  1077   NUM016_5_bnd_prime :: "TPTP_Interpret.ind \<Rightarrow> bool"
  1078   NUM016_5_bnd_factorial_plus_one :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
  1079   NUM016_5_bnd_prime_divisor :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
  1080   NUM016_5_bnd_divides :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1081   NUM016_5_bnd_less :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1082 
  1083      (* (Annotated_step ("6", "unfold_def"), *)
  1084 lemma "((((((((((((\<forall>X::TPTP_Interpret.ind. \<not> NUM016_5_bnd_less X X) \<and>
  1085                     (\<forall>(X::TPTP_Interpret.ind)
  1086                         Y::TPTP_Interpret.ind.
  1087                         \<not> NUM016_5_bnd_less X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
  1088                    (\<forall>X::TPTP_Interpret.ind. NUM016_5_bnd_divides X X)) \<and>
  1089                   (\<forall>(X::TPTP_Interpret.ind)
  1090                       (Y::TPTP_Interpret.ind)
  1091                       Z::TPTP_Interpret.ind.
  1092                       (\<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_divides Y Z) \<or>
  1093                       NUM016_5_bnd_divides X Z)) \<and>
  1094                  (\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
  1095                      \<not> NUM016_5_bnd_divides X Y \<or> \<not> NUM016_5_bnd_less Y X)) \<and>
  1096                 (\<forall>X::TPTP_Interpret.ind.
  1097                     NUM016_5_bnd_less X (NUM016_5_bnd_factorial_plus_one X))) \<and>
  1098                (\<forall>(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind.
  1099                    \<not> NUM016_5_bnd_divides X (NUM016_5_bnd_factorial_plus_one Y) \<or>
  1100                    NUM016_5_bnd_less Y X)) \<and>
  1101               (\<forall>X::TPTP_Interpret.ind.
  1102                   NUM016_5_bnd_prime X \<or>
  1103                   NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor X) X)) \<and>
  1104              (\<forall>X::TPTP_Interpret.ind.
  1105                  NUM016_5_bnd_prime X \<or>
  1106                  NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor X))) \<and>
  1107             (\<forall>X::TPTP_Interpret.ind.
  1108                 NUM016_5_bnd_prime X \<or>
  1109                 NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor X) X)) \<and>
  1110            NUM016_5_bnd_prime NUM016_5_bnd_a) \<and>
  1111           (\<forall>X::TPTP_Interpret.ind.
  1112               (\<not> NUM016_5_bnd_prime X \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a X) \<or>
  1113               NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) X)) =
  1114          True \<Longrightarrow>
  1115          (\<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> \<not> (\<not> (\<forall>SX0::TPTP_Interpret.ind.
  1116      \<not> NUM016_5_bnd_less SX0 SX0) \<or>
  1117                                \<not> (\<forall>(SX0::TPTP_Interpret.ind)
  1118      SX1::TPTP_Interpret.ind.
  1119      \<not> NUM016_5_bnd_less SX0 SX1 \<or> \<not> NUM016_5_bnd_less SX1 SX0)) \<or>
  1120                           \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1121 NUM016_5_bnd_divides SX0 SX0)) \<or>
  1122                      \<not> (\<forall>(SX0::TPTP_Interpret.ind)
  1123                            (SX1::TPTP_Interpret.ind)
  1124                            SX2::TPTP_Interpret.ind.
  1125                            (\<not> NUM016_5_bnd_divides SX0 SX1 \<or>
  1126                             \<not> NUM016_5_bnd_divides SX1 SX2) \<or>
  1127                            NUM016_5_bnd_divides SX0 SX2)) \<or>
  1128                 \<not> (\<forall>(SX0::TPTP_Interpret.ind)
  1129                       SX1::TPTP_Interpret.ind.
  1130                       \<not> NUM016_5_bnd_divides SX0 SX1 \<or>
  1131                       \<not> NUM016_5_bnd_less SX1 SX0)) \<or>
  1132            \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1133                  NUM016_5_bnd_less SX0 (NUM016_5_bnd_factorial_plus_one SX0))) \<or>
  1134       \<not> (\<forall>(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind.
  1135             \<not> NUM016_5_bnd_divides SX0 (NUM016_5_bnd_factorial_plus_one SX1) \<or>
  1136             NUM016_5_bnd_less SX1 SX0)) \<or>
  1137  \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1138        NUM016_5_bnd_prime SX0 \<or>
  1139        NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor SX0) SX0)) \<or>
  1140                             \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1141   NUM016_5_bnd_prime SX0 \<or> NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor SX0))) \<or>
  1142                        \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1143                              NUM016_5_bnd_prime SX0 \<or>
  1144                              NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor SX0)
  1145                               SX0)) \<or>
  1146                   \<not> NUM016_5_bnd_prime NUM016_5_bnd_a) \<or>
  1147              \<not> (\<forall>SX0::TPTP_Interpret.ind.
  1148                    (\<not> NUM016_5_bnd_prime SX0 \<or> \<not> NUM016_5_bnd_less NUM016_5_bnd_a SX0) \<or>
  1149                    NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a)
  1150                     SX0))) =
  1151          True"
  1152 by (tactic \<open>unfold_def_tac @{context} []\<close>)
  1153 
  1154      (* (Annotated_step ("3", "unfold_def"), *)
  1155 lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) &
  1156                            (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
  1157                           (ALL X. bnd_divides X X)) &
  1158                          (ALL X Y Z.
  1159                              (~ bnd_divides X Y | ~ bnd_divides Y Z) |
  1160                              bnd_divides X Z)) &
  1161                         (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
  1162                        (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
  1163                       (ALL X Y.
  1164                           ~ bnd_divides X (bnd_factorial_plus_one Y) |
  1165                           bnd_less Y X)) &
  1166                      (ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) &
  1167                     (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
  1168                    (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
  1169                   bnd_prime bnd_a) &
  1170                  (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
  1171                          bnd_less (bnd_factorial_plus_one bnd_a) X))) =
  1172              False
  1173              ==> (~ ((((((((((((ALL X. ~ bnd_less X X) &
  1174                                (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) &
  1175                               (ALL X. bnd_divides X X)) &
  1176                              (ALL X Y Z.
  1177                                  (~ bnd_divides X Y | ~ bnd_divides Y Z) |
  1178                                  bnd_divides X Z)) &
  1179                             (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) &
  1180                            (ALL X. bnd_less X (bnd_factorial_plus_one X))) &
  1181                           (ALL X Y.
  1182                               ~ bnd_divides X (bnd_factorial_plus_one Y) |
  1183                               bnd_less Y X)) &
  1184                          (ALL X. bnd_prime X |
  1185                                  bnd_divides (bnd_prime_divisor X) X)) &
  1186                         (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) &
  1187                        (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) &
  1188                       bnd_prime bnd_a) &
  1189                      (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
  1190                              bnd_less (bnd_factorial_plus_one bnd_a) X))) =
  1191                  False"
  1192 by (tactic \<open>unfold_def_tac @{context} []\<close>)
  1193 
  1194 (* SET062^6.p.out
  1195       [[(Annotated_step ("3", "unfold_def"), *)
  1196 lemma "(\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False \<Longrightarrow>
  1197          (\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False"
  1198 by (tactic \<open>unfold_def_tac @{context} []\<close>)
  1199 
  1200 (*
  1201 (* SEU559^2.p.out *)
  1202    (* [[(Annotated_step ("3", "unfold_def"), *)
  1203 lemma "bnd_subset = (\<lambda>A B. \<forall>Xx. bnd_in Xx A \<longrightarrow> bnd_in Xx B) \<and>
  1204          (\<forall>A B. (\<forall>Xx. bnd_in Xx A \<longrightarrow> bnd_in Xx B) \<longrightarrow>
  1205                 bnd_subset A B) =
  1206          False \<Longrightarrow>
  1207          (\<forall>SY0 SY1.
  1208              (\<forall>Xx. bnd_in Xx SY0 \<longrightarrow> bnd_in Xx SY1) \<longrightarrow>
  1209              (\<forall>SY5. bnd_in SY5 SY0 \<longrightarrow> bnd_in SY5 SY1)) =
  1210          False"
  1211 by (tactic {*unfold_def_tac [@{thm bnd_subset_def}]*})
  1212 
  1213 (* SEU559^2.p.out
  1214     [[(Annotated_step ("6", "unfold_def"), *)
  1215 lemma "(\<not> (\<exists>Xx. \<forall>Xy. Xx \<longrightarrow> Xy)) = True \<Longrightarrow>
  1216          (\<not> \<not> (\<forall>SX0. \<not> (\<forall>SX1. \<not> SX0 \<or> SX1))) = True"
  1217 by (tactic {*unfold_def_tac []*})
  1218 
  1219 (* SEU502^2.p.out
  1220     [[(Annotated_step ("3", "unfold_def"), *)
  1221 lemma "bnd_emptysetE =
  1222          (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<and>
  1223          (bnd_emptysetE \<longrightarrow>
  1224           (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
  1225          False \<Longrightarrow>
  1226          ((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
  1227           (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> False)) =
  1228          False"
  1229 by (tactic {*unfold_def_tac [@{thm bnd_emptysetE_def}]*})
  1230 *)
  1231 
  1232 typedecl AGT037_2_bnd_mu
  1233 consts
  1234   AGT037_2_bnd_sK1_SX0 :: TPTP_Interpret.ind
  1235   AGT037_2_bnd_cola :: AGT037_2_bnd_mu
  1236   AGT037_2_bnd_jan :: AGT037_2_bnd_mu
  1237   AGT037_2_bnd_possibly_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1238   AGT037_2_bnd_sK5_SY68 ::
  1239     "TPTP_Interpret.ind
  1240      \<Rightarrow> AGT037_2_bnd_mu
  1241        \<Rightarrow> AGT037_2_bnd_mu
  1242          \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
  1243   AGT037_2_bnd_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1244   AGT037_2_bnd_very_much_likes :: "AGT037_2_bnd_mu \<Rightarrow> AGT037_2_bnd_mu \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1245   AGT037_2_bnd_a1 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1246   AGT037_2_bnd_a2 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1247   AGT037_2_bnd_a3 :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind \<Rightarrow> bool"
  1248 
  1249 (*test that nullary skolem terms are OK*)
  1250      (* (Annotated_step ("79", "extcnf_forall_neg"), *)
  1251 lemma "(\<forall>SX0::TPTP_Interpret.ind.
  1252              AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola SX0) =
  1253          False \<Longrightarrow>
  1254          AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_SX0 =
  1255          False"
  1256 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
  1257 
  1258      (* (Annotated_step ("202", "extcnf_forall_neg"), *)
  1259 lemma "\<forall>(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu)
  1260             SV45::TPTP_Interpret.ind.
  1261             ((((\<forall>SY68::TPTP_Interpret.ind.
  1262                    \<not> AGT037_2_bnd_a1 SV45 SY68 \<or>
  1263                    AGT037_2_bnd_likes SV29 SV39 SY68) =
  1264                False \<or>
  1265                (\<not> (\<forall>SY69::TPTP_Interpret.ind.
  1266                       \<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
  1267                       AGT037_2_bnd_likes SV29 SV39 SY69)) =
  1268                True) \<or>
  1269               AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
  1270              AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
  1271             AGT037_2_bnd_a3 SV13 SV45 = False \<Longrightarrow>
  1272          \<forall>(SV29::AGT037_2_bnd_mu) (SV39::AGT037_2_bnd_mu) (SV13::TPTP_Interpret.ind)
  1273             SV45::TPTP_Interpret.ind.
  1274             ((((\<not> AGT037_2_bnd_a1 SV45
  1275                    (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45) \<or>
  1276                 AGT037_2_bnd_likes SV29 SV39
  1277                  (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45)) =
  1278                False \<or>
  1279                (\<not> (\<forall>SY69::TPTP_Interpret.ind.
  1280                       \<not> AGT037_2_bnd_a2 SV45 SY69 \<or>
  1281                       AGT037_2_bnd_likes SV29 SV39 SY69)) =
  1282                True) \<or>
  1283               AGT037_2_bnd_likes SV29 SV39 SV45 = False) \<or>
  1284              AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) \<or>
  1285             AGT037_2_bnd_a3 SV13 SV45 = False"
  1286 (*
  1287 apply (rule allI)+
  1288 apply (erule_tac x = "SV13" in allE)
  1289 apply (erule_tac x = "SV39" in allE)
  1290 apply (erule_tac x = "SV29" in allE)
  1291 apply (erule_tac x = "SV45" in allE)
  1292 apply (erule disjE)+
  1293 defer
  1294 apply (tactic {*clause_breaker 1*})+
  1295 apply (drule_tac sk = "bnd_sK5_SY68 SV13 SV39 SV29 SV45" in leo2_skolemise)
  1296 defer
  1297 apply (tactic {*clause_breaker 1*})
  1298 apply (tactic {*nonfull_extcnf_combined_tac []*})
  1299 *)
  1300 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
  1301 
  1302 (*(*NUM667^1*)
  1303 lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
  1304    ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
  1305       (SV14 = SV13) = False) \<or>
  1306      bnd_less SV12 SV14 = False) \<or>
  1307     bnd_less SV9 SV10 = True) \<or>
  1308    (SV9 = SV11) = False \<Longrightarrow>
  1309 \<forall>SV9 SV14 SV10 SV11 SV13 SV12.
  1310    ((((bnd_less SV12 SV13 = False \<or>
  1311        bnd_less SV11 SV10 = False) \<or>
  1312       (SV14 = SV13) = False) \<or>
  1313      bnd_less SV12 SV14 = False) \<or>
  1314     bnd_less SV9 SV10 = True) \<or>
  1315    (SV9 = SV11) = False"
  1316 (*
  1317 apply (tactic {*
  1318   extcnf_combined_tac NONE
  1319    [ConstsDiff,
  1320     StripQuantifiers]
  1321    []*})
  1322 *)
  1323 (*
  1324 apply (rule allI)+
  1325 apply (erule_tac x = "SV12" in allE)
  1326 apply (erule_tac x = "SV13" in allE)
  1327 apply (erule_tac x = "SV14" in allE)
  1328 apply (erule_tac x = "SV9" in allE)
  1329 apply (erule_tac x = "SV10" in allE)
  1330 apply (erule_tac x = "SV11" in allE)
  1331 *)
  1332 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "300") 1*})
  1333 
  1334 
  1335 (*NUM667^1 node 302 -- dec*)
  1336 lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
  1337        ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False \<or>
  1338           (SV14 = SV13) = False) \<or>
  1339          bnd_less SV12 SV14 = False) \<or>
  1340         bnd_less SV9 SV10 = True) \<or>
  1341        (SV9 = SV11) =
  1342        False \<Longrightarrow>
  1343        \<forall>SV9 SV14 SV10 SV13 SV11 SV12.
  1344        (((((SV12 = SV11) = False \<or> (SV13 = SV10) = False) \<or>
  1345           (SV14 = SV13) = False) \<or>
  1346          bnd_less SV12 SV14 = False) \<or>
  1347         bnd_less SV9 SV10 = True) \<or>
  1348        (SV9 = SV11) =
  1349        False"
  1350 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "302") 1*})
  1351 *)
  1352 
  1353 
  1354 (*
  1355 (*CSR122^2*)
  1356      (* (Annotated_step ("23", "extuni_bool2"), *)
  1357 lemma "(bnd_holdsDuring_THFTYPE_IiooI
  1358            (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1359            (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1360                   bnd_lBill_THFTYPE_i \<or>
  1361                \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1362                   bnd_lBill_THFTYPE_i)) =
  1363           bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1364            bnd_lBill_THFTYPE_i) =
  1365          False \<Longrightarrow>
  1366          bnd_holdsDuring_THFTYPE_IiooI
  1367           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1368           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1369                  bnd_lBill_THFTYPE_i \<or>
  1370               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1371                  bnd_lBill_THFTYPE_i)) =
  1372          True \<or>
  1373          bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1374           bnd_lBill_THFTYPE_i =
  1375          True"
  1376 (* apply (erule extuni_bool2) *)
  1377 (* done *)
  1378 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "23") 1*})
  1379 
  1380      (* (Annotated_step ("24", "extuni_bool1"), *)
  1381 lemma "(bnd_holdsDuring_THFTYPE_IiooI
  1382            (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1383            (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1384                   bnd_lBill_THFTYPE_i \<or>
  1385                \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1386                   bnd_lBill_THFTYPE_i)) =
  1387           bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1388            bnd_lBill_THFTYPE_i) =
  1389          False \<Longrightarrow>
  1390          bnd_holdsDuring_THFTYPE_IiooI
  1391           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1392           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1393                  bnd_lBill_THFTYPE_i \<or>
  1394               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1395                  bnd_lBill_THFTYPE_i)) =
  1396          False \<or>
  1397          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1398           bnd_lBill_THFTYPE_i =
  1399          False"
  1400 (* apply (erule extuni_bool1) *)
  1401 (* done *)
  1402 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "24") 1*})
  1403 
  1404      (* (Annotated_step ("25", "extuni_bool2"), *)
  1405 lemma "(bnd_holdsDuring_THFTYPE_IiooI
  1406            (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1407            (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1408                   bnd_lBill_THFTYPE_i \<or>
  1409                \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1410                   bnd_lBill_THFTYPE_i)) =
  1411           bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1412            bnd_lBill_THFTYPE_i) =
  1413          False \<Longrightarrow>
  1414          bnd_holdsDuring_THFTYPE_IiooI
  1415           (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1416           (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1417                  bnd_lBill_THFTYPE_i \<or>
  1418               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1419                  bnd_lBill_THFTYPE_i)) =
  1420          True \<or>
  1421          bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1422           bnd_lBill_THFTYPE_i =
  1423          True"
  1424 (* apply (erule extuni_bool2) *)
  1425 (* done *)
  1426 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "25") 1*})
  1427 
  1428      (* (Annotated_step ("26", "extuni_bool1"), *)
  1429 lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
  1430                  (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1431                  (\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1432                         bnd_lMary_THFTYPE_i
  1433                         bnd_lBill_THFTYPE_i \<or>
  1434                      \<not> bnd_likes_THFTYPE_IiioI
  1435                         bnd_lSue_THFTYPE_i
  1436                         bnd_lBill_THFTYPE_i)) =
  1437                 bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
  1438                False \<Longrightarrow>
  1439          \<forall>SV2. bnd_holdsDuring_THFTYPE_IiooI
  1440                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1441                 (\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1442                        bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
  1443                     \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1444                        bnd_lBill_THFTYPE_i)) =
  1445                False \<or>
  1446                bnd_holdsDuring_THFTYPE_IiooI SV2 True = False"
  1447 (* apply (rule allI, erule allE) *)
  1448 (* apply (erule extuni_bool1) *)
  1449 (* done *)
  1450 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "26") 1*})
  1451 
  1452      (* (Annotated_step ("27", "extuni_bool2"), *)
  1453 lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
  1454                  (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1455                  (\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1456                         bnd_lMary_THFTYPE_i
  1457                         bnd_lBill_THFTYPE_i \<or>
  1458                      \<not> bnd_likes_THFTYPE_IiioI
  1459                         bnd_lSue_THFTYPE_i
  1460                         bnd_lBill_THFTYPE_i)) =
  1461                 bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
  1462                False \<Longrightarrow>
  1463          \<forall>SV2. bnd_holdsDuring_THFTYPE_IiooI
  1464                 (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1465                 (\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1466                        bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
  1467                     \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1468                        bnd_lBill_THFTYPE_i)) =
  1469                True \<or>
  1470                bnd_holdsDuring_THFTYPE_IiooI SV2 True = True"
  1471 (* apply (rule allI, erule allE) *)
  1472 (* apply (erule extuni_bool2) *)
  1473 (* done *)
  1474 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "27") 1*})
  1475 
  1476      (* (Annotated_step ("30", "extuni_bool1"), *)
  1477 lemma "((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1478                  bnd_lBill_THFTYPE_i \<or>
  1479               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1480                  bnd_lBill_THFTYPE_i)) =
  1481           True) =
  1482          False \<Longrightarrow>
  1483          (\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1484                 bnd_lBill_THFTYPE_i \<or>
  1485              \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1486                 bnd_lBill_THFTYPE_i)) =
  1487          False \<or>
  1488          True = False"
  1489 (* apply (erule extuni_bool1) *)
  1490 (* done *)
  1491 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "30") 1*})
  1492 
  1493      (* (Annotated_step ("29", "extuni_bind"), *)
  1494 lemma "(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
  1495           bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) =
  1496          False \<or>
  1497          ((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1498                  bnd_lBill_THFTYPE_i \<or>
  1499               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1500                  bnd_lBill_THFTYPE_i)) =
  1501           True) =
  1502          False \<Longrightarrow>
  1503          ((\<not> (\<not> bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i
  1504                  bnd_lBill_THFTYPE_i \<or>
  1505               \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1506                  bnd_lBill_THFTYPE_i)) =
  1507           True) =
  1508          False"
  1509 (* apply (tactic {*break_hypotheses 1*}) *)
  1510 (* apply (erule extuni_bind) *)
  1511 (* apply (tactic {*clause_breaker 1*}) *)
  1512 (* done *)
  1513 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "29") 1*})
  1514 
  1515      (* (Annotated_step ("28", "extuni_dec"), *)
  1516 lemma "\<forall>SV2. (bnd_holdsDuring_THFTYPE_IiooI
  1517                  (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i)
  1518                  (\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1519                         bnd_lMary_THFTYPE_i
  1520                         bnd_lBill_THFTYPE_i \<or>
  1521                      \<not> bnd_likes_THFTYPE_IiioI
  1522                         bnd_lSue_THFTYPE_i
  1523                         bnd_lBill_THFTYPE_i)) =
  1524                 bnd_holdsDuring_THFTYPE_IiooI SV2 True) =
  1525                False \<Longrightarrow>
  1526          \<forall>SV2. (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i =
  1527                 SV2) =
  1528                False \<or>
  1529                ((\<not> (\<not> bnd_likes_THFTYPE_IiioI
  1530                        bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i \<or>
  1531                     \<not> bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i
  1532                        bnd_lBill_THFTYPE_i)) =
  1533                 True) =
  1534                False"
  1535 (* apply (rule allI) *)
  1536 (* apply (erule_tac x = "SV2" in allE) *)
  1537 (* apply (erule extuni_dec_2) *)
  1538 (* done *)
  1539 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "28") 1*})
  1540 *)
  1541 
  1542 (* QUA002^1
  1543    (* [[(Annotated_step ("49", "extuni_dec"), *)
  1544 lemma "((bnd_sK3_E = bnd_sK1_X1 \<or> bnd_sK3_E = bnd_sK2_X2) =
  1545           (bnd_sK3_E = bnd_sK2_X2 \<or> bnd_sK3_E = bnd_sK1_X1)) =
  1546          False \<Longrightarrow>
  1547          ((bnd_sK3_E = bnd_sK2_X2) = (bnd_sK3_E = bnd_sK2_X2)) =
  1548          False \<or>
  1549          ((bnd_sK3_E = bnd_sK1_X1) = (bnd_sK3_E = bnd_sK1_X1)) =
  1550          False"
  1551 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "49") 1*})
  1552 
  1553      (* (Annotated_step ("20", "unfold_def"), *)
  1554 lemma "(bnd_addition bnd_sK1_X1 bnd_sK2_X2 \<noteq>
  1555           bnd_addition bnd_sK2_X2 bnd_sK1_X1) =
  1556          True \<Longrightarrow>
  1557          (bnd_sup
  1558            (\<lambda>SX0::TPTP_Interpret.ind.
  1559                SX0 = bnd_sK1_X1 \<or> SX0 = bnd_sK2_X2) \<noteq>
  1560           bnd_sup
  1561            (\<lambda>SX0::TPTP_Interpret.ind.
  1562                SX0 = bnd_sK2_X2 \<or> SX0 = bnd_sK1_X1)) =
  1563          True"
  1564 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "20") 1*})
  1565 *)
  1566 
  1567 (*
  1568 (*SEU620^2*)
  1569      (* (Annotated_step ("11", "unfold_def"), *)
  1570 lemma "bnd_kpairiskpair =
  1571          (\<forall>Xx Xy.
  1572              bnd_iskpair
  1573               (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
  1574                 (bnd_setadjoin
  1575                   (bnd_setadjoin Xx
  1576                     (bnd_setadjoin Xy bnd_emptyset))
  1577                   bnd_emptyset))) \<and>
  1578          bnd_kpair =
  1579          (\<lambda>Xx Xy.
  1580              bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
  1581               (bnd_setadjoin
  1582                 (bnd_setadjoin Xx
  1583                   (bnd_setadjoin Xy bnd_emptyset))
  1584                 bnd_emptyset)) \<and>
  1585          bnd_iskpair =
  1586          (\<lambda>A. \<exists>Xx. bnd_in Xx (bnd_setunion A) \<and>
  1587                    (\<exists>Xy. bnd_in Xy (bnd_setunion A) \<and>
  1588                          A =
  1589                          bnd_setadjoin
  1590                           (bnd_setadjoin Xx bnd_emptyset)
  1591                           (bnd_setadjoin
  1592                             (bnd_setadjoin Xx
  1593                               (bnd_setadjoin Xy bnd_emptyset))
  1594                             bnd_emptyset))) \<and>
  1595          (\<forall>SY5 SY6.
  1596              (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1597                (bnd_setadjoin
  1598                  (bnd_setadjoin SY5
  1599                    (bnd_setadjoin SY6 bnd_emptyset))
  1600                  bnd_emptyset) =
  1601               bnd_setadjoin
  1602                (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
  1603                (bnd_setadjoin
  1604                  (bnd_setadjoin (bnd_sK3 SY6 SY5)
  1605                    (bnd_setadjoin (bnd_sK4 SY6 SY5)
  1606                      bnd_emptyset))
  1607                  bnd_emptyset) \<and>
  1608               bnd_in (bnd_sK4 SY6 SY5)
  1609                (bnd_setunion
  1610                  (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1611                    (bnd_setadjoin
  1612                      (bnd_setadjoin SY5
  1613                        (bnd_setadjoin SY6 bnd_emptyset))
  1614                      bnd_emptyset)))) \<and>
  1615              bnd_in (bnd_sK3 SY6 SY5)
  1616               (bnd_setunion
  1617                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1618                   (bnd_setadjoin
  1619                     (bnd_setadjoin SY5
  1620                       (bnd_setadjoin SY6 bnd_emptyset))
  1621                     bnd_emptyset)))) =
  1622          True \<Longrightarrow>
  1623          (\<forall>SX0 SX1.
  1624              \<not> (\<not> \<not> (bnd_setadjoin
  1625                       (bnd_setadjoin SX0 bnd_emptyset)
  1626                       (bnd_setadjoin
  1627                         (bnd_setadjoin SX0
  1628                           (bnd_setadjoin SX1 bnd_emptyset))
  1629                         bnd_emptyset) \<noteq>
  1630                      bnd_setadjoin
  1631                       (bnd_setadjoin (bnd_sK3 SX1 SX0)
  1632                         bnd_emptyset)
  1633                       (bnd_setadjoin
  1634                         (bnd_setadjoin (bnd_sK3 SX1 SX0)
  1635                           (bnd_setadjoin (bnd_sK4 SX1 SX0)
  1636                             bnd_emptyset))
  1637                         bnd_emptyset) \<or>
  1638                      \<not> bnd_in (bnd_sK4 SX1 SX0)
  1639                         (bnd_setunion
  1640                           (bnd_setadjoin
  1641                             (bnd_setadjoin SX0 bnd_emptyset)
  1642                             (bnd_setadjoin
  1643                               (bnd_setadjoin SX0
  1644 (bnd_setadjoin SX1 bnd_emptyset))
  1645                               bnd_emptyset)))) \<or>
  1646                 \<not> bnd_in (bnd_sK3 SX1 SX0)
  1647                    (bnd_setunion
  1648                      (bnd_setadjoin
  1649                        (bnd_setadjoin SX0 bnd_emptyset)
  1650                        (bnd_setadjoin
  1651                          (bnd_setadjoin SX0
  1652                            (bnd_setadjoin SX1 bnd_emptyset))
  1653                          bnd_emptyset))))) =
  1654          True"
  1655 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
  1656 
  1657      (* (Annotated_step ("3", "unfold_def"), *)
  1658 lemma "bnd_kpairiskpair =
  1659          (\<forall>Xx Xy.
  1660              bnd_iskpair
  1661               (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
  1662                 (bnd_setadjoin
  1663                   (bnd_setadjoin Xx
  1664                     (bnd_setadjoin Xy bnd_emptyset))
  1665                   bnd_emptyset))) \<and>
  1666          bnd_kpair =
  1667          (\<lambda>Xx Xy.
  1668              bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset)
  1669               (bnd_setadjoin
  1670                 (bnd_setadjoin Xx
  1671                   (bnd_setadjoin Xy bnd_emptyset))
  1672                 bnd_emptyset)) \<and>
  1673          bnd_iskpair =
  1674          (\<lambda>A. \<exists>Xx. bnd_in Xx (bnd_setunion A) \<and>
  1675                    (\<exists>Xy. bnd_in Xy (bnd_setunion A) \<and>
  1676                          A =
  1677                          bnd_setadjoin
  1678                           (bnd_setadjoin Xx bnd_emptyset)
  1679                           (bnd_setadjoin
  1680                             (bnd_setadjoin Xx
  1681                               (bnd_setadjoin Xy bnd_emptyset))
  1682                             bnd_emptyset))) \<and>
  1683          (bnd_kpairiskpair \<longrightarrow>
  1684           (\<forall>Xx Xy. bnd_iskpair (bnd_kpair Xx Xy))) =
  1685          False \<Longrightarrow>
  1686          ((\<forall>SY5 SY6.
  1687               \<exists>SY7. bnd_in SY7
  1688                      (bnd_setunion
  1689                        (bnd_setadjoin
  1690                          (bnd_setadjoin SY5 bnd_emptyset)
  1691                          (bnd_setadjoin
  1692                            (bnd_setadjoin SY5
  1693                              (bnd_setadjoin SY6 bnd_emptyset))
  1694                            bnd_emptyset))) \<and>
  1695                     (\<exists>SY8. bnd_in SY8
  1696                             (bnd_setunion
  1697                               (bnd_setadjoin
  1698 (bnd_setadjoin SY5 bnd_emptyset)
  1699 (bnd_setadjoin
  1700   (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
  1701   bnd_emptyset))) \<and>
  1702                            bnd_setadjoin
  1703                             (bnd_setadjoin SY5 bnd_emptyset)
  1704                             (bnd_setadjoin
  1705                               (bnd_setadjoin SY5
  1706 (bnd_setadjoin SY6 bnd_emptyset))
  1707                               bnd_emptyset) =
  1708                            bnd_setadjoin
  1709                             (bnd_setadjoin SY7 bnd_emptyset)
  1710                             (bnd_setadjoin
  1711                               (bnd_setadjoin SY7
  1712 (bnd_setadjoin SY8 bnd_emptyset))
  1713                               bnd_emptyset))) \<longrightarrow>
  1714           (\<forall>SY0 SY1.
  1715               \<exists>SY3. bnd_in SY3
  1716                      (bnd_setunion
  1717                        (bnd_setadjoin
  1718                          (bnd_setadjoin SY0 bnd_emptyset)
  1719                          (bnd_setadjoin
  1720                            (bnd_setadjoin SY0
  1721                              (bnd_setadjoin SY1 bnd_emptyset))
  1722                            bnd_emptyset))) \<and>
  1723                     (\<exists>SY4. bnd_in SY4
  1724                             (bnd_setunion
  1725                               (bnd_setadjoin
  1726 (bnd_setadjoin SY0 bnd_emptyset)
  1727 (bnd_setadjoin
  1728   (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
  1729   bnd_emptyset))) \<and>
  1730                            bnd_setadjoin
  1731                             (bnd_setadjoin SY0 bnd_emptyset)
  1732                             (bnd_setadjoin
  1733                               (bnd_setadjoin SY0
  1734 (bnd_setadjoin SY1 bnd_emptyset))
  1735                               bnd_emptyset) =
  1736                            bnd_setadjoin
  1737                             (bnd_setadjoin SY3 bnd_emptyset)
  1738                             (bnd_setadjoin
  1739                               (bnd_setadjoin SY3
  1740 (bnd_setadjoin SY4 bnd_emptyset))
  1741                               bnd_emptyset)))) =
  1742          False"
  1743 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "3") 1*})
  1744 
  1745      (* (Annotated_step ("8", "extcnf_combined"), *)
  1746 lemma "(\<forall>SY5 SY6.
  1747              \<exists>SY7. bnd_in SY7
  1748                     (bnd_setunion
  1749                       (bnd_setadjoin
  1750                         (bnd_setadjoin SY5 bnd_emptyset)
  1751                         (bnd_setadjoin
  1752                           (bnd_setadjoin SY5
  1753                             (bnd_setadjoin SY6 bnd_emptyset))
  1754                           bnd_emptyset))) \<and>
  1755                    (\<exists>SY8. bnd_in SY8
  1756                            (bnd_setunion
  1757                              (bnd_setadjoin
  1758                                (bnd_setadjoin SY5 bnd_emptyset)
  1759                                (bnd_setadjoin
  1760  (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset))
  1761  bnd_emptyset))) \<and>
  1762                           bnd_setadjoin
  1763                            (bnd_setadjoin SY5 bnd_emptyset)
  1764                            (bnd_setadjoin
  1765                              (bnd_setadjoin SY5
  1766                                (bnd_setadjoin SY6 bnd_emptyset))
  1767                              bnd_emptyset) =
  1768                           bnd_setadjoin
  1769                            (bnd_setadjoin SY7 bnd_emptyset)
  1770                            (bnd_setadjoin
  1771                              (bnd_setadjoin SY7
  1772                                (bnd_setadjoin SY8 bnd_emptyset))
  1773                              bnd_emptyset))) =
  1774          True \<Longrightarrow>
  1775          (\<forall>SY5 SY6.
  1776              (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1777                (bnd_setadjoin
  1778                  (bnd_setadjoin SY5
  1779                    (bnd_setadjoin SY6 bnd_emptyset))
  1780                  bnd_emptyset) =
  1781               bnd_setadjoin
  1782                (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset)
  1783                (bnd_setadjoin
  1784                  (bnd_setadjoin (bnd_sK3 SY6 SY5)
  1785                    (bnd_setadjoin (bnd_sK4 SY6 SY5)
  1786                      bnd_emptyset))
  1787                  bnd_emptyset) \<and>
  1788               bnd_in (bnd_sK4 SY6 SY5)
  1789                (bnd_setunion
  1790                  (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1791                    (bnd_setadjoin
  1792                      (bnd_setadjoin SY5
  1793                        (bnd_setadjoin SY6 bnd_emptyset))
  1794                      bnd_emptyset)))) \<and>
  1795              bnd_in (bnd_sK3 SY6 SY5)
  1796               (bnd_setunion
  1797                 (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset)
  1798                   (bnd_setadjoin
  1799                     (bnd_setadjoin SY5
  1800                       (bnd_setadjoin SY6 bnd_emptyset))
  1801                     bnd_emptyset)))) =
  1802          True"
  1803 by (tactic {*
  1804 HEADGOAL (extcnf_combined_tac Full false (hd prob_names))
  1805 *})
  1806 
  1807      (* (Annotated_step ("7", "extcnf_combined"), *)
  1808 lemma "(\<not> (\<forall>SY0 SY1.
  1809                 \<exists>SY3. bnd_in SY3
  1810                        (bnd_setunion
  1811                          (bnd_setadjoin
  1812                            (bnd_setadjoin SY0 bnd_emptyset)
  1813                            (bnd_setadjoin
  1814                              (bnd_setadjoin SY0
  1815                                (bnd_setadjoin SY1 bnd_emptyset))
  1816                              bnd_emptyset))) \<and>
  1817                       (\<exists>SY4. bnd_in SY4
  1818                               (bnd_setunion
  1819 (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset)
  1820   (bnd_setadjoin
  1821     (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
  1822     bnd_emptyset))) \<and>
  1823                              bnd_setadjoin
  1824                               (bnd_setadjoin SY0 bnd_emptyset)
  1825                               (bnd_setadjoin
  1826 (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset))
  1827 bnd_emptyset) =
  1828                              bnd_setadjoin
  1829                               (bnd_setadjoin SY3 bnd_emptyset)
  1830                               (bnd_setadjoin
  1831 (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset))
  1832 bnd_emptyset)))) =
  1833          True \<Longrightarrow>
  1834          (\<forall>SY24.
  1835              (\<forall>SY25.
  1836                  bnd_setadjoin
  1837                   (bnd_setadjoin bnd_sK1 bnd_emptyset)
  1838                   (bnd_setadjoin
  1839                     (bnd_setadjoin bnd_sK1
  1840                       (bnd_setadjoin bnd_sK2 bnd_emptyset))
  1841                     bnd_emptyset) \<noteq>
  1842                  bnd_setadjoin (bnd_setadjoin SY24 bnd_emptyset)
  1843                   (bnd_setadjoin
  1844                     (bnd_setadjoin SY24
  1845                       (bnd_setadjoin SY25 bnd_emptyset))
  1846                     bnd_emptyset) \<or>
  1847                  \<not> bnd_in SY25
  1848                     (bnd_setunion
  1849                       (bnd_setadjoin
  1850                         (bnd_setadjoin bnd_sK1 bnd_emptyset)
  1851                         (bnd_setadjoin
  1852                           (bnd_setadjoin bnd_sK1
  1853                             (bnd_setadjoin bnd_sK2
  1854                               bnd_emptyset))
  1855                           bnd_emptyset)))) \<or>
  1856              \<not> bnd_in SY24
  1857                 (bnd_setunion
  1858                   (bnd_setadjoin
  1859                     (bnd_setadjoin bnd_sK1 bnd_emptyset)
  1860                     (bnd_setadjoin
  1861                       (bnd_setadjoin bnd_sK1
  1862                         (bnd_setadjoin bnd_sK2 bnd_emptyset))
  1863                       bnd_emptyset)))) =
  1864          True"
  1865 by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
  1866 *)
  1867 
  1868 (*PUZ081^2*)
  1869 (*
  1870      (* (Annotated_step ("9", "unfold_def"), *)
  1871 lemma "bnd_says bnd_mel
  1872           (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) \<Longrightarrow>
  1873          bnd_says bnd_mel
  1874           (\<not> bnd_knave bnd_zoey \<and> \<not> bnd_knave bnd_mel) =
  1875          True"
  1876 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*})
  1877 
  1878      (* (Annotated_step ("10", "unfold_def"), *)
  1879 lemma "bnd_says bnd_zoey (bnd_knave bnd_mel) \<Longrightarrow>
  1880          bnd_says bnd_zoey (bnd_knave bnd_mel) = True"
  1881 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})
  1882 
  1883      (* (Annotated_step ("11", "unfold_def"), *)
  1884 lemma "\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S \<Longrightarrow>
  1885          (\<forall>P S. bnd_knave P \<and> bnd_says P S \<longrightarrow> \<not> S) = True"
  1886 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
  1887 
  1888      (* (Annotated_step ("12", "unfold_def"), *)
  1889 lemma "\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S \<Longrightarrow>
  1890          (\<forall>P S. bnd_knight P \<and> bnd_says P S \<longrightarrow> S) = True"
  1891 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})
  1892 
  1893      (* (Annotated_step ("13", "unfold_def"), *)
  1894 lemma "\<forall>P. bnd_knight P \<noteq> bnd_knave P \<Longrightarrow>
  1895          (\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True"
  1896 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "13") 1*})
  1897 
  1898      (* (Annotated_step ("15", "extcnf_combined"), *)
  1899 lemma "(\<not> (\<exists>TZ TM. TZ bnd_zoey \<and> TM bnd_mel)) = True \<Longrightarrow>
  1900          ((\<forall>TM. \<not> TM bnd_mel) \<or> (\<forall>TZ. \<not> TZ bnd_zoey)) = True"
  1901 by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})
  1902 
  1903      (* (Annotated_step ("18", "extcnf_combined"), *)
  1904 lemma "(\<forall>P. bnd_knight P \<noteq> bnd_knave P) = True \<Longrightarrow>
  1905          ((\<forall>P. \<not> bnd_knave P \<or> \<not> bnd_knight P) \<and>
  1906           (\<forall>P. bnd_knave P \<or> bnd_knight P)) =
  1907          True"
  1908 by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*})
  1909 *)
  1910 
  1911 (*
  1912 (*from SEU667^2.p.out*)
  1913      (* (Annotated_step ("10", "unfold_def"), *)
  1914 lemma "bnd_dpsetconstrSub =
  1915          (\<forall>A B Xphi.
  1916              bnd_subset (bnd_dpsetconstr A B Xphi)
  1917               (bnd_cartprod A B)) \<and>
  1918          bnd_dpsetconstr =
  1919          (\<lambda>A B Xphi.
  1920              bnd_dsetconstr (bnd_cartprod A B)
  1921               (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
  1922                          (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
  1923                                Xu = bnd_kpair Xx Xy))) \<and>
  1924          bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
  1925          (\<not> bnd_subset
  1926              (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
  1927                (\<lambda>SY66.
  1928                    \<exists>SY67.
  1929                       bnd_in SY67 bnd_sK1 \<and>
  1930                       (\<exists>SY68.
  1931                           (bnd_in SY68 bnd_sK2 \<and>
  1932                            bnd_sK3 SY67 SY68) \<and>
  1933                           SY66 = bnd_kpair SY67 SY68)))
  1934              (bnd_cartprod bnd_sK1 bnd_sK2)) =
  1935          True \<Longrightarrow>
  1936          (\<not> bnd_subset
  1937              (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2)
  1938                (\<lambda>SX0. \<not> (\<forall>SX1. \<not> \<not> (\<not> bnd_in SX1 bnd_sK1 \<or>
  1939     \<not> \<not> (\<forall>SX2. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX2 bnd_sK2 \<or>
  1940                          \<not> bnd_sK3 SX1 SX2) \<or>
  1941                     SX0 \<noteq> bnd_kpair SX1 SX2))))))
  1942              (bnd_cartprod bnd_sK1 bnd_sK2)) =
  1943          True"
  1944 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*})
  1945 
  1946 
  1947      (* (Annotated_step ("11", "unfold_def"), *)
  1948 lemma "bnd_dpsetconstrSub =
  1949          (\<forall>A B Xphi.
  1950              bnd_subset (bnd_dpsetconstr A B Xphi)
  1951               (bnd_cartprod A B)) \<and>
  1952          bnd_dpsetconstr =
  1953          (\<lambda>A B Xphi.
  1954              bnd_dsetconstr (bnd_cartprod A B)
  1955               (\<lambda>Xu. \<exists>Xx. bnd_in Xx A \<and>
  1956                          (\<exists>Xy. (bnd_in Xy B \<and> Xphi Xx Xy) \<and>
  1957                                Xu = bnd_kpair Xx Xy))) \<and>
  1958          bnd_breln = (\<lambda>A B C. bnd_subset C (bnd_cartprod A B)) \<and>
  1959          (\<forall>SY21 SY22 SY23.
  1960              bnd_subset
  1961               (bnd_dsetconstr (bnd_cartprod SY21 SY22)
  1962                 (\<lambda>SY35.
  1963                     \<exists>SY36.
  1964                        bnd_in SY36 SY21 \<and>
  1965                        (\<exists>SY37.
  1966                            (bnd_in SY37 SY22 \<and> SY23 SY36 SY37) \<and>
  1967                            SY35 = bnd_kpair SY36 SY37)))
  1968               (bnd_cartprod SY21 SY22)) =
  1969          True \<Longrightarrow>
  1970          (\<forall>SX0 SX1 SX2.
  1971              bnd_subset
  1972               (bnd_dsetconstr (bnd_cartprod SX0 SX1)
  1973                 (\<lambda>SX3. \<not> (\<forall>SX4. \<not> \<not> (\<not> bnd_in SX4 SX0 \<or>
  1974      \<not> \<not> (\<forall>SX5. \<not> \<not> (\<not> \<not> (\<not> bnd_in SX5 SX1 \<or> \<not> SX2 SX4 SX5) \<or>
  1975                      SX3 \<noteq> bnd_kpair SX4 SX5))))))
  1976               (bnd_cartprod SX0 SX1)) =
  1977          True"
  1978 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
  1979 *)
  1980 
  1981 (*
  1982 (*from ALG001^5*)
  1983       (* (Annotated_step ("4", "extcnf_forall_neg"), *)
  1984 lemma "(\<forall>(Xh1 :: bnd_g \<Rightarrow> bnd_b) (Xh2 :: bnd_b \<Rightarrow> bnd_a) (Xf1 :: bnd_g \<Rightarrow> bnd_g \<Rightarrow> bnd_g) (Xf2 :: bnd_b \<Rightarrow> bnd_b \<Rightarrow> bnd_b) (Xf3 :: bnd_a \<Rightarrow> bnd_a \<Rightarrow> bnd_a).
  1985              (\<forall>Xx Xy. Xh1 (Xf1 Xx Xy) = Xf2 (Xh1 Xx) (Xh1 Xy)) \<and>
  1986              (\<forall>Xx Xy.
  1987                  Xh2 (Xf2 Xx Xy) = Xf3 (Xh2 Xx) (Xh2 Xy)) \<longrightarrow>
  1988              (\<forall>Xx Xy.
  1989                  Xh2 (Xh1 (Xf1 Xx Xy)) =
  1990                  Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy)))) =
  1991          False \<Longrightarrow>
  1992          ((\<forall>SY35 SY36.
  1993               bnd_sK1 (bnd_sK3 SY35 SY36) =
  1994               bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) \<and>
  1995           (\<forall>SY31 SY32.
  1996               bnd_sK2 (bnd_sK4 SY31 SY32) =
  1997               bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) \<longrightarrow>
  1998           (\<forall>SY39 SY40.
  1999               bnd_sK2 (bnd_sK1 (bnd_sK3 SY39 SY40)) =
  2000               bnd_sK5 (bnd_sK2 (bnd_sK1 SY39))
  2001                (bnd_sK2 (bnd_sK1 SY40)))) =
  2002          False"
  2003 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "4") 1*})
  2004 *)
  2005 
  2006 (*SYN044^4*)
  2007 (*
  2008 declare [[ML_print_depth = 1400]]
  2009 (* the_tactics *)
  2010 *}
  2011 
  2012      (* (Annotated_step ("12", "unfold_def"), *)
  2013 lemma "bnd_mor =
  2014          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
  2015              (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2016              X U \<or> Y U) \<and>
  2017          bnd_mnot =
  2018          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2019              \<not> X U) \<and>
  2020          bnd_mimplies =
  2021          (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
  2022          bnd_mbox_s4 =
  2023          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
  2024              \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
  2025          bnd_mand =
  2026          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
  2027              (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2028              X U \<and> Y U) \<and>
  2029          bnd_ixor =
  2030          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2031              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2032              bnd_inot (bnd_iequiv P Q)) \<and>
  2033          bnd_ivalid = All \<and>
  2034          bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
  2035          bnd_isatisfiable = Ex \<and>
  2036          bnd_ior =
  2037          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2038              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2039              bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
  2040          bnd_inot =
  2041          (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
  2042              bnd_mnot (bnd_mbox_s4 P)) \<and>
  2043          bnd_iinvalid =
  2044          (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
  2045              \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
  2046          bnd_iimplies =
  2047          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2048              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2049              bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
  2050          bnd_iimplied =
  2051          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2052              Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
  2053          bnd_ifalse = bnd_inot bnd_itrue \<and>
  2054          bnd_iequiv =
  2055          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2056              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2057              bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
  2058          bnd_icountersatisfiable =
  2059          (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
  2060              \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
  2061          bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
  2062          bnd_iand = bnd_mand \<and>
  2063          (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
  2064              Z::TPTP_Interpret.ind.
  2065              bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) \<Longrightarrow>
  2066          (\<forall>(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind)
  2067              Z::TPTP_Interpret.ind.
  2068              bnd_irel X Y \<and> bnd_irel Y Z \<longrightarrow> bnd_irel X Z) =
  2069          True"
  2070 (* by (tactic {*tectoc @{context}*}) *)
  2071 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*})
  2072 
  2073      (* (Annotated_step ("11", "unfold_def"), *)
  2074 lemma "bnd_mor =
  2075          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
  2076              (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2077              X U \<or> Y U) \<and>
  2078          bnd_mnot =
  2079          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2080              \<not> X U) \<and>
  2081          bnd_mimplies =
  2082          (\<lambda>U::TPTP_Interpret.ind \<Rightarrow> bool. bnd_mor (bnd_mnot U)) \<and>
  2083          bnd_mbox_s4 =
  2084          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool) X::TPTP_Interpret.ind.
  2085              \<forall>Y::TPTP_Interpret.ind. bnd_irel X Y \<longrightarrow> P Y) \<and>
  2086          bnd_mand =
  2087          (\<lambda>(X::TPTP_Interpret.ind \<Rightarrow> bool)
  2088              (Y::TPTP_Interpret.ind \<Rightarrow> bool) U::TPTP_Interpret.ind.
  2089              X U \<and> Y U) \<and>
  2090          bnd_ixor =
  2091          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2092              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2093              bnd_inot (bnd_iequiv P Q)) \<and>
  2094          bnd_ivalid = All \<and>
  2095          bnd_itrue = (\<lambda>W::TPTP_Interpret.ind. True) \<and>
  2096          bnd_isatisfiable = Ex \<and>
  2097          bnd_ior =
  2098          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2099              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2100              bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
  2101          bnd_inot =
  2102          (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool.
  2103              bnd_mnot (bnd_mbox_s4 P)) \<and>
  2104          bnd_iinvalid =
  2105          (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
  2106              \<forall>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
  2107          bnd_iimplies =
  2108          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2109              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2110              bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) \<and>
  2111          bnd_iimplied =
  2112          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2113              Q::TPTP_Interpret.ind \<Rightarrow> bool. bnd_iimplies Q P) \<and>
  2114          bnd_ifalse = bnd_inot bnd_itrue \<and>
  2115          bnd_iequiv =
  2116          (\<lambda>(P::TPTP_Interpret.ind \<Rightarrow> bool)
  2117              Q::TPTP_Interpret.ind \<Rightarrow> bool.
  2118              bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) \<and>
  2119          bnd_icountersatisfiable =
  2120          (\<lambda>Phi::TPTP_Interpret.ind \<Rightarrow> bool.
  2121              \<exists>W::TPTP_Interpret.ind. \<not> Phi W) \<and>
  2122          bnd_iatom = (\<lambda>P::TPTP_Interpret.ind \<Rightarrow> bool. P) \<and>
  2123          bnd_iand = bnd_mand \<and>
  2124          bnd_ivalid
  2125           (bnd_iimplies (bnd_iatom bnd_q) (bnd_iatom bnd_r)) \<Longrightarrow>
  2126          (\<forall>SY161::TPTP_Interpret.ind.
  2127              \<not> (\<forall>SY162::TPTP_Interpret.ind.
  2128                    bnd_irel SY161 SY162 \<longrightarrow> bnd_q SY162) \<or>
  2129              (\<forall>SY163::TPTP_Interpret.ind.
  2130                  bnd_irel SY161 SY163 \<longrightarrow> bnd_r SY163)) =
  2131          True"
  2132 (* by (tactic {*tectoc @{context}*}) *)
  2133 by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*})
  2134 
  2135 lemma "
  2136 (\<forall>SY136.
  2137     \<not> (\<forall>SY137. bnd_irel SY136 SY137 \<longrightarrow> bnd_r SY137) \<or>
  2138     (\<forall>SY138.
  2139         bnd_irel SY136 SY138 \<longrightarrow> bnd_p SY138 \<and> bnd_q SY138)) =
  2140 True \<Longrightarrow>
  2141 (\<forall>SY136.
  2142     bnd_irel SY136 (bnd_sK5 SY136) \<and> \<not> bnd_r (bnd_sK5 SY136) \<or>
  2143     (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_p SY138) \<and>
  2144     (\<forall>SY138. \<not> bnd_irel SY136 SY138 \<or> bnd_q SY138)) =
  2145 True"
  2146 by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*})
  2147 *)
  2148 
  2149      (* (Annotated_step ("11", "extcnf_forall_neg"), *)
  2150 lemma "\<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
  2151             (\<forall>SY2::TPTP_Interpret.ind.
  2152                 \<not> (\<not> (\<not> SV1 SY2 \<or> SEV405_5_bnd_cA) \<or>
  2153                    \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 SY2))) =
  2154             False \<Longrightarrow>
  2155          \<forall>SV1::TPTP_Interpret.ind \<Rightarrow> bool.
  2156             (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
  2157                 \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
  2158             False"
  2159 (* apply (tactic {*full_extcnf_combined_tac*}) *)
  2160 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
  2161 
  2162      (* (Annotated_step ("13", "extcnf_forall_pos"), *)
  2163 lemma "(\<forall>SY31 SY32.
  2164              bnd_sK2 (bnd_sK4 SY31 SY32) =
  2165              bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) =
  2166          True \<Longrightarrow>
  2167          \<forall>SV1. (\<forall>SY42.
  2168                    bnd_sK2 (bnd_sK4 SV1 SY42) =
  2169                    bnd_sK5 (bnd_sK2 SV1) (bnd_sK2 SY42)) =
  2170                True"
  2171 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
  2172 
  2173      (* (Annotated_step ("14", "extcnf_forall_pos"), *)
  2174 lemma "(\<forall>SY35 SY36.
  2175              bnd_sK1 (bnd_sK3 SY35 SY36) =
  2176              bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) =
  2177          True \<Longrightarrow>
  2178          \<forall>SV2. (\<forall>SY43.
  2179                    bnd_sK1 (bnd_sK3 SV2 SY43) =
  2180                    bnd_sK4 (bnd_sK1 SV2) (bnd_sK1 SY43)) =
  2181                True"
  2182 by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
  2183 
  2184 
  2185 (*from SYO198^5.p.out*)
  2186    (* [[(Annotated_step ("11", "extcnf_forall_special_pos"), *)
  2187 lemma "(\<forall>SX0::bool \<Rightarrow> bool.
  2188              \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
  2189          True \<Longrightarrow>
  2190          (\<not> \<not> (\<not> True \<or> \<not> True)) = True"
  2191 apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
  2192 done
  2193 
  2194      (* (Annotated_step ("13", "extcnf_forall_special_pos"), *)
  2195 lemma "(\<forall>SX0::bool \<Rightarrow> bool.
  2196              \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
  2197          True \<Longrightarrow>
  2198          (\<not> \<not> (\<not> bnd_sK1_Xx \<or> \<not> bnd_sK2_Xy)) = True"
  2199 apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
  2200 done
  2201 
  2202    (* [[(Annotated_step ("8", "polarity_switch"), *)
  2203 lemma "(\<forall>(Xx::bool) (Xy::bool) Xz::bool. True \<and> True \<longrightarrow> True) =
  2204          False \<Longrightarrow>
  2205          (\<not> (\<forall>(Xx::bool) (Xy::bool) Xz::bool.
  2206                 True \<and> True \<longrightarrow> True)) =
  2207          True"
  2208 apply (tactic \<open>nonfull_extcnf_combined_tac @{context} [Polarity_switch]\<close>)
  2209 done
  2210 
  2211 lemma "((\<forall>SY22 SY23 SY24.
  2212        bnd_sK1_RRR SY22 SY23 \<and> bnd_sK1_RRR SY23 SY24 \<longrightarrow>
  2213        bnd_sK1_RRR SY22 SY24) \<and>
  2214    (\<forall>SY25.
  2215        (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
  2216        (\<forall>SY27.
  2217            (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
  2218            bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) \<longrightarrow>
  2219    (\<forall>SY29. \<exists>SY30. \<forall>SY31. SY29 SY31 \<longrightarrow> bnd_sK1_RRR SY31 SY30)) =
  2220   False \<Longrightarrow>
  2221   (\<forall>SY25.
  2222       (\<forall>SY26. SY25 SY26 \<longrightarrow> bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) \<and>
  2223       (\<forall>SY27.
  2224           (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
  2225           bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) =
  2226   True"
  2227 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2228 done
  2229 
  2230 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
  2231    (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
  2232    (\<forall>A B. A = B \<longrightarrow>
  2233           (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
  2234    (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
  2235           bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  2236   False \<Longrightarrow>
  2237  (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) =
  2238   True"
  2239 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2240 done
  2241 
  2242 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
  2243    (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
  2244    (\<forall>A B. A = B \<longrightarrow>
  2245           (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
  2246    (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
  2247           bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  2248   False \<Longrightarrow>
  2249   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) =
  2250   True"
  2251 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2252 done
  2253 
  2254 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
  2255    (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
  2256    (\<forall>A B. A = B \<longrightarrow>
  2257           (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
  2258    (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
  2259           bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  2260   False \<Longrightarrow>
  2261   (\<forall>A B. A = B \<longrightarrow>
  2262          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) =
  2263   True"
  2264 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2265 done
  2266 
  2267 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
  2268    (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) \<longrightarrow>
  2269    (\<forall>A B. A = B \<longrightarrow>
  2270           (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) \<longrightarrow>
  2271    (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
  2272           bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset)) =
  2273   False \<Longrightarrow>
  2274   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
  2275          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset) =
  2276   False"
  2277 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2278 done
  2279 
  2280 (*nested conjunctions*)
  2281 lemma "((((\<forall>Xx. bnd_cP bnd_e Xx = Xx) \<and>
  2282      (\<forall>Xy. bnd_cP Xy bnd_e = Xy)) \<and>
  2283     (\<forall>Xz. bnd_cP Xz Xz = bnd_e)) \<and>
  2284    (\<forall>Xx Xy Xz.
  2285        bnd_cP (bnd_cP Xx Xy) Xz = bnd_cP Xx (bnd_cP Xy Xz)) \<longrightarrow>
  2286    (\<forall>Xa Xb. bnd_cP Xa Xb = bnd_cP Xb Xa)) =
  2287   False \<Longrightarrow>
  2288   (\<forall>Xx. bnd_cP bnd_e Xx = Xx) =
  2289   True"
  2290 apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
  2291 done
  2292 
  2293 end