| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/HOL/TPTP/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 100 kB |
|
Quelle TPTP_Proof_Reconstruction_Test_Units.thySprache: Isabelle |
|||||||||||||||
|
(* Title: HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Author: Nik Sultana, Cambridge University Computer Laboratory Unit tests for proof reconstruction module. *) theory TPTP_Proof_Reconstruction_Test_Units imports TPTP_Test TPTP_Proof_Reconstruction begin declare [[ML_exception_trace, ML_print_depth = 200]] declare [[tptp_trace_reconstruction = true]] lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P ==> apply (tactic ‹canonicalise_qtfr_order @{context} 1›) oops lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P ==> apply (tactic ‹canonicalise_qtfr_order @{context} 1›) apply (rule allI)+ apply (tactic ‹nominal_inst_parametermatch_tac @{context} @{thm allE} 1›)+ oops (*Could test bind_tac further with NUM667^1 inode43*) (* (* SEU581^2.p_nux *) (* (Annotated_step ("inode1", "bind"), *) lemma "∀(SV5::TPTP_Interpret.ind ==> bool) SV6::TPTP_Interpret.ind. (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) (bnd_powerset bnd_sK1_A) = bnd_in (bnd_dsetconstr SV6 SV5) (bnd_powerset SV6)) = False ==> (bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) (bnd_powerset bnd_sK1_A) = bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) (bnd_powerset bnd_sK1_A)) = False" ML_prf {* open TPTP_Syntax; open TPTP_Proof; val binds = [Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))), Bind ("SV5", (* |> TPTP_Reconstruct.permute *) (* val binds = [Bind ("SV5", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term Bind ("SV6", Atom (THF_Atom_term (Term_Func (Uninterpreted "sK1_A", [])))) ] *) val tec = (* map (bind_tac @{context} (hd prob_names)) binds |> FIRST *) bind_tac @{context} (hd prob_names) binds *} apply (tactic {*tec*}) done (* (Annotated_step ("inode2", "bind"), *) lemma "∀(SV7::TPTP_Interpret.ind) SV8::TPTP_Interpret.ind. (bnd_subset SV8 SV7 = bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) bnd_sK1_A) = False ∨ bnd_in SV8 (bnd_powerset SV7) = False ==> (bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) bnd_sK1_A = bnd_subset (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) bnd_sK1_A) = False ∨ bnd_in (bnd_dsetconstr bnd_sK1_A bnd_sK2_SY15) (bnd_powerset bnd_sK1_A) = False" ML_prf {* open TPTP_Syntax; open TPTP_Proof; val binds = [Bind ("SV8", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic Apply, [ (* |> TPTP_Reconstruct.permute *) val tec = (* map (bind_tac @{context} (hd prob_names)) binds |> FIRST *) bind_tac @{context} (hd prob_names) binds *} apply (tactic {*tec*}) done *) (* from SEU897^5 lemma " ∀SV9 SV10 SV11 SV12 SV13 SV14. (((((bnd_sK5_SY14 SV14 SV13 SV12 = SV11) = False ∨ (bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 SV11)) = False) ∨ bnd_cR SV14 = False) ∨ (SV12 = SV13 SV14) = False) ∨ bnd_cR SV9 = False) ∨ (SV11 = SV10 SV9) = False ==> ∀SV14 SV13 SV12 SV10 SV9. (((((bnd_sK5_SY14 SV14 SV13 SV12 = bnd_sK5_SY14 SV14 SV13 SV12) = False ∨ (bnd_sK4_SX0 = SV10 (bnd_sK5_SY14 SV9 SV10 (bnd_sK5_SY14 SV14 SV13 SV12))) = False) ∨ bnd_cR SV14 = False) ∨ (SV12 = SV13 SV14) = False) ∨ bnd_cR SV9 = False) ∨ (bnd_sK5_SY14 SV14 SV13 SV12 = SV10 SV9) = False" ML_prf {* open TPTP_Syntax; open TPTP_Proof; val binds = [Bind ("SV11", Fmla (Interpreted_ExtraLogic Apply, [Fmla (Interpreted_ExtraLogic val tec = bind_tac @{context} (hd prob_names) binds *} apply (tactic {*tec*}) done *) subsection "Interpreting the inferences" (*from SET598^5 lemma "(bnd_sK1_X = (λSY17. bnd_sK2_Y SY17 ∧ bnd_sK3_Z SY17) ⟶ ((∀SY25. bnd_sK1_X SY25 ⟶ bnd_sK2_Y SY25) ∧ (∀SY26. bnd_sK1_X SY26 ⟶ bnd_sK3_Z SY26)) ∧ (∀SY27. (∀SY21. SY27 SY21 ⟶ bnd_sK2_Y SY21) ∧ (∀SY15. SY27 SY15 ⟶ bnd_sK3_Z SY15) ⟶ (∀SY30. SY27 SY30 ⟶ bnd_sK1_X SY30))) = False ==> (¬ (bnd_sK1_X = (λSY17. bnd_sK2_Y SY17 ∧ bnd_sK3_Z SY17) ⟶ ((∀SY25. bnd_sK1_X SY25 ⟶ bnd_sK2_Y SY25) ∧ (∀SY26. bnd_sK1_X SY26 ⟶ bnd_sK3_Z SY26)) ∧ (∀SY27. (∀SY21. SY27 SY21 ⟶ bnd_sK2_Y SY21) ∧ (∀SY15. SY27 SY15 ⟶ bnd_sK3_Z SY15) ⟶ (∀SY30. SY27 SY30 ⟶ bnd_sK1_X SY30)))) = True" apply (tactic {*polarity_switch_tac @{context}*}) done lemma " (((∀SY25. bnd_sK1_X SY25 ⟶ bnd_sK2_Y SY25) ∧ (∀SY26. bnd_sK1_X SY26 ⟶ bnd_sK3_Z SY26)) ∧ (∀SY27. (∀SY21. SY27 SY21 ⟶ bnd_sK2_Y SY21) ∧ (∀SY15. SY27 SY15 ⟶ bnd_sK3_Z SY15) ⟶ (∀SY30. SY27 SY30 ⟶ bnd_sK1_X SY30)) ⟶ bnd_sK1_X = (λSY17. bnd_sK2_Y SY17 ∧ bnd_sK3_Z SY17)) = False ==> (¬ (((∀SY25. bnd_sK1_X SY25 ⟶ bnd_sK2_Y SY25) ∧ (∀SY26. bnd_sK1_X SY26 ⟶ bnd_sK3_Z SY26)) ∧ (∀SY27. (∀SY21. SY27 SY21 ⟶ bnd_sK2_Y SY21) ∧ (∀SY15. SY27 SY15 ⟶ bnd_sK3_Z SY15) ⟶ (∀SY30. SY27 SY30 ⟶ bnd_sK1_X SY30)) ⟶ bnd_sK1_X = (λSY17. bnd_sK2_Y SY17 ∧ bnd_sK3_Z SY17))) = True" apply (tactic {*polarity_switch_tac @{context}*}) done *) (* beware lack of type annotations (* lemma "!!x. (A x = B x) = False ==> (B x = A x) = False" *) (* lemma "!!x. (A x = B x) = True ==> (B x = A x) = True" *) (* lemma "((A x) = (B x)) = True ==> ((B x) = (A x)) = True" *) lemma "(A = B) = True ==> (B = A) = True" *) lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False" apply (tactic ‹expander_animal @{context} 1›) oops lemma "(A & B) ==> ~(~A | ~B)" by (tactic ‹expander_animal @{context} 1›) lemma "(A | B) ==> ~(~A & ~B)" by (tactic ‹expander_animal @{context} 1›) lemma "(A | B) | C ==> A | (B | C)" by (tactic ‹expander_animal @{context} 1›) lemma "(~~A) = B ==> A = B" by (tactic ‹expander_animal @{context} 1›) lemma "~ ~ (A = True) ==> A = True" by (tactic ‹expander_animal @{context} 1›) (*This might not be a goal which might realistically arise: lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *) lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))" apply (tactic ‹expander_animal @{context} 1›)+ apply (rule conjI) apply assumption apply (rule sym, assumption) done lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" by (tactic ‹expander_animal @{context} 1›)+ (*some lemmas assume constants in the signature of PUZ114^5*) consts PUZ114_5_bnd_sK1 :: "TPTP_Interpret.ind" PUZ114_5_bnd_sK2 :: "TPTP_Interpret.ind" PUZ114_5_bnd_sK3 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" PUZ114_5_bnd_sK4 :: "(TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool) ==> TPTP PUZ114_5_bnd_sK5 :: "(TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool) ==> TPTP PUZ114_5_bnd_s :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" PUZ114_5_bnd_c1 :: TPTP_Interpret.ind (*testing logical expansion*) lemma "!! SY30. (SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1 ∧ (∀Xj Xk. SY30 Xj Xk ⟶ SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk ∧ SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)) ⟶ SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) ==> ( (~ SY30 PUZ114_5_bnd_c1 PUZ114_5_bnd_c1) | (~ (∀Xj Xk. SY30 Xj Xk ⟶ SY30 (PUZ114_5_bnd_s (PUZ114_5_bnd_s Xj)) Xk ∧ SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk))) | SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 )" by (tactic ‹expander_animal @{context} 1›)+ (* extcnf_forall_pos: (! X. L1) | ... | Ln ---------------------------- X' fresh ! X'. (L1[X'/X] | ... | Ln) After elimination rule has been applied we'll have a subgoal which looks like th (! X. L1) ---------------------------- X' fresh ! X'. (L1[X'/X] | ... | Ln) and we need to transform it so that, in Isabelle, we go from (! X. L1) ==> ! X'. (L1[X'/X] | ... | Ln) to ∧ X'. L1[X'/X] ==> (L1[X'/X] | ... | Ln) (where X' is fresh, or renamings are done suitably).*) lemma "A | B ==> A | B | C" apply (tactic ‹flip_conclusion_tac @{context} 1›)+ apply (tactic ‹break_hypotheses 1›)+ oops consts CSR122_1_bnd_lBill_THFTYPE_i :: TPTP_Interpret.ind CSR122_1_bnd_lMary_THFTYPE_i :: TPTP_Interpret.ind CSR122_1_bnd_lSue_THFTYPE_i :: TPTP_Interpret.ind CSR122_1_bnd_n2009_THFTYPE_i :: TPTP_Interpret.ind CSR122_1_bnd_lYearFn_THFTYPE_IiiI :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" CSR122_1_bnd_holdsDuring_THFTYPE_IiooI :: "TPTP_Interpret.ind ==> bool ==> bool" CSR122_1_bnd_likes_THFTYPE_IiioI :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" lemma "∀SV2. (CSR122_1_bnd_holdsDuring_THFTYPE_IiooI (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i) (¬ (¬ CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i ∨ ¬ CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i)) = CSR122_1_bnd_holdsDuring_THFTYPE_IiooI SV2 True) = False ==> ∀SV2. (CSR122_1_bnd_lYearFn_THFTYPE_IiiI CSR122_1_bnd_n2009_THFTYPE_i = SV2) = False ∨ ((¬ (¬ CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lMary_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i ∨ ¬ CSR122_1_bnd_likes_THFTYPE_IiioI CSR122_1_bnd_lSue_THFTYPE_i CSR122_1_bnd_lBill_THFTYPE_i)) = True) = False" apply (rule allI, erule_tac x = "SV2" in allE) apply (tactic ‹extuni_dec_tac @{context} 1›) done (*SEU882^5*) (* lemma "∀(SV2::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind ==> TPTP_Interpret.ind. (SV1 SV2 = bnd_sK1_Xy) = False ==> ∀SV2::TPTP_Interpret.ind. (bnd_sK1_Xy = bnd_sK1_Xy) = False" ML_prf {* open TPTP_Syntax; open TPTP_Proof; val binds = [Bind ("SV1", Quant (Lambda, [("SX0", SOME (Fmla_type (Atom (THF_Atom_term (Term val tec = bind_tac @{context} (hd prob_names) binds *} (* apply (tactic {*strip_qtfrs (* THEN tec *) *) apply (tactic {*tec*}) done *) lemma "A | B ==> C1 | A | C2 | B | C3" apply (erule disjE) apply (tactic ‹clause_breaker 1›) apply (tactic ‹clause_breaker 1›) done lemma "A ==> A" apply (tactic ‹clause_breaker 1›) done typedecl NUM667_1_bnd_nat consts NUM667_1_bnd_less :: "NUM667_1_bnd_nat ==> NUM667_1_bnd_nat ==> bool" NUM667_1_bnd_x :: NUM667_1_bnd_nat NUM667_1_bnd_y :: NUM667_1_bnd_nat (*NUM667^1 node 302 -- dec*) lemma "∀SV12 SV13 SV14 SV9 SV10 SV11. ((((NUM667_1_bnd_less SV12 SV13 = NUM667_1_bnd_less SV11 SV10) = False ∨ (SV14 = SV13) = False) ∨ NUM667_1_bnd_less SV12 SV14 = False) ∨ NUM667_1_bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False ==> ∀SV9 SV14 SV10 SV13 SV11 SV12. (((((SV12 = SV11) = False ∨ (SV13 = SV10) = False) ∨ (SV14 = SV13) = False) ∨ NUM667_1_bnd_less SV12 SV14 = False) ∨ NUM667_1_bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False" apply (tactic ‹strip_qtfrs_tac @{context}›) apply (tactic ‹break_hypotheses 1›) apply (tactic ‹ALLGOALS (TRY o clause_breaker)›) apply (tactic ‹extuni_dec_tac @{context} 1›) done ML ‹ extuni_dec_n @{context} 2; › (*NUM667^1, node 202*) lemma "∀SV9 SV10 SV11. ((((SV9 = SV11) = (NUM667_1_bnd_x = NUM667_1_bnd_y)) = False ∨ NUM667_1_bnd_less SV11 SV10 = False) ∨ NUM667_1_bnd_less SV9 SV10 = True) ∨ NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y = True ==> ∀SV10 SV9 SV11. ((((SV11 = NUM667_1_bnd_x) = False ∨ (SV9 = NUM667_1_bnd_y) = False) ∨ NUM667_1_bnd_less SV11 SV10 = False) ∨ NUM667_1_bnd_less SV9 SV10 = True) ∨ NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y = True" apply (tactic ‹strip_qtfrs_tac @{context}›) apply (tactic ‹break_hypotheses 1›) apply (tactic ‹ALLGOALS (TRY o clause_breaker)›) apply (tactic ‹extuni_dec_tac @{context} 1›) done (*NUM667^1 node 141*) (* lemma "((bnd_x = bnd_x) = False ∨ (bnd_y = bnd_z) = False) ∨ bnd_less bnd_x bnd_y = True ==> (bnd_y = bnd_z) = False ∨ bnd_less bnd_x bnd_y = True" apply (tactic {*strip_qtfrs*}) apply (tactic {*break_hypotheses 1*}) apply (tactic {*ALLGOALS (TRY o clause_breaker)*}) apply (erule extuni_triv) done *) ML ‹ fun full_extcnf_combined_tac ctxt = extcnf_combined_tac ctxt NONE [ConstsDiff, StripQuantifiers, Flip_Conclusion, Loop [ Close_Branch, ConjI, King_Cong, Break_Hypotheses, Existential_Free, Existential_Var, Universal, RemoveRedundantQuantifications], CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates], AbsorbSkolemDefs] [] › ML ‹ fun nonfull_extcnf_combined_tac ctxt feats = extcnf_combined_tac ctxt NONE [ConstsDiff, StripQuantifiers, InnerLoopOnce (Break_Hypotheses :: feats), AbsorbSkolemDefs] [] › consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind lemma "∀SV2. (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False ==> (SEU882_5_bnd_sK1_Xy = SEU882_5_bnd_sK1_Xy) = False" (* apply (erule_tac x = "(@X. False)" in allE) *) (* apply (tactic {*remove_redundant_quantification 1*}) *) (* apply assumption *) by (tactic ‹nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications (*NUM667^1*) (* (* (Annotated_step ("153", "extuni_triv"), *) lemma "((bnd_y = bnd_x) = False ∨ (bnd_z = bnd_z) = False) ∨ (bnd_y = bnd_z) = True ==> (bnd_y = bnd_x) = False ∨ (bnd_y = bnd_z) = True" apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*}) done (* (Annotated_step ("162", "extuni_triv"), *) lemma "((bnd_y = bnd_x) = False ∨ (bnd_z = bnd_z) = False) ∨ bnd_less bnd_y bnd_z = True ==> (bnd_y = bnd_x) = False ∨ bnd_less bnd_y bnd_z = True" apply (tactic {*nonfull_extcnf_combined_tac [Extuni_Triv]*}) done *) (* SEU602^2 *) consts SEU602_2_bnd_sK7_E :: "(TPTP_Interpret.ind ==> bool) ==> TPTP_Interpret.ind" SEU602_2_bnd_sK2_SY17 :: TPTP_Interpret.ind SEU602_2_bnd_in :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" (* (Annotated_step ("113", "extuni_func"), *) lemma "∀SV49::TPTP_Interpret.ind ==> bool. (SV49 = (λSY23::TPTP_Interpret.ind. ¬ SEU602_2_bnd_in SY23 SEU602_2_bnd_sK2_SY17)) = False ==> ∀SV49::TPTP_Interpret.ind ==> bool. (SV49 (SEU602_2_bnd_sK7_E SV49) = (¬ SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) = False" (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error si by (tactic ‹nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]› consts SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind ==> bool) ==> TPTP_Interpret.ind" SEV405_5_bnd_cA :: bool lemma "∀SV1::TPTP_Interpret.ind ==> bool. (∀SY2::TPTP_Interpret.ind. ¬ (¬ (¬ SV1 SY2 ∨ SEV405_5_bnd_cA) ∨ ¬ (¬ SEV405_5_bnd_cA ∨ SV1 SY2))) = False ==> ∀SV1::TPTP_Interpret.ind ==> bool. (¬ (¬ (¬ SV1 (SEV405_5_bnd_sK1_SY2 SV1) ∨ SEV405_5_bnd_cA) ∨ ¬ (¬ SEV405_5_bnd_cA ∨ SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) = False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) (* strip quantifiers -- creating a space of permutations; from shallowest to deepes flip the conclusion -- giving us branch apply some collection of rules, in some order, until the space has been explored *) consts SEU581_2_bnd_sK1 :: "TPTP_Interpret.ind" SEU581_2_bnd_sK2 :: "TPTP_Interpret.ind ==> bool" SEU581_2_bnd_subset :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> HOL.bool" SEU581_2_bnd_dsetconstr :: "TPTP_Interpret.ind ==> (TPTP_Interpret.ind ==> HOL.boo (*testing parameters*) lemma "! X :: TPTP_Interpret.ind . (∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerse \ by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "(A & B) = True ==> (A | B) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "(¬ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True ==> (bnd_su by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing goals with parameters*) lemma "(¬ bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True ==> ! X. (b by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "(A & B) = True ==> (B & A) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) (*appreciating differences between THEN, REPEAT, and APPEND*) lemma "A & B ==> B & A" apply (tactic ‹ TRY (etac @{thm conjE} 1) THEN TRY (rtac @{thm conjI} 1)›) by assumption+ lemma "A & B ==> B & A" by (tactic ‹ etac @{thm conjE} 1 THEN rtac @{thm conjI} 1 THEN REPEAT (atac 1)›) lemma "A & B ==> B & A" apply (tactic ‹ rtac @{thm conjI} 1 APPEND etac @{thm conjE} 1›) back by assumption+ consts SEU581_2_bnd_sK3 :: "TPTP_Interpret.ind" SEU581_2_bnd_sK4 :: "TPTP_Interpret.ind" SEU581_2_bnd_sK5 :: "(TPTP_Interpret.ind ==> bool) ==> TPTP_Interpret.ind" SEU581_2_bnd_powerset :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" SEU581_2_bnd_in :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" consts bnd_c1 :: TPTP_Interpret.ind bnd_s :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" lemma "(∀SX0. (¬ (¬ SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) ∨ ¬ (¬ SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0))) (PUZ114_5_bnd_sK5 SX0) ∨ ¬ SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0)) (bnd_s (PUZ114_5_bnd_sK5 SX0)))) ∨ ¬ SX0 bnd_c1 bnd_c1) ∨ SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) = True ==> ∀SV1. ((¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1))) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1)) (bnd_s (PUZ114_5_bnd_sK5 SV1)))) ∨ ¬ SV1 bnd_c1 bnd_c1) ∨ SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "(¬ SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_ by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing repeated application of simulator*) lemma "(¬ ¬ False) = True ==> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) False = True ∨ False = True ∨ False = True" by (tactic ‹full_extcnf_combined_tac @{context}›) (*Testing non-normal conclusion. Ideally we should be able to apply the tactic to arbitrary chains of extcnf steps -- where it's not generally the case that the conclusions are normal.*) lemma "(¬ ¬ False) = True ==> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) (¬ False) = False" by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing repeated application of simulator, involving different extcnf rules*) lemma "(¬ ¬ (False | False)) = True ==> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) False = True ∨ False = True ∨ False = True" by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing logical expansion*) lemma "(∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ⟶ SEU581_2_bnd_subset B \ by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing extcnf_forall_pos*) lemma "(∀A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_p SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "((∀A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_ \ by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing parameters*) lemma "(∀A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) ⟶ SEU581_2_bnd_subset B \ by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "((? A .P1 A) = False) | P2 = True ==> !X. ((P1 X) = False | P2 = True)" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) ==> !X. (P1a X = True | P1b by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = T by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = T by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) ==> ! Y. (!X. (P1a X = T by (tactic ‹full_extcnf_combined_tac @{context}›) consts dud_bnd_s :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" (*this lemma kills blast*) lemma "(¬ (∀SX0 SX1. ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SX0)) SX1) ∨ ¬ (∀SX0 SX1. ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) = False ==> (¬ (∀SX0 SX1. ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) = False" by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing logical expansion -- this should be done by blast*) lemma "(∀A B. bnd_in B (bnd_powerset A) ⟶ SEU581_2_bnd_subset B A) = True \ by (tactic ‹full_extcnf_combined_tac @{context}›) (*testing related to PUZ114^5.p.out*) lemma "∀SV1. ((¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1))) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1)) (bnd_s (PUZ114_5_bnd_sK5 SV1))))) = True ∨ (¬ SV1 bnd_c1 bnd_c1) = True) ∨ SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True ==> ∀SV1. (SV1 bnd_c1 bnd_c1 = False ∨ (¬ (¬ SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ (¬ SV1 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SV1))) (PUZ114_5_bnd_sK5 SV1) ∨ ¬ SV1 (bnd_s (PUZ114_5_bnd_sK4 SV1)) (bnd_s (PUZ114_5_bnd_sK5 SV1))))) = True) ∨ SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "∀SV2. (∀SY41. ¬ PUZ114_5_bnd_sK3 SV2 SY41 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SY41) = True ==> ∀SV4 SV2. (¬ PUZ114_5_bnd_sK3 SV2 SV4 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) lemma "∀SV3. (∀SY42. ¬ PUZ114_5_bnd_sK3 SV3 SY42 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SY42)) = True ==> ∀SV5 SV3. (¬ PUZ114_5_bnd_sK3 SV3 SV5 ∨ PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) = True" by (tactic ‹full_extcnf_combined_tac @{context}›) subsection "unfold_def" (* (Annotated_step ("9", "unfold_def"), *) lemma "bnd_kpairiskpair = (ALL Xx Xy. bnd_iskpair (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) & bnd_kpair = (%Xx Xy. bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset)) & bnd_iskpair = (%A. EX Xx. bnd_in Xx (bnd_setunion A) & (EX Xy. bnd_in Xy (bnd_setunion A) & A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) & (~ (ALL SY0 SY1. EX SY3. bnd_in SY3 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) & (EX SY4. bnd_in SY4 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) & bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset)) bnd_emptyset)))) = True ==> (~ (ALL SX0 SX1. ~ (ALL SX2. ~ ~ (~ bnd_in SX2 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset ~ ~ (ALL SX3. ~ ~ (~ bnd_in SX3 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) | bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset) ~= bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset)) bnd_emptyset))))))) = True" by (tactic ‹unfold_def_tac @{context} []›) (* (Annotated_step ("10", "unfold_def"), *) lemma "bnd_kpairiskpair = (ALL Xx Xy. bnd_iskpair (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) & bnd_kpair = (%Xx Xy. bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset)) & bnd_iskpair = (%A. EX Xx. bnd_in Xx (bnd_setunion A) & (EX Xy. bnd_in Xy (bnd_setunion A) & A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) & (ALL SY5 SY6. EX SY7. bnd_in SY7 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) & (EX SY8. bnd_in SY8 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) & bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset)) bnd_emptyset))) = True ==> (ALL SX0 SX1. ~ (ALL SX2. ~ ~ (~ bnd_in SX2 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) | ~ ~ (ALL SX3. ~ ~ (~ bnd_in SX3 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))) | bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset) ~= bnd_setadjoin (bnd_setadjoin SX2 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset)) bnd_emptyset)))))) = True" by (tactic ‹unfold_def_tac @{context} []›) (* (Annotated_step ("12", "unfold_def"), *) lemma "bnd_cCKB6_BLACK = (λXu Xv. ∀Xw. Xw bnd_c1 bnd_c1 ∧ (∀Xj Xk. Xw Xj Xk ⟶ Xw (bnd_s (bnd_s Xj)) Xk ∧ Xw (bnd_s Xj) (bnd_s Xk)) ⟶ Xw Xu Xv) ∧ ((((∀SY36 SY37. ¬ PUZ114_5_bnd_sK3 SY36 SY37 ∨ PUZ114_5_bnd_sK3 (bnd_s (bnd_s SY36)) SY37) ∧ (∀SY38 SY39. ¬ PUZ114_5_bnd_sK3 SY38 SY39 ∨ PUZ114_5_bnd_sK3 (bnd_s SY38) (bnd_s SY39))) ∧ PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) ∧ ¬ PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1))) (bnd_s PUZ114_5_bnd_sK2)) = True ==> (¬ (¬ ¬ (¬ ¬ (¬ (∀SX0 SX1. ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (bnd_s (bnd_s SX0)) SX1) ∨ ¬ (∀SX0 SX1. ¬ PUZ114_5_bnd_sK3 SX0 SX1 ∨ PUZ114_5_bnd_sK3 (bnd_s SX0) (bnd_s SX1))) ∨ ¬ PUZ114_5_bnd_sK3 bnd_c1 bnd_c1) ∨ ¬ ¬ PUZ114_5_bnd_sK3 (bnd_s (bnd_s (bnd_s PUZ114_5_bnd_sK1))) (bnd_s PUZ114_5_bnd_sK2))) = True" (* apply (erule conjE)+ apply (erule subst)+ apply (tactic {*log_expander 1*})+ apply (rule refl) *) by (tactic ‹unfold_def_tac @{context} []›) (* (Annotated_step ("13", "unfold_def"), *) lemma "bnd_cCKB6_BLACK = (λXu Xv. ∀Xw. Xw bnd_c1 bnd_c1 ∧ (∀Xj Xk. Xw Xj Xk ⟶ Xw (bnd_s (bnd_s Xj)) Xk ∧ Xw (bnd_s Xj) (bnd_s Xk)) ⟶ Xw Xu Xv) ∧ (∀SY30. (SY30 (PUZ114_5_bnd_sK4 SY30) (PUZ114_5_bnd_sK5 SY30) ∧ (¬ SY30 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SY30))) (PUZ114_5_bnd_sK5 SY30) ∨ ¬ SY30 (bnd_s (PUZ114_5_bnd_sK4 SY30)) (bnd_s (PUZ114_5_bnd_sK5 SY30))) ∨ ¬ SY30 bnd_c1 bnd_c1) ∨ SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) = True ==> (∀SX0. (¬ (¬ SX0 (PUZ114_5_bnd_sK4 SX0) (PUZ114_5_bnd_sK5 SX0) ∨ ¬ (¬ SX0 (bnd_s (bnd_s (PUZ114_5_bnd_sK4 SX0))) (PUZ114_5_bnd_sK5 SX0) ∨ ¬ SX0 (bnd_s (PUZ114_5_bnd_sK4 SX0)) (bnd_s (PUZ114_5_bnd_sK5 SX0)))) ∨ ¬ SX0 bnd_c1 bnd_c1) ∨ SX0 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) = True" (* apply (erule conjE)+ apply (tactic {*expander_animal 1*})+ apply assumption *) by (tactic ‹unfold_def_tac @{context} []›) (*FIXME move this heuristic elsewhere*) ML ‹ (*Other than the list (which must not be empty) this function expects a parameter indicating the smallest integer. (Using Int.minInt isn't always viable).*) fun max_int_floored min l = if null l then raise List.Empty else fold (curry Int.max) l min; val _ = @{assert} (max_int_floored ~101002 [1] = 1) val _ = @{assert} (max_int_floored 0 [1, 3, 5] = 5) fun max_index_floored min l = let val max = max_int_floored min l in find_index (pair max #> (=)) l end › ML ‹ max_index_floored 0 [1, 3, 5] › ML ‹ (* Given argument ([h_1, ..., h_n], conc), obtained from term of form h_1 ==> ... ==> h_n ==> conclusion, this function indicates which h_i is biggest, or NONE if h_n = 0. *) fun biggest_hypothesis (hypos, _) = if null hypos then NONE else map size_of_term hypos |> max_index_floored 0 |> SOME › ML ‹ fun biggest_hyp_first_tac i = fn st => let val results = TERMFUN biggest_hypothesis (SOME i) st in if null results then no_tac st else let val result = the_single results in case result of NONE => no_tac st | SOME n => if n > 0 then rotate_tac n i st else no_tac st end end › (* (Annotated_step ("6", "unfold_def"), *) lemma "(¬ (∃U :: TPTP_Interpret.ind ==> bool. ∀V. U V = SEV405_5_bnd_cA)) = True (¬ ¬ (∀SX0 :: TPTP_Interpret.ind ==> bool. ¬ (∀SX1. ¬ (¬ (¬ SX0 SX1 ∨ SEV405_5_b ¬ (¬ SEV405_5_bnd_cA ∨ SX0 SX1))))) = True" (* by (tactic {*unfold_def_tac []*}) *) oops subsection "Using leo2_tac" (*these require PUZ114^5's proof to be loaded ML {*leo2_tac @{context} (hd prob_names) "50"*} ML {*leo2_tac @{context} (hd prob_names) "4"*} ML {*leo2_tac @{context} (hd prob_names) "9"*} (* (Annotated_step ("9", "extcnf_combined"), *) lemma "(∀SY30. SY30 bnd_c1 bnd_c1 ∧ (∀Xj Xk. SY30 Xj Xk ⟶ SY30 (bnd_s (bnd_s Xj)) Xk ∧ SY30 (bnd_s Xj) (bnd_s Xk)) ⟶ SY30 bnd_sK1 bnd_sK2) = True ==> (∀SY30. (SY30 (bnd_sK4 SY30) (bnd_sK5 SY30) ∧ (¬ SY30 (bnd_s (bnd_s (bnd_sK4 SY30))) (bnd_sK5 SY30) ∨ ¬ SY30 (bnd_s (bnd_sK4 SY30)) (bnd_s (bnd_sK5 SY30))) ∨ ¬ SY30 bnd_c1 bnd_c1) ∨ SY30 bnd_sK1 bnd_sK2) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*}) *) typedecl GEG007_1_bnd_reg consts GEG007_1_bnd_sK7_SX2 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> GEG007_1_bn GEG007_1_bnd_sK6_SX2 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> GEG007_1_bn GEG007_1_bnd_a :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" GEG007_1_bnd_catalunya :: "GEG007_1_bnd_reg" GEG007_1_bnd_spain :: "GEG007_1_bnd_reg" GEG007_1_bnd_c :: "GEG007_1_bnd_reg ==> GEG007_1_bnd_reg ==> bool" (* (Annotated_step ("147", "extcnf_forall_neg"), *) lemma "∀SV13 SV6. (∀SX2. ¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_spain ∨ GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya) = False ∨ GEG007_1_bnd_a SV6 SV13 = False ==> ∀SV6 SV13. (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_spain ∨ GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) = False ∨ GEG007_1_bnd_a SV6 SV13 = False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) (* (Annotated_step ("116", "extcnf_forall_neg"), *) lemma "∀SV13 SV6. (∀SX2. ¬ ¬ (¬ ¬ (¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_catalunya ∨ ¬ ¬ ¬ (∀SX3. ¬ ¬ (¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 SX2) ∨ ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)))) ∨ ¬ ¬ (¬ GEG007_1_bnd_c SX2 GEG007_1_bnd_spain ∨ ¬ ¬ ¬ (∀SX3. ¬ ¬ (¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 SX2) ∨ ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SX3 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) = False ∨ GEG007_1_bnd_a SV6 SV13 = False ==> ∀SV6 SV13. (¬ ¬ (¬ ¬ (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6) GEG007_1_bnd_catalunya ∨ ¬ ¬ ¬ (∀SY68. ¬ ¬ (¬ (∀SY69. ¬ GEG007_1_bnd_c SY69 SY68 ∨ GEG007_1_bnd_c SY69 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) ∨ ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SY68 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_catalunya)) ¬ ¬ (¬ GEG007_1_bnd_c (GEG007_1_bnd_sK6_SX2 SV13 SV6) GEG007_1_bnd_spain ∨ ¬ ¬ ¬ (∀SY71. ¬ ¬ (¬ (∀SY72. ¬ GEG007_1_bnd_c SY72 SY71 ∨ GEG007_1_bnd_c SY72 (GEG007_1_bnd_sK6_SX2 SV13 SV6)) ∨ ¬ (∀SX4. ¬ GEG007_1_bnd_c SX4 SY71 ∨ GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) False ∨ GEG007_1_bnd_a SV6 SV13 = False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) consts PUZ107_5_bnd_sK1_SX0 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" lemma "∀(SV4::TPTP_Interpret.ind) (SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind) (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind. ((SV1 ≠ SV3) = False ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨ PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False ==> \ (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind) (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind. ((SV1 = SV3) = True ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨ PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Not_neg]›) lemma " \ (SV4::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind) (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind. ((SV1 ≠ SV3 ∨ SV2 ≠ SV4) = False ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨ PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False ==> \ (SV6::TPTP_Interpret.ind) (SV2::TPTP_Interpret.ind) (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind. ((SV1 ≠ SV3) = False ∨ PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) ∨ PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Or_neg]›) consts NUM016_5_bnd_a :: TPTP_Interpret.ind NUM016_5_bnd_prime :: "TPTP_Interpret.ind ==> bool" NUM016_5_bnd_factorial_plus_one :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" NUM016_5_bnd_prime_divisor :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind" NUM016_5_bnd_divides :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" NUM016_5_bnd_less :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" (* (Annotated_step ("6", "unfold_def"), *) lemma "((((((((((((∀X::TPTP_Interpret.ind. ¬ NUM016_5_bnd_less X X) ∧ (∀(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind. ¬ NUM016_5_bnd_less X Y ∨ ¬ NUM016_5_bnd_less Y X)) ∧ (∀X::TPTP_Interpret.ind. NUM016_5_bnd_divides X X)) ∧ (∀(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind) Z::TPTP_Interpret.ind. (¬ NUM016_5_bnd_divides X Y ∨ ¬ NUM016_5_bnd_divides Y Z) ∨ NUM016_5_bnd_divides X Z)) ∧ (∀(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind. ¬ NUM016_5_bnd_divides X Y ∨ ¬ NUM016_5_bnd_less Y X)) ∧ (∀X::TPTP_Interpret.ind. NUM016_5_bnd_less X (NUM016_5_bnd_factorial_plus_one X))) ∧ (∀(X::TPTP_Interpret.ind) Y::TPTP_Interpret.ind. ¬ NUM016_5_bnd_divides X (NUM016_5_bnd_factorial_plus_one Y) ∨ NUM016_5_bnd_less Y X)) ∧ (∀X::TPTP_Interpret.ind. NUM016_5_bnd_prime X ∨ NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor X) X)) ∧ (∀X::TPTP_Interpret.ind. NUM016_5_bnd_prime X ∨ NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor X))) ∧ (∀X::TPTP_Interpret.ind. NUM016_5_bnd_prime X ∨ NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor X) X)) ∧ NUM016_5_bnd_prime NUM016_5_bnd_a) ∧ (∀X::TPTP_Interpret.ind. (¬ NUM016_5_bnd_prime X ∨ ¬ NUM016_5_bnd_less NUM016_5_bnd_a X) ∨ NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) X)) = True ==> (¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ ¬ (¬ (∀SX0::TPTP_Interpret.in ¬ NUM016_5_bnd_less SX0 SX0) ∨ ¬ (∀(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind. ¬ NUM016_5_bnd_less SX0 SX1 ∨ ¬ NUM016_5_bnd_less SX1 SX0)) ∨ ¬ (∀SX0::TPTP_Interpret.ind. NUM016_5_bnd_divides SX0 SX0)) ∨ ¬ (∀(SX0::TPTP_Interpret.ind) (SX1::TPTP_Interpret.ind) SX2::TPTP_Interpret.ind. (¬ NUM016_5_bnd_divides SX0 SX1 ∨ ¬ NUM016_5_bnd_divides SX1 SX2) ∨ NUM016_5_bnd_divides SX0 SX2)) ∨ ¬ (∀(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind. ¬ NUM016_5_bnd_divides SX0 SX1 ∨ ¬ NUM016_5_bnd_less SX1 SX0)) ∨ ¬ (∀SX0::TPTP_Interpret.ind. NUM016_5_bnd_less SX0 (NUM016_5_bnd_factorial_plus_one SX0))) ∨ ¬ (∀(SX0::TPTP_Interpret.ind) SX1::TPTP_Interpret.ind. ¬ NUM016_5_bnd_divides SX0 (NUM016_5_bnd_factorial_plus_one SX1) ∨ NUM016_5_bnd_less SX1 SX0)) ∨ ¬ (∀SX0::TPTP_Interpret.ind. NUM016_5_bnd_prime SX0 ∨ NUM016_5_bnd_divides (NUM016_5_bnd_prime_divisor SX0) SX0)) ∨ ¬ (∀SX0::TPTP_Interpret.ind. NUM016_5_bnd_prime SX0 ∨ NUM016_5_bnd_prime (NUM016_5_bnd_prime_divisor SX0))) ∨ ¬ (∀SX0::TPTP_Interpret.ind. NUM016_5_bnd_prime SX0 ∨ NUM016_5_bnd_less (NUM016_5_bnd_prime_divisor SX0) SX0)) ∨ ¬ NUM016_5_bnd_prime NUM016_5_bnd_a) ∨ ¬ (∀SX0::TPTP_Interpret.ind. (¬ NUM016_5_bnd_prime SX0 ∨ ¬ NUM016_5_bnd_less NUM016_5_bnd_a SX0) ∨ NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a) SX0))) = True" by (tactic ‹unfold_def_tac @{context} []›) (* (Annotated_step ("3", "unfold_def"), *) lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) & (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) & (ALL X. bnd_divides X X)) & (ALL X Y Z. (~ bnd_divides X Y | ~ bnd_divides Y Z) | bnd_divides X Z)) & (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) & (ALL X. bnd_less X (bnd_factorial_plus_one X))) & (ALL X Y. ~ bnd_divides X (bnd_factorial_plus_one Y) | bnd_less Y X)) & (ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) & (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) & (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) & bnd_prime bnd_a) & (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) | bnd_less (bnd_factorial_plus_one bnd_a) X))) = False ==> (~ ((((((((((((ALL X. ~ bnd_less X X) & (ALL X Y. ~ bnd_less X Y | ~ bnd_less Y X)) & (ALL X. bnd_divides X X)) & (ALL X Y Z. (~ bnd_divides X Y | ~ bnd_divides Y Z) | bnd_divides X Z)) & (ALL X Y. ~ bnd_divides X Y | ~ bnd_less Y X)) & (ALL X. bnd_less X (bnd_factorial_plus_one X))) & (ALL X Y. ~ bnd_divides X (bnd_factorial_plus_one Y) | bnd_less Y X)) & (ALL X. bnd_prime X | bnd_divides (bnd_prime_divisor X) X)) & (ALL X. bnd_prime X | bnd_prime (bnd_prime_divisor X))) & (ALL X. bnd_prime X | bnd_less (bnd_prime_divisor X) X)) & bnd_prime bnd_a) & (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) | bnd_less (bnd_factorial_plus_one bnd_a) X))) = False" by (tactic ‹unfold_def_tac @{context} []›) (* SET062^6.p.out [[(Annotated_step ("3", "unfold_def"), *) lemma "(∀Z3. False ⟶ bnd_cA Z3) = False ==> (∀Z3. False ⟶ bnd_cA Z3) = False" by (tactic ‹unfold_def_tac @{context} []›) (* (* SEU559^2.p.out *) (* [[(Annotated_step ("3", "unfold_def"), *) lemma "bnd_subset = (λA B. ∀Xx. bnd_in Xx A ⟶ bnd_in Xx B) ∧ (∀A B. (∀Xx. bnd_in Xx A ⟶ bnd_in Xx B) ⟶ bnd_subset A B) = False ==> (∀SY0 SY1. (∀Xx. bnd_in Xx SY0 ⟶ bnd_in Xx SY1) ⟶ (∀SY5. bnd_in SY5 SY0 ⟶ bnd_in SY5 SY1)) = False" by (tactic {*unfold_def_tac [@{thm bnd_subset_def}]*}) (* SEU559^2.p.out [[(Annotated_step ("6", "unfold_def"), *) lemma "(¬ (∃Xx. ∀Xy. Xx ⟶ Xy)) = True ==> (¬ ¬ (∀SX0. ¬ (∀SX1. ¬ SX0 ∨ SX1))) = True" by (tactic {*unfold_def_tac []*}) (* SEU502^2.p.out [[(Annotated_step ("3", "unfold_def"), *) lemma "bnd_emptysetE = (∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ∧ (bnd_emptysetE ⟶ (∀Xx. bnd_in Xx bnd_emptyset ⟶ False)) = False ==> ((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶ (∀Xx. bnd_in Xx bnd_emptyset ⟶ False)) = False" by (tactic {*unfold_def_tac [@{thm bnd_emptysetE_def}]*}) *) typedecl AGT037_2_bnd_mu consts AGT037_2_bnd_sK1_SX0 :: TPTP_Interpret.ind AGT037_2_bnd_cola :: AGT037_2_bnd_mu AGT037_2_bnd_jan :: AGT037_2_bnd_mu AGT037_2_bnd_possibly_likes :: "AGT037_2_bnd_mu ==> AGT037_2_bnd_mu ==> TPTP_Inter AGT037_2_bnd_sK5_SY68 :: "TPTP_Interpret.ind ==> AGT037_2_bnd_mu ==> AGT037_2_bnd_mu ==> TPTP_Interpret.ind ==> TPTP_Interpret.ind" AGT037_2_bnd_likes :: "AGT037_2_bnd_mu ==> AGT037_2_bnd_mu ==> TPTP_Interpret.ind AGT037_2_bnd_very_much_likes :: "AGT037_2_bnd_mu ==> AGT037_2_bnd_mu ==> TPTP_Inte AGT037_2_bnd_a1 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" AGT037_2_bnd_a2 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" AGT037_2_bnd_a3 :: "TPTP_Interpret.ind ==> TPTP_Interpret.ind ==> bool" (*test that nullary skolem terms are OK*) (* (Annotated_step ("79", "extcnf_forall_neg"), *) lemma "(∀SX0::TPTP_Interpret.ind. AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola SX0) = False ==> AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_ False" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) (* (Annotated_step ("202", "extcnf_forall_neg"), *) lemma "∀(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu SV45::TPTP_Interpret.ind. ((((∀SY68::TPTP_Interpret.ind. ¬ AGT037_2_bnd_a1 SV45 SY68 ∨ AGT037_2_bnd_likes SV29 SV39 SY68) = False ∨ (¬ (∀SY69::TPTP_Interpret.ind. ¬ AGT037_2_bnd_a2 SV45 SY69 ∨ AGT037_2_bnd_likes SV29 SV39 SY69)) = True) ∨ AGT037_2_bnd_likes SV29 SV39 SV45 = False) ∨ AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) ∨ AGT037_2_bnd_a3 SV13 SV45 = False ==> ∀(SV29::AGT037_2_bnd_mu) (SV39::AGT037_2_bnd_mu) (SV13::TPTP_Interpret.ind) SV45::TPTP_Interpret.ind. ((((¬ AGT037_2_bnd_a1 SV45 (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45) ∨ AGT037_2_bnd_likes SV29 SV39 (AGT037_2_bnd_sK5_SY68 SV13 SV39 SV29 SV45)) = False ∨ (¬ (∀SY69::TPTP_Interpret.ind. ¬ AGT037_2_bnd_a2 SV45 SY69 ∨ AGT037_2_bnd_likes SV29 SV39 SY69)) = True) ∨ AGT037_2_bnd_likes SV29 SV39 SV45 = False) ∨ AGT037_2_bnd_very_much_likes SV29 SV39 SV45 = True) ∨ AGT037_2_bnd_a3 SV13 SV45 = False" (* apply (rule allI)+ apply (erule_tac x = "SV13" in allE) apply (erule_tac x = "SV39" in allE) apply (erule_tac x = "SV29" in allE) apply (erule_tac x = "SV45" in allE) apply (erule disjE)+ defer apply (tactic {*clause_breaker 1*})+ apply (drule_tac sk = "bnd_sK5_SY68 SV13 SV39 SV29 SV45" in leo2_skolemise) defer apply (tactic {*clause_breaker 1*}) apply (tactic {*nonfull_extcnf_combined_tac []*}) *) by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) (*(*NUM667^1*) lemma "∀SV12 SV13 SV14 SV9 SV10 SV11. ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False ∨ (SV14 = SV13) = False) ∨ bnd_less SV12 SV14 = False) ∨ bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False ==> \ ((((bnd_less SV12 SV13 = False ∨ bnd_less SV11 SV10 = False) ∨ (SV14 = SV13) = False) ∨ bnd_less SV12 SV14 = False) ∨ bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False" (* apply (tactic {* extcnf_combined_tac NONE [ConstsDiff, StripQuantifiers] []*}) *) (* apply (rule allI)+ apply (erule_tac x = "SV12" in allE) apply (erule_tac x = "SV13" in allE) apply (erule_tac x = "SV14" in allE) apply (erule_tac x = "SV9" in allE) apply (erule_tac x = "SV10" in allE) apply (erule_tac x = "SV11" in allE) *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "300") 1*}) (*NUM667^1 node 302 -- dec*) lemma "∀SV12 SV13 SV14 SV9 SV10 SV11. ((((bnd_less SV12 SV13 = bnd_less SV11 SV10) = False ∨ (SV14 = SV13) = False) ∨ bnd_less SV12 SV14 = False) ∨ bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False ==> ∀SV9 SV14 SV10 SV13 SV11 SV12. (((((SV12 = SV11) = False ∨ (SV13 = SV10) = False) ∨ (SV14 = SV13) = False) ∨ bnd_less SV12 SV14 = False) ∨ bnd_less SV9 SV10 = True) ∨ (SV9 = SV11) = False" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "302") 1*}) *) (* (*CSR122^2*) (* (Annotated_step ("23", "extuni_bool2"), *) lemma "(bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i) = False ==> bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True ∨ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i = True" (* apply (erule extuni_bool2) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "23") 1*}) (* (Annotated_step ("24", "extuni_bool1"), *) lemma "(bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i) = False ==> bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = False ∨ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i = False" (* apply (erule extuni_bool1) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "24") 1*}) (* (Annotated_step ("25", "extuni_bool2"), *) lemma "(bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i) = False ==> bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True ∨ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i = True" (* apply (erule extuni_bool2) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "25") 1*}) (* (Annotated_step ("26", "extuni_bool1"), *) lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_holdsDuring_THFTYPE_IiooI SV2 True) = False ==> ∀SV2. bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = False ∨ bnd_holdsDuring_THFTYPE_IiooI SV2 True = False" (* apply (rule allI, erule allE) *) (* apply (erule extuni_bool1) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "26") 1*}) (* (Annotated_step ("27", "extuni_bool2"), *) lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_holdsDuring_THFTYPE_IiooI SV2 True) = False ==> ∀SV2. bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True ∨ bnd_holdsDuring_THFTYPE_IiooI SV2 True = True" (* apply (rule allI, erule allE) *) (* apply (erule extuni_bool2) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "27") 1*}) (* (Annotated_step ("30", "extuni_bool1"), *) lemma "((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True) = False ==> (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = False ∨ True = False" (* apply (erule extuni_bool1) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "30") 1*}) (* (Annotated_step ("29", "extuni_bind"), *) lemma "(bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i = bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) = False ∨ ((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True) = False ==> ((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True) = False" (* apply (tactic {*break_hypotheses 1*}) *) (* apply (erule extuni_bind) *) (* apply (tactic {*clause_breaker 1*}) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "29") 1*}) (* (Annotated_step ("28", "extuni_dec"), *) lemma "∀SV2. (bnd_holdsDuring_THFTYPE_IiooI (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i) (¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = bnd_holdsDuring_THFTYPE_IiooI SV2 True) = False ==> ∀SV2. (bnd_lYearFn_THFTYPE_IiiI bnd_n2009_THFTYPE_i = SV2) = False ∨ ((¬ (¬ bnd_likes_THFTYPE_IiioI bnd_lMary_THFTYPE_i bnd_lBill_THFTYPE_i ∨ ¬ bnd_likes_THFTYPE_IiioI bnd_lSue_THFTYPE_i bnd_lBill_THFTYPE_i)) = True) = False" (* apply (rule allI) *) (* apply (erule_tac x = "SV2" in allE) *) (* apply (erule extuni_dec_2) *) (* done *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "28") 1*}) *) (* QUA002^1 (* [[(Annotated_step ("49", "extuni_dec"), *) lemma "((bnd_sK3_E = bnd_sK1_X1 ∨ bnd_sK3_E = bnd_sK2_X2) = (bnd_sK3_E = bnd_sK2_X2 ∨ bnd_sK3_E = bnd_sK1_X1)) = False ==> ((bnd_sK3_E = bnd_sK2_X2) = (bnd_sK3_E = bnd_sK2_X2)) = False ∨ ((bnd_sK3_E = bnd_sK1_X1) = (bnd_sK3_E = bnd_sK1_X1)) = False" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "49") 1*}) (* (Annotated_step ("20", "unfold_def"), *) lemma "(bnd_addition bnd_sK1_X1 bnd_sK2_X2 ≠ bnd_addition bnd_sK2_X2 bnd_sK1_X1) = True ==> (bnd_sup (λSX0::TPTP_Interpret.ind. SX0 = bnd_sK1_X1 ∨ SX0 = bnd_sK2_X2) ≠ bnd_sup (λSX0::TPTP_Interpret.ind. SX0 = bnd_sK2_X2 ∨ SX0 = bnd_sK1_X1)) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "20") 1*}) *) (* (*SEU620^2*) (* (Annotated_step ("11", "unfold_def"), *) lemma "bnd_kpairiskpair = (∀Xx Xy. bnd_iskpair (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) ∧ bnd_kpair = (λXx Xy. bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset)) ∧ bnd_iskpair = (λA. ∃Xx. bnd_in Xx (bnd_setunion A) ∧ (∃Xy. bnd_in Xy (bnd_setunion A) ∧ A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) ∧ (∀SY5 SY6. (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset) (bnd_setadjoin (bnd_setadjoin (bnd_sK3 SY6 SY5) (bnd_setadjoin (bnd_sK4 SY6 SY5) bnd_emptyset)) bnd_emptyset) ∧ bnd_in (bnd_sK4 SY6 SY5) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset)))) ∧ bnd_in (bnd_sK3 SY6 SY5) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset)))) = True ==> (∀SX0 SX1. ¬ (¬ ¬ (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset) ≠ bnd_setadjoin (bnd_setadjoin (bnd_sK3 SX1 SX0) bnd_emptyset) (bnd_setadjoin (bnd_setadjoin (bnd_sK3 SX1 SX0) (bnd_setadjoin (bnd_sK4 SX1 SX0) bnd_emptyset)) bnd_emptyset) ∨ ¬ bnd_in (bnd_sK4 SX1 SX0) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset)))) ∨ ¬ bnd_in (bnd_sK3 SX1 SX0) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SX0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SX0 (bnd_setadjoin SX1 bnd_emptyset)) bnd_emptyset))))) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*}) (* (Annotated_step ("3", "unfold_def"), *) lemma "bnd_kpairiskpair = (∀Xx Xy. bnd_iskpair (bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) ∧ bnd_kpair = (λXx Xy. bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset)) ∧ bnd_iskpair = (λA. ∃Xx. bnd_in Xx (bnd_setunion A) ∧ (∃Xy. bnd_in Xy (bnd_setunion A) ∧ A = bnd_setadjoin (bnd_setadjoin Xx bnd_emptyset) (bnd_setadjoin (bnd_setadjoin Xx (bnd_setadjoin Xy bnd_emptyset)) bnd_emptyset))) ∧ (bnd_kpairiskpair ⟶ (∀Xx Xy. bnd_iskpair (bnd_kpair Xx Xy))) = False ==> ((∀SY5 SY6. ∃SY7. bnd_in SY7 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) ∧ (∃SY8. bnd_in SY8 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) ∧ bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset)) bnd_emptyset))) ⟶ (∀SY0 SY1. ∃SY3. bnd_in SY3 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) ∧ (∃SY4. bnd_in SY4 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) ∧ bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset)) bnd_emptyset)))) = False" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "3") 1*}) (* (Annotated_step ("8", "extcnf_combined"), *) lemma "(∀SY5 SY6. ∃SY7. bnd_in SY7 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) ∧ (∃SY8. bnd_in SY8 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset))) ∧ bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY7 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY7 (bnd_setadjoin SY8 bnd_emptyset)) bnd_emptyset))) = True ==> (∀SY5 SY6. (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin (bnd_sK3 SY6 SY5) bnd_emptyset) (bnd_setadjoin (bnd_setadjoin (bnd_sK3 SY6 SY5) (bnd_setadjoin (bnd_sK4 SY6 SY5) bnd_emptyset)) bnd_emptyset) ∧ bnd_in (bnd_sK4 SY6 SY5) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset)))) ∧ bnd_in (bnd_sK3 SY6 SY5) (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY5 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY5 (bnd_setadjoin SY6 bnd_emptyset)) bnd_emptyset)))) = True" by (tactic {* HEADGOAL (extcnf_combined_tac Full false (hd prob_names)) *}) (* (Annotated_step ("7", "extcnf_combined"), *) lemma "(¬ (∀SY0 SY1. ∃SY3. bnd_in SY3 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) ∧ (∃SY4. bnd_in SY4 (bnd_setunion (bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset))) ∧ bnd_setadjoin (bnd_setadjoin SY0 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY0 (bnd_setadjoin SY1 bnd_emptyset)) bnd_emptyset) = bnd_setadjoin (bnd_setadjoin SY3 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY3 (bnd_setadjoin SY4 bnd_emptyset)) bnd_emptyset)))) = True ==> (∀SY24. (∀SY25. bnd_setadjoin (bnd_setadjoin bnd_sK1 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin bnd_sK1 (bnd_setadjoin bnd_sK2 bnd_emptyset)) bnd_emptyset) ≠ bnd_setadjoin (bnd_setadjoin SY24 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin SY24 (bnd_setadjoin SY25 bnd_emptyset)) bnd_emptyset) ∨ ¬ bnd_in SY25 (bnd_setunion (bnd_setadjoin (bnd_setadjoin bnd_sK1 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin bnd_sK1 (bnd_setadjoin bnd_sK2 bnd_emptyset)) bnd_emptyset)))) ∨ ¬ bnd_in SY24 (bnd_setunion (bnd_setadjoin (bnd_setadjoin bnd_sK1 bnd_emptyset) (bnd_setadjoin (bnd_setadjoin bnd_sK1 (bnd_setadjoin bnd_sK2 bnd_emptyset)) bnd_emptyset)))) = True" by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*}) *) (*PUZ081^2*) (* (* (Annotated_step ("9", "unfold_def"), *) lemma "bnd_says bnd_mel (¬ bnd_knave bnd_zoey ∧ ¬ bnd_knave bnd_mel) ==> bnd_says bnd_mel (¬ bnd_knave bnd_zoey ∧ ¬ bnd_knave bnd_mel) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "9") 1*}) (* (Annotated_step ("10", "unfold_def"), *) lemma "bnd_says bnd_zoey (bnd_knave bnd_mel) ==> bnd_says bnd_zoey (bnd_knave bnd_mel) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*}) (* (Annotated_step ("11", "unfold_def"), *) lemma "∀P S. bnd_knave P ∧ bnd_says P S ⟶ ¬ S ==> (∀P S. bnd_knave P ∧ bnd_says P S ⟶ ¬ S) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*}) (* (Annotated_step ("12", "unfold_def"), *) lemma "∀P S. bnd_knight P ∧ bnd_says P S ⟶ S ==> (∀P S. bnd_knight P ∧ bnd_says P S ⟶ S) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*}) (* (Annotated_step ("13", "unfold_def"), *) lemma "∀P. bnd_knight P ≠ bnd_knave P ==> (∀P. bnd_knight P ≠ bnd_knave P) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "13") 1*}) (* (Annotated_step ("15", "extcnf_combined"), *) lemma "(¬ (∃TZ TM. TZ bnd_zoey ∧ TM bnd_mel)) = True ==> ((∀TM. ¬ TM bnd_mel) ∨ (∀TZ. ¬ TZ bnd_zoey)) = True" by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*}) (* (Annotated_step ("18", "extcnf_combined"), *) lemma "(∀P. bnd_knight P ≠ bnd_knave P) = True ==> ((∀P. ¬ bnd_knave P ∨ ¬ bnd_knight P) ∧ (∀P. bnd_knave P ∨ bnd_knight P)) = True" by (tactic {*extcnf_combined_tac Full false (hd prob_names) 1*}) *) (* (*from SEU667^2.p.out*) (* (Annotated_step ("10", "unfold_def"), *) lemma "bnd_dpsetconstrSub = (∀A B Xphi. bnd_subset (bnd_dpsetconstr A B Xphi) (bnd_cartprod A B)) ∧ bnd_dpsetconstr = (λA B Xphi. bnd_dsetconstr (bnd_cartprod A B) (λXu. ∃Xx. bnd_in Xx A ∧ (∃Xy. (bnd_in Xy B ∧ Xphi Xx Xy) ∧ Xu = bnd_kpair Xx Xy))) ∧ bnd_breln = (λA B C. bnd_subset C (bnd_cartprod A B)) ∧ (¬ bnd_subset (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2) (λSY66. ∃SY67. bnd_in SY67 bnd_sK1 ∧ (∃SY68. (bnd_in SY68 bnd_sK2 ∧ bnd_sK3 SY67 SY68) ∧ SY66 = bnd_kpair SY67 SY68))) (bnd_cartprod bnd_sK1 bnd_sK2)) = True ==> (¬ bnd_subset (bnd_dsetconstr (bnd_cartprod bnd_sK1 bnd_sK2) (λSX0. ¬ (∀SX1. ¬ ¬ (¬ bnd_in SX1 bnd_sK1 ∨ ¬ ¬ (∀SX2. ¬ ¬ (¬ ¬ (¬ bnd_in SX2 bnd_sK2 ∨ ¬ bnd_sK3 SX1 SX2) ∨ SX0 ≠ bnd_kpair SX1 SX2)))))) (bnd_cartprod bnd_sK1 bnd_sK2)) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "10") 1*}) (* (Annotated_step ("11", "unfold_def"), *) lemma "bnd_dpsetconstrSub = (∀A B Xphi. bnd_subset (bnd_dpsetconstr A B Xphi) (bnd_cartprod A B)) ∧ bnd_dpsetconstr = (λA B Xphi. bnd_dsetconstr (bnd_cartprod A B) (λXu. ∃Xx. bnd_in Xx A ∧ (∃Xy. (bnd_in Xy B ∧ Xphi Xx Xy) ∧ Xu = bnd_kpair Xx Xy))) ∧ bnd_breln = (λA B C. bnd_subset C (bnd_cartprod A B)) ∧ (∀SY21 SY22 SY23. bnd_subset (bnd_dsetconstr (bnd_cartprod SY21 SY22) (λSY35. ∃SY36. bnd_in SY36 SY21 ∧ (∃SY37. (bnd_in SY37 SY22 ∧ SY23 SY36 SY37) ∧ SY35 = bnd_kpair SY36 SY37))) (bnd_cartprod SY21 SY22)) = True ==> (∀SX0 SX1 SX2. bnd_subset (bnd_dsetconstr (bnd_cartprod SX0 SX1) (λSX3. ¬ (∀SX4. ¬ ¬ (¬ bnd_in SX4 SX0 ∨ ¬ ¬ (∀SX5. ¬ ¬ (¬ ¬ (¬ bnd_in SX5 SX1 ∨ ¬ SX2 SX4 SX5) ∨ SX3 ≠ bnd_kpair SX4 SX5)))))) (bnd_cartprod SX0 SX1)) = True" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*}) *) (* (*from ALG001^5*) (* (Annotated_step ("4", "extcnf_forall_neg"), *) lemma "(∀(Xh1 :: bnd_g ==> bnd_b) (Xh2 :: bnd_b ==> bnd_a) (Xf1 :: bnd_g ==> bnd_ (∀Xx Xy. Xh1 (Xf1 Xx Xy) = Xf2 (Xh1 Xx) (Xh1 Xy)) ∧ (∀Xx Xy. Xh2 (Xf2 Xx Xy) = Xf3 (Xh2 Xx) (Xh2 Xy)) ⟶ (∀Xx Xy. Xh2 (Xh1 (Xf1 Xx Xy)) = Xf3 (Xh2 (Xh1 Xx)) (Xh2 (Xh1 Xy)))) = False ==> ((∀SY35 SY36. bnd_sK1 (bnd_sK3 SY35 SY36) = bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) ∧ (∀SY31 SY32. bnd_sK2 (bnd_sK4 SY31 SY32) = bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) ⟶ (∀SY39 SY40. bnd_sK2 (bnd_sK1 (bnd_sK3 SY39 SY40)) = bnd_sK5 (bnd_sK2 (bnd_sK1 SY39)) (bnd_sK2 (bnd_sK1 SY40)))) = False" by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "4") 1*}) *) (*SYN044^4*) (* declare [[ML_print_depth = 1400]] (* the_tactics *) *} (* (Annotated_step ("12", "unfold_def"), *) lemma "bnd_mor = (λ(X::TPTP_Interpret.ind ==> bool) (Y::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. X U ∨ Y U) ∧ bnd_mnot = (λ(X::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. ¬ X U) ∧ bnd_mimplies = (λU::TPTP_Interpret.ind ==> bool. bnd_mor (bnd_mnot U)) ∧ bnd_mbox_s4 = (λ(P::TPTP_Interpret.ind ==> bool) X::TPTP_Interpret.ind. ∀Y::TPTP_Interpret.ind. bnd_irel X Y ⟶ P Y) ∧ bnd_mand = (λ(X::TPTP_Interpret.ind ==> bool) (Y::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. X U ∧ Y U) ∧ bnd_ixor = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_inot (bnd_iequiv P Q)) ∧ bnd_ivalid = All ∧ bnd_itrue = (λW::TPTP_Interpret.ind. True) ∧ bnd_isatisfiable = Ex ∧ bnd_ior = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) ∧ bnd_inot = (λP::TPTP_Interpret.ind ==> bool. bnd_mnot (bnd_mbox_s4 P)) ∧ bnd_iinvalid = (λPhi::TPTP_Interpret.ind ==> bool. ∀W::TPTP_Interpret.ind. ¬ Phi W) ∧ bnd_iimplies = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) ∧ bnd_iimplied = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_iimplies Q P) ∧ bnd_ifalse = bnd_inot bnd_itrue ∧ bnd_iequiv = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) ∧ bnd_icountersatisfiable = (λPhi::TPTP_Interpret.ind ==> bool. ∃W::TPTP_Interpret.ind. ¬ Phi W) ∧ bnd_iatom = (λP::TPTP_Interpret.ind ==> bool. P) ∧ bnd_iand = bnd_mand ∧ (∀(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind) Z::TPTP_Interpret.ind. bnd_irel X Y ∧ bnd_irel Y Z ⟶ bnd_irel X Z) ==> (∀(X::TPTP_Interpret.ind) (Y::TPTP_Interpret.ind) Z::TPTP_Interpret.ind. bnd_irel X Y ∧ bnd_irel Y Z ⟶ bnd_irel X Z) = True" (* by (tactic {*tectoc @{context}*}) *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "12") 1*}) (* (Annotated_step ("11", "unfold_def"), *) lemma "bnd_mor = (λ(X::TPTP_Interpret.ind ==> bool) (Y::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. X U ∨ Y U) ∧ bnd_mnot = (λ(X::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. ¬ X U) ∧ bnd_mimplies = (λU::TPTP_Interpret.ind ==> bool. bnd_mor (bnd_mnot U)) ∧ bnd_mbox_s4 = (λ(P::TPTP_Interpret.ind ==> bool) X::TPTP_Interpret.ind. ∀Y::TPTP_Interpret.ind. bnd_irel X Y ⟶ P Y) ∧ bnd_mand = (λ(X::TPTP_Interpret.ind ==> bool) (Y::TPTP_Interpret.ind ==> bool) U::TPTP_Interpret.ind. X U ∧ Y U) ∧ bnd_ixor = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_inot (bnd_iequiv P Q)) ∧ bnd_ivalid = All ∧ bnd_itrue = (λW::TPTP_Interpret.ind. True) ∧ bnd_isatisfiable = Ex ∧ bnd_ior = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_mor (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) ∧ bnd_inot = (λP::TPTP_Interpret.ind ==> bool. bnd_mnot (bnd_mbox_s4 P)) ∧ bnd_iinvalid = (λPhi::TPTP_Interpret.ind ==> bool. ∀W::TPTP_Interpret.ind. ¬ Phi W) ∧ bnd_iimplies = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_mimplies (bnd_mbox_s4 P) (bnd_mbox_s4 Q)) ∧ bnd_iimplied = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_iimplies Q P) ∧ bnd_ifalse = bnd_inot bnd_itrue ∧ bnd_iequiv = (λ(P::TPTP_Interpret.ind ==> bool) Q::TPTP_Interpret.ind ==> bool. bnd_iand (bnd_iimplies P Q) (bnd_iimplies Q P)) ∧ bnd_icountersatisfiable = (λPhi::TPTP_Interpret.ind ==> bool. ∃W::TPTP_Interpret.ind. ¬ Phi W) ∧ bnd_iatom = (λP::TPTP_Interpret.ind ==> bool. P) ∧ bnd_iand = bnd_mand ∧ bnd_ivalid (bnd_iimplies (bnd_iatom bnd_q) (bnd_iatom bnd_r)) ==> (∀SY161::TPTP_Interpret.ind. ¬ (∀SY162::TPTP_Interpret.ind. bnd_irel SY161 SY162 ⟶ bnd_q SY162) ∨ (∀SY163::TPTP_Interpret.ind. bnd_irel SY161 SY163 ⟶ bnd_r SY163)) = True" (* by (tactic {*tectoc @{context}*}) *) by (tactic {*rtac (leo2_tac @{context} (hd prob_names) "11") 1*}) lemma " (∀SY136. ¬ (∀SY137. bnd_irel SY136 SY137 ⟶ bnd_r SY137) ∨ (∀SY138. bnd_irel SY136 SY138 ⟶ bnd_p SY138 ∧ bnd_q SY138)) = True ==> (∀SY136. bnd_irel SY136 (bnd_sK5 SY136) ∧ ¬ bnd_r (bnd_sK5 SY136) ∨ (∀SY138. ¬ bnd_irel SY136 SY138 ∨ bnd_p SY138) ∧ (∀SY138. ¬ bnd_irel SY136 SY138 ∨ bnd_q SY138)) = True" by (tactic {*HEADGOAL (extcnf_combined_tac Full false (hd prob_names))*}) *) (* (Annotated_step ("11", "extcnf_forall_neg"), *) lemma "∀SV1::TPTP_Interpret.ind ==> bool. (∀SY2::TPTP_Interpret.ind. ¬ (¬ (¬ SV1 SY2 ∨ SEV405_5_bnd_cA) ∨ ¬ (¬ SEV405_5_bnd_cA ∨ SV1 SY2))) = False ==> ∀SV1::TPTP_Interpret.ind ==> bool. (¬ (¬ (¬ SV1 (SEV405_5_bnd_sK1_SY2 SV1) ∨ SEV405_5_bnd_cA) ∨ ¬ (¬ SEV405_5_bnd_cA ∨ SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) = False" (* apply (tactic {*full_extcnf_combined_tac*}) *) by (tactic ‹nonfull_extcnf_combined_tac @{context} [Existential_Var]›) (* (Annotated_step ("13", "extcnf_forall_pos"), *) lemma "(∀SY31 SY32. bnd_sK2 (bnd_sK4 SY31 SY32) = bnd_sK5 (bnd_sK2 SY31) (bnd_sK2 SY32)) = True ==> ∀SV1. (∀SY42. bnd_sK2 (bnd_sK4 SV1 SY42) = bnd_sK5 (bnd_sK2 SV1) (bnd_sK2 SY42)) = True" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Universal]›) (* (Annotated_step ("14", "extcnf_forall_pos"), *) lemma "(∀SY35 SY36. bnd_sK1 (bnd_sK3 SY35 SY36) = bnd_sK4 (bnd_sK1 SY35) (bnd_sK1 SY36)) = True ==> ∀SV2. (∀SY43. bnd_sK1 (bnd_sK3 SV2 SY43) = bnd_sK4 (bnd_sK1 SV2) (bnd_sK1 SY43)) = True" by (tactic ‹nonfull_extcnf_combined_tac @{context} [Universal]›) (*from SYO198^5.p.out*) (* [[(Annotated_step ("11", "extcnf_forall_special_pos"), *) lemma "(∀SX0::bool ==> bool. ¬ ¬ (¬ SX0 bnd_sK1_Xx ∨ ¬ SX0 bnd_sK2_Xy)) = True ==> (¬ ¬ (¬ True ∨ ¬ True)) = True" apply (tactic ‹extcnf_forall_special_pos_tac 1›) done (* (Annotated_step ("13", "extcnf_forall_special_pos"), *) lemma "(∀SX0::bool ==> bool. ¬ ¬ (¬ SX0 bnd_sK1_Xx ∨ ¬ SX0 bnd_sK2_Xy)) = True ==> (¬ ¬ (¬ bnd_sK1_Xx ∨ ¬ bnd_sK2_Xy)) = True" apply (tactic ‹extcnf_forall_special_pos_tac 1›) done (* [[(Annotated_step ("8", "polarity_switch"), *) lemma "(∀(Xx::bool) (Xy::bool) Xz::bool. True ∧ True ⟶ True) = False ==> (¬ (∀(Xx::bool) (Xy::bool) Xz::bool. True ∧ True ⟶ True)) = True" apply (tactic ‹nonfull_extcnf_combined_tac @{context} [Polarity_switch]›) done lemma "((∀SY22 SY23 SY24. bnd_sK1_RRR SY22 SY23 ∧ bnd_sK1_RRR SY23 SY24 ⟶ bnd_sK1_RRR SY22 SY24) ∧ (∀SY25. (∀SY26. SY25 SY26 ⟶ bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) ∧ (∀SY27. (∀SY28. SY25 SY28 ⟶ bnd_sK1_RRR SY28 SY27) ⟶ bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) ⟶ (∀SY29. ∃SY30. ∀SY31. SY29 SY31 ⟶ bnd_sK1_RRR SY31 SY30)) = False ==> (∀SY25. (∀SY26. SY25 SY26 ⟶ bnd_sK1_RRR SY26 (bnd_sK2_U SY25)) ∧ (∀SY27. (∀SY28. SY25 SY28 ⟶ bnd_sK1_RRR SY28 SY27) ⟶ bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) = True" apply (tactic ‹standard_cnf_tac @{context} 1›) done lemma "((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶ (∀Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) ⟶ (∀A B. A = B ⟶ (∀Xx Xy. Xx = Xy ⟶ bnd_in Xx A = bnd_in Xy B)) ⟶ (∀SY0. bnd_in SY0 bnd_omega ⟶ bnd_setadjoin SY0 SY0 ≠ bnd_emptyset)) = False ==> (∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) = True" apply (tactic ‹standard_cnf_tac @{context} 1›) done lemma "((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶ (∀Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) ⟶ (∀A B. A = B ⟶ (∀Xx Xy. Xx = Xy ⟶ bnd_in Xx A = bnd_in Xy B)) ⟶ (∀SY0. bnd_in SY0 bnd_omega ⟶ bnd_setadjoin SY0 SY0 ≠ bnd_emptyset)) = False ==> (∀Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) = True" apply (tactic ‹standard_cnf_tac @{context} 1›) done lemma "((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶ (∀Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) ⟶ (∀A B. A = B ⟶ (∀Xx Xy. Xx = Xy ⟶ bnd_in Xx A = bnd_in Xy B)) ⟶ (∀SY0. bnd_in SY0 bnd_omega ⟶ bnd_setadjoin SY0 SY0 ≠ bnd_emptyset)) = False ==> (∀A B. A = B ⟶ (∀Xx Xy. Xx = Xy ⟶ bnd_in Xx A = bnd_in Xy B)) = True" apply (tactic ‹standard_cnf_tac @{context} 1›) done lemma "((∀Xx. bnd_in Xx bnd_emptyset ⟶ (∀Xphi. Xphi)) ⟶ (∀Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) ⟶ (∀A B. A = B ⟶ (∀Xx Xy. Xx = Xy ⟶ bnd_in Xx A = bnd_in Xy B)) ⟶ (∀SY0. bnd_in SY0 bnd_omega ⟶ bnd_setadjoin SY0 SY0 ≠ bnd_emptyset)) = False ==> (∀SY0. bnd_in SY0 bnd_omega ⟶ bnd_setadjoin SY0 SY0 ≠ bnd_emptyset) = False" apply (tactic ‹standard_cnf_tac @{context} 1›) done (*nested conjunctions*) lemma "((((∀Xx. bnd_cP bnd_e Xx = Xx) ∧ (∀Xy. bnd_cP Xy bnd_e = Xy)) ∧ (∀Xz. bnd_cP Xz Xz = bnd_e)) ∧ (∀Xx Xy Xz. bnd_cP (bnd_cP Xx Xy) Xz = bnd_cP Xx (bnd_cP Xy Xz)) ⟶ (∀Xa Xb. bnd_cP Xa Xb = bnd_cP Xb Xa)) = False ==> (∀Xx. bnd_cP bnd_e Xx = Xx) = True" apply (tactic ‹standard_cnf_tac @{context} 1›) done end
¤ Dauer der Verarbeitung: 0.88 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26