|
section \<open>Meson test cases\<close>
theory Meson_Test
imports Main
begin
text \<open>
WARNING: there are many potential conflicts between variables used
below and constants declared in HOL!
\<close>
hide_const (open) implies union inter subset quotient sum
text \<open>
Test data for the MESON proof procedure
(Excludes the equality problems 51, 52, 56, 58)
\<close>
subsection \<open>Interactive examples\<close>
lemma problem_25:
"(\x. P x) & (\x. L x --> ~ (M x & R x)) & (\x. P x --> (M x & L x)) & ((\x. P x --> Q x) | (\x. P x & R x)) --> (\x. Q x & P x)"
apply (rule ccontr)
ML_prf \<open>
val ctxt = \<^context>;
val prem25 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
val nnf25 = Meson.make_nnf ctxt prem25;
val xsko25 = Meson.skolemize ctxt nnf25;
\<close>
apply (tactic \<open>cut_tac xsko25 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>
val ctxt = \<^context>;
val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
val clauses25 = Meson.make_clauses ctxt [sko25]; (*7 clauses*)
val horns25 = Meson.make_horns clauses25; (*16 Horn clauses*)
val go25 :: _ = Meson.gocls clauses25;
val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go25 :: horns25)) ctxt;
Goal.prove ctxt' [] [] \<^prop>\False\ (fn _ =>
resolve_tac ctxt' [go25] 1 THEN
Meson.depth_prolog_tac ctxt' horns25);
\<close>
oops
lemma problem_26:
"((\x. p x) = (\x. q x)) & (\x. \y. p x & q y --> (r x = s y)) --> ((\x. p x --> r x) = (\x. q x --> s x))"
apply (rule ccontr)
ML_prf \<open>
val ctxt = \<^context>;
val prem26 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>
val nnf26 = Meson.make_nnf ctxt prem26;
val xsko26 = Meson.skolemize ctxt nnf26;
\<close>
apply (tactic \<open>cut_tac xsko26 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>
val ctxt = \<^context>;
val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
val clauses26 = Meson.make_clauses ctxt [sko26];
val _ = \<^assert> (length clauses26 = 9);
val horns26 = Meson.make_horns clauses26;
val _ = \<^assert> (length horns26 = 24);
val go26 :: _ = Meson.gocls clauses26;
val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go26 :: horns26)) ctxt;
Goal.prove ctxt' [] [] \<^prop>\False\ (fn _ =>
resolve_tac ctxt' [go26] 1 THEN
Meson.depth_prolog_tac ctxt' horns26); (*7 ms*)
(*Proof is of length 107!!*)
\<close>
oops
lemma problem_43: \<comment> \<open>NOW PROVED AUTOMATICALLY!!\<close> (*16 Horn clauses*)
"(\x. \y. q x y = (\z. p z x = (p z y::bool))) --> (\x. (\y. q x y = (q y x::bool)))"
apply (rule ccontr)
ML_prf \<open>
val ctxt = \<^context>;
val prem43 = Thm.assume \<^cprop>\<open>\<not> ?thesis\<close>;
val nnf43 = Meson.make_nnf ctxt prem43;
val xsko43 = Meson.skolemize ctxt nnf43;
\<close>
apply (tactic \<open>cut_tac xsko43 1 THEN REPEAT (eresolve_tac \<^context> [exE] 1)\<close>)
ML_val \<open>
val ctxt = \<^context>;
val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal})));
val clauses43 = Meson.make_clauses ctxt [sko43];
val _ = \<^assert> (length clauses43 = 6);
val horns43 = Meson.make_horns clauses43;
val _ = \<^assert> (length horns43 = 16);
val go43 :: _ = Meson.gocls clauses43;
val ctxt' = fold Thm.declare_hyps (maps Thm.chyps_of (go43 :: horns43)) ctxt;
Goal.prove ctxt' [] [] \<^prop>\False\ (fn _ =>
resolve_tac ctxt' [go43] 1 THEN
Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43); (*7ms*)
\<close>
oops
(*
#1 (q x xa ==> ~ q x xa) ==> q xa x
#2 (q xa x ==> ~ q xa x) ==> q x xa
#3 (~ q x xa ==> q x xa) ==> ~ q xa x
#4 (~ q xa x ==> q xa x) ==> ~ q x xa
#5 [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?U ==> p ?W ?U |] ==> p ?W ?V
#6 [| ~ p ?W ?U ==> p ?W ?U; p ?W ?V ==> ~ p ?W ?V |] ==> ~ q ?U ?V
#7 [| p ?W ?V ==> ~ p ?W ?V; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?U
#8 [| ~ q ?U ?V ==> q ?U ?V; ~ p ?W ?V ==> p ?W ?V |] ==> p ?W ?U
#9 [| ~ p ?W ?V ==> p ?W ?V; p ?W ?U ==> ~ p ?W ?U |] ==> ~ q ?U ?V
#10 [| p ?W ?U ==> ~ p ?W ?U; ~ q ?U ?V ==> q ?U ?V |] ==> ~ p ?W ?V
#11 [| p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U;
p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V |] ==> q ?U ?V
#12 [| p (xb ?U ?V) ?V ==> ~ p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
p (xb ?U ?V) ?U
#13 [| q ?U ?V ==> ~ q ?U ?V; p (xb ?U ?V) ?U ==> ~ p (xb ?U ?V) ?U |] ==>
p (xb ?U ?V) ?V
#14 [| ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U;
~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V |] ==> q ?U ?V
#15 [| ~ p (xb ?U ?V) ?V ==> p (xb ?U ?V) ?V; q ?U ?V ==> ~ q ?U ?V |] ==>
~ p (xb ?U ?V) ?U
#16 [| q ?U ?V ==> ~ q ?U ?V; ~ p (xb ?U ?V) ?U ==> p (xb ?U ?V) ?U |] ==>
~ p (xb ?U ?V) ?V
And here is the proof! (Unkn is the start state after use of goal clause)
[Unkn, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
Res ([Thm "#1"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
Asm 1, Res ([Thm "#13"], false, 1), Asm 1, Res ([Thm "#10"], false, 1),
Res ([Thm "#16"], false, 1), Asm 2, Asm 1, Res ([Thm "#1"], false, 1),
Asm 1, Res ([Thm "#14"], false, 1), Res ([Thm "#5"], false, 1),
Res ([Thm "#2"], false, 1), Asm 1, Res ([Thm "#13"], false, 1), Asm 2,
Asm 1, Res ([Thm "#8"], false, 1), Res ([Thm "#2"], false, 1), Asm 1,
Res ([Thm "#12"], false, 1), Asm 2, Asm 1] : lderiv list
*)
text \<open>
MORE and MUCH HARDER test data for the MESON proof procedure
(courtesy John Harrison).
\<close>
(* ========================================================================= *)
(* 100 problems selected from the TPTP library *)
(* ========================================================================= *)
(*
* Original timings for John Harrison's MESON_TAC.
* Timings below on a 600MHz Pentium III (perch)
* Some timings below refer to griffon, which is a dual 2.5GHz Power Mac G5.
*
* A few variable names have been changed to avoid clashing with constants.
*
* Changed numeric constants e.g. 0, 1, 2... to num0, num1, num2...
*
* Here's a list giving typical CPU times, as well as common names and
* literature references.
*
* BOO003-1 34.6 B2 part 1 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob2_part1.ver1.in [ANL]
* BOO004-1 36.7 B2 part 2 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob2_part2.ver1 [ANL]
* BOO005-1 47.4 B3 part 1 [McCharen, et al., 1976]; B5 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob3_part1.ver1.in [ANL]
* BOO006-1 48.4 B3 part 2 [McCharen, et al., 1976]; B6 [McCharen, et al., 1976]; Lemma proved [Overbeek, et al., 1976]; prob3_part2.ver1 [ANL]
* BOO011-1 19.0 B7 [McCharen, et al., 1976]; prob7.ver1 [ANL]
* CAT001-3 45.2 C1 [McCharen, et al., 1976]; p1.ver3.in [ANL]
* CAT003-3 10.5 C3 [McCharen, et al., 1976]; p3.ver3.in [ANL]
* CAT005-1 480.1 C5 [McCharen, et al., 1976]; p5.ver1.in [ANL]
* CAT007-1 11.9 C7 [McCharen, et al., 1976]; p7.ver1.in [ANL]
* CAT018-1 81.3 p18.ver1.in [ANL]
* COL001-2 16.0 C1 [Wos & McCune, 1988]
* COL023-1 5.1 [McCune & Wos, 1988]
* COL032-1 15.8 [McCune & Wos, 1988]
* COL052-2 13.2 bird4.ver2.in [ANL]
* COL075-2 116.9 [Jech, 1994]
* COM001-1 1.7 shortburst [Wilson & Minker, 1976]
* COM002-1 4.4 burstall [Wilson & Minker, 1976]
* COM002-2 7.4
* COM003-2 22.1 [Brushi, 1991]
* COM004-1 45.1
* GEO003-1 71.7 T3 [McCharen, et al., 1976]; t3.ver1.in [ANL]
* GEO017-2 78.8 D4.1 [Quaife, 1989]
* GEO027-3 181.5 D10.1 [Quaife, 1989]
* GEO058-2 104.0 R4 [Quaife, 1989]
* GEO079-1 2.4 GEOMETRY THEOREM [Slagle, 1967]
* GRP001-1 47.8 CADE-11 Competition 1 [Overbeek, 1990]; G1 [McCharen, et al., 1976]; THEOREM 1 [Lusk & McCune, 1993]; wos10 [Wilson & Minker, 1976]; xsquared.ver1.in [ANL]; [Robinson, 1963]
* GRP008-1 50.4 Problem 4 [Wos, 1965]; wos4 [Wilson & Minker, 1976]
* GRP013-1 40.2 Problem 11 [Wos, 1965]; wos11 [Wilson & Minker, 1976]
* GRP037-3 43.8 Problem 17 [Wos, 1965]; wos17 [Wilson & Minker, 1976]
* GRP031-2 3.2 ls23 [Lawrence & Starkey, 1974]; ls23 [Wilson & Minker, 1976]
* GRP034-4 2.5 ls26 [Lawrence & Starkey, 1974]; ls26 [Wilson & Minker, 1976]
* GRP047-2 11.7 [Veroff, 1992]
* GRP130-1 170.6 Bennett QG8 [TPTP]; QG8 [Slaney, 1993]
* GRP156-1 48.7 ax_mono1c [Schulz, 1995]
* GRP168-1 159.1 p01a [Schulz, 1995]
* HEN003-3 39.9 HP3 [McCharen, et al., 1976]
* HEN007-2 125.7 H7 [McCharen, et al., 1976]
* HEN008-4 62.0 H8 [McCharen, et al., 1976]
* HEN009-5 136.3 H9 [McCharen, et al., 1976]; hp9.ver3.in [ANL]
* HEN012-3 48.5 new.ver2.in [ANL]
* LCL010-1 370.9 EC-73 [McCune & Wos, 1992]; ec_yq.in [OTTER]
* LCL077-2 51.6 morgan.two.ver1.in [ANL]
* LCL082-1 14.6 IC-1.1 [Wos, et al., 1990]; IC-65 [McCune & Wos, 1992]; ls2 [SETHEO]; S1 [Pfenning, 1988]
* LCL111-1 585.6 CADE-11 Competition 6 [Overbeek, 1990]; mv25.in [OTTER]; MV-57 [McCune & ;Wos, 1992]; mv.in part 2 [OTTER]; ovb6 [SETHEO]; THEOREM 6 [Lusk & McCune, 1993]
* LCL143-1 10.9 Lattice structure theorem 2 [Bonacina, 1991]
* LCL182-1 271.6 Problem 2.16 [Whitehead & Russell, 1927]
* LCL200-1 12.0 Problem 2.46 [Whitehead & Russell, 1927]
* LCL215-1 214.4 Problem 2.62 [Whitehead & Russell, 1927]; Problem 2.63 [Whitehead & Russell, 1927]
* LCL230-2 0.2 Pelletier 5 [Pelletier, 1986]
* LDA003-1 68.5 Problem 3 [Jech, 1993]
* MSC002-1 9.2 DBABHP [Michie, et al., 1972]; DBABHP [Wilson & Minker, 1976]
* MSC003-1 3.2 HASPARTS-T1 [Wilson & Minker, 1976]
* MSC004-1 9.3 HASPARTS-T2 [Wilson & Minker, 1976]
* MSC005-1 1.8 Problem 5.1 [Plaisted, 1982]
* MSC006-1 39.0 nonob.lop [SETHEO]
* NUM001-1 14.0 Chang-Lee-10a [Chang, 1970]; ls28 [Lawrence & Starkey, 1974]; ls28 [Wilson & Minker, 1976]
* NUM021-1 52.3 ls65 [Lawrence & Starkey, 1974]; ls65 [Wilson & Minker, 1976]
* NUM024-1 64.6 ls75 [Lawrence & Starkey, 1974]; ls75 [Wilson & Minker, 1976]
* NUM180-1 621.2 LIM2.1 [Quaife]
* NUM228-1 575.9 TRECDEF4 cor. [Quaife]
* PLA002-1 37.4 Problem 5.7 [Plaisted, 1982]
* PLA006-1 7.2 [Segre & Elkan, 1994]
* PLA017-1 484.8 [Segre & Elkan, 1994]
* PLA022-1 19.1 [Segre & Elkan, 1994]
* PLA022-2 19.7 [Segre & Elkan, 1994]
* PRV001-1 10.3 PV1 [McCharen, et al., 1976]
* PRV003-1 3.9 E2 [McCharen, et al., 1976]; v2.lop [SETHEO]
* PRV005-1 4.3 E4 [McCharen, et al., 1976]; v4.lop [SETHEO]
* PRV006-1 6.0 E5 [McCharen, et al., 1976]; v5.lop [SETHEO]
* PRV009-1 2.2 Hoares FIND [Bledsoe, 1977]; Problem 5.5 [Plaisted, 1982]
* PUZ012-1 3.5 Boxes-of-fruit [Wos, 1988]; Boxes-of-fruit [Wos, et al., 1992]; boxes.ver1.in [ANL]
* PUZ020-1 56.6 knightknave.in [ANL]
* PUZ025-1 58.4 Problem 35 [Smullyan, 1978]; tandl35.ver1.in [ANL]
* PUZ029-1 5.1 pigs.ver1.in [ANL]
* RNG001-3 82.4 EX6-T? [Wilson & Minker, 1976]; ex6.lop [SETHEO]; Example 6a [Fleisig, et al., 1974]; FEX6T1 [SPRFN]; FEX6T2 [SPRFN]
* RNG001-5 399.8 Problem 21 [Wos, 1965]; wos21 [Wilson & Minker, 1976]
* RNG011-5 8.4 CADE-11 Competition Eq-10 [Overbeek, 1990]; PROBLEM 10 [Zhang, 1993]; THEOREM EQ-10 [Lusk & McCune, 1993]
* RNG023-6 9.1 [Stevens, 1987]
* RNG028-2 9.3 PROOF III [Anantharaman & Hsiang, 1990]
* RNG038-2 16.2 Problem 27 [Wos, 1965]; wos27 [Wilson & Minker, 1976]
* RNG040-2 180.5 Problem 29 [Wos, 1965]; wos29 [Wilson & Minker, 1976]
* RNG041-1 35.8 Problem 30 [Wos, 1965]; wos30 [Wilson & Minker, 1976]
* ROB010-1 205.0 Lemma 3.3 [Winker, 1990]; RA2 [Lusk & Wos, 1992]
* ROB013-1 23.6 Lemma 3.5 [Winker, 1990]
* ROB016-1 15.2 Corollary 3.7 [Winker, 1990]
* ROB021-1 230.4 [McCune, 1992]
* SET005-1 192.2 ls108 [Lawrence & Starkey, 1974]; ls108 [Wilson & Minker, 1976]
* SET009-1 10.5 ls116 [Lawrence & Starkey, 1974]; ls116 [Wilson & Minker, 1976]
* SET025-4 694.7 Lemma 10 [Boyer, et al, 1986]
* SET046-5 2.3 p42.in [ANL]; Pelletier 42 [Pelletier, 1986]
* SET047-5 3.7 p43.in [ANL]; Pelletier 43 [Pelletier, 1986]
* SYN034-1 2.8 QW [Michie, et al., 1972]; QW [Wilson & Minker, 1976]
* SYN071-1 1.9 Pelletier 48 [Pelletier, 1986]
* SYN349-1 61.7 Ch17N5 [Tammet, 1994]
* SYN352-1 5.5 Ch18N4 [Tammet, 1994]
* TOP001-2 61.1 Lemma 1a [Wick & McCune, 1989]
* TOP002-2 0.4 Lemma 1b [Wick & McCune, 1989]
* TOP004-1 181.6 Lemma 1d [Wick & McCune, 1989]
* TOP004-2 9.0 Lemma 1d [Wick & McCune, 1989]
* TOP005-2 139.8 Lemma 1e [Wick & McCune, 1989]
*)
abbreviation "EQU001_0_ax equal \ (\X. equal(X::'a,X)) &
(\<forall>Y X. equal(X::'a,Y) --> equal(Y::'a,X)) &
(\<forall>Y X Z. equal(X::'a,Y) & equal(Y::'a,Z) --> equal(X::'a,Z))"
abbreviation "BOO002_0_ax equal INVERSE multiplicative_identity
additive_identity multiply product add sum \<equiv>
(\<forall>X Y. sum(X::'a,Y,add(X::'a,Y))) &
(\<forall>X Y. product(X::'a,Y,multiply(X::'a,Y))) &
(\<forall>Y X Z. sum(X::'a,Y,Z) --> sum(Y::'a,X,Z)) &
(\<forall>Y X Z. product(X::'a,Y,Z) --> product(Y::'a,X,Z)) &
(\<forall>X. sum(additive_identity::'a,X,X)) &
(\<forall>X. sum(X::'a,additive_identity,X)) &
(\<forall>X. product(multiplicative_identity::'a,X,X)) &
(\<forall>X. product(X::'a,multiplicative_identity,X)) &
(\<forall>Y Z X V3 V1 V2 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & product(X::'a,V3,V4) --> sum(V1::'a,V2,V4)) &
(\<forall>Y Z V1 V2 X V3 V4. product(X::'a,Y,V1) & product(X::'a,Z,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(X::'a,V3,V4)) &
(\<forall>Y Z V3 X V1 V2 V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & product(V3::'a,X,V4) --> sum(V1::'a,V2,V4)) &
(\<forall>Y Z V1 V2 V3 X V4. product(Y::'a,X,V1) & product(Z::'a,X,V2) & sum(Y::'a,Z,V3) & sum(V1::'a,V2,V4) --> product(V3::'a,X,V4)) &
(\<forall>Y Z X V3 V1 V2 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & sum(X::'a,V3,V4) --> product(V1::'a,V2,V4)) &
(\<forall>Y Z V1 V2 X V3 V4. sum(X::'a,Y,V1) & sum(X::'a,Z,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(X::'a,V3,V4)) &
(\<forall>Y Z V3 X V1 V2 V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & sum(V3::'a,X,V4) --> product(V1::'a,V2,V4)) &
(\<forall>Y Z V1 V2 V3 X V4. sum(Y::'a,X,V1) & sum(Z::'a,X,V2) & product(Y::'a,Z,V3) & product(V1::'a,V2,V4) --> sum(V3::'a,X,V4)) &
(\<forall>X. sum(INVERSE(X),X,multiplicative_identity)) &
(\<forall>X. sum(X::'a,INVERSE(X),multiplicative_identity)) &
(\<forall>X. product(INVERSE(X),X,additive_identity)) &
(\<forall>X. product(X::'a,INVERSE(X),additive_identity)) &
(\<forall>X Y U V. sum(X::'a,Y,U) & sum(X::'a,Y,V) --> equal(U::'a,V)) &
(\<forall>X Y U V. product(X::'a,Y,U) & product(X::'a,Y,V) --> equal(U::'a,V))"
abbreviation "BOO002_0_eq INVERSE multiply add product sum equal \
(\<forall>X Y W Z. equal(X::'a,Y) & sum(X::'a,W,Z) --> sum(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & sum(W::'a,X,Z) --> sum(W::'a,Y,Z)) &
(\<forall>X W Z Y. equal(X::'a,Y) & sum(W::'a,Z,X) --> sum(W::'a,Z,Y)) &
(\<forall>X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) &
(\<forall>X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &
(\<forall>X Y W. equal(X::'a,Y) --> equal(add(X::'a,W),add(Y::'a,W))) &
(\<forall>X W Y. equal(X::'a,Y) --> equal(add(W::'a,X),add(W::'a,Y))) &
(\<forall>X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &
(\<forall>X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &
(\<forall>X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y)))"
(*51194 inferences so far. Searching to depth 13. 232.9 secs*)
lemma BOO003_1:
"EQU001_0_ax equal &
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~product(x::'a,x,x)) --> False"
by meson
(*51194 inferences so far. Searching to depth 13. 204.6 secs
Strange! The previous problem also has 51194 inferences at depth 13. They
must be very similar!*)
lemma BOO004_1:
"EQU001_0_ax equal &
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~sum(x::'a,x,x)) --> False"
by meson
(*74799 inferences so far. Searching to depth 13. 290.0 secs*)
lemma BOO005_1:
"EQU001_0_ax equal &
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~sum(x::'a,multiplicative_identity,multiplicative_identity)) --> False"
by meson
(*74799 inferences so far. Searching to depth 13. 314.6 secs*)
lemma BOO006_1:
"EQU001_0_ax equal &
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~product(x::'a,additive_identity,additive_identity)) --> False"
by meson
(*5 inferences so far. Searching to depth 5. 1.3 secs*)
lemma BOO011_1:
"EQU001_0_ax equal &
BOO002_0_ax equal INVERSE multiplicative_identity additive_identity multiply product add sum &
BOO002_0_eq INVERSE multiply add product sum equal &
(~equal(INVERSE(additive_identity),multiplicative_identity)) --> False"
by meson
abbreviation "CAT003_0_ax f1 compos codomain domain equal there_exists equivalent \
(\<forall>Y X. equivalent(X::'a,Y) --> there_exists(X)) &
(\<forall>X Y. equivalent(X::'a,Y) --> equal(X::'a,Y)) &
(\<forall>X Y. there_exists(X) & equal(X::'a,Y) --> equivalent(X::'a,Y)) &
(\<forall>X. there_exists(domain(X)) --> there_exists(X)) &
(\<forall>X. there_exists(codomain(X)) --> there_exists(X)) &
(\<forall>Y X. there_exists(compos(X::'a,Y)) --> there_exists(domain(X))) &
(\<forall>X Y. there_exists(compos(X::'a,Y)) --> equal(domain(X),codomain(Y))) &
(\<forall>X Y. there_exists(domain(X)) & equal(domain(X),codomain(Y)) --> there_exists(compos(X::'a,Y))) &
(\<forall>X Y Z. equal(compos(X::'a,compos(Y::'a,Z)),compos(compos(X::'a,Y),Z))) &>
(\<forall>X. equal(compos(X::'a,domain(X)),X)) &
(\<forall>X. equal(compos(codomain(X),X),X)) &
(\<forall>X Y. equivalent(X::'a,Y) --> there_exists(Y)) &
(\<forall>X Y. there_exists(X) & there_exists(Y) & equal(X::'a,Y) --> equivalent(X::'a,Y)) &
(\<forall>Y X. there_exists(compos(X::'a,Y)) --> there_exists(codomain(X))) &
(\<forall>X Y. there_exists(f1(X::'a,Y)) | equal(X::'a,Y)) &
(\<forall>X Y. equal(X::'a,f1(X::'a,Y)) | equal(Y::'a,f1(X::'a,Y)) | equal(X::'a,Y)) &n>
(\<forall>X Y. equal(X::'a,f1(X::'a,Y)) & equal(Y::'a,f1(X::'a,Y)) --> equal(X::'a,Y))"
abbreviation "CAT003_0_eq f1 compos codomain domain equivalent there_exists equal \
(\<forall>X Y. equal(X::'a,Y) & there_exists(X) --> there_exists(Y)) &
(\<forall>X Y Z. equal(X::'a,Y) & equivalent(X::'a,Z) --> equivalent(Y::'a,Z)) &
(\<forall>X Z Y. equal(X::'a,Y) & equivalent(Z::'a,X) --> equivalent(Z::'a,Y)) &
(\<forall>X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) &
(\<forall>X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) &
(\<forall>X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z))) &
(\<forall>X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) &
(\<forall>A B C. equal(A::'a,B) --> equal(f1(A::'a,C),f1(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(f1(F'::'a,D),f1(F'::'a,E)))"
(*4007 inferences so far. Searching to depth 9. 13 secs*)
lemma CAT001_3:
"EQU001_0_ax equal &
CAT003_0_ax f1 compos codomain domain equal there_exists equivalent &
CAT003_0_eq f1 compos codomain domain equivalent there_exists equal &
(there_exists(compos(a::'a,b))) &
(\<forall>Y X Z. equal(compos(compos(a::'a,b),X),Y) & equal(compos(compos(a::'a,b),Z),Y) --> equal(X::'a,Z)) &
(there_exists(compos(b::'a,h))) &
(equal(compos(b::'a,h),compos(b::'a,g))) &
(~equal(h::'a,g)) --> False"
by meson
(*245 inferences so far. Searching to depth 7. 1.0 secs*)
lemma CAT003_3:
"EQU001_0_ax equal &
CAT003_0_ax f1 compos codomain domain equal there_exists equivalent &
CAT003_0_eq f1 compos codomain domain equivalent there_exists equal &
(there_exists(compos(a::'a,b))) &
(\<forall>Y X Z. equal(compos(X::'a,compos(a::'a,b)),Y) & equal(compos(Z::'a,compos(a::'a,b)),Y) --> equal(X::'a,Z)) &
(there_exists(h)) &
(equal(compos(h::'a,a),compos(g::'a,a))) &
(~equal(g::'a,h)) --> False"
by meson
abbreviation "CAT001_0_ax equal codomain domain identity_map compos product defined \
(\<forall>X Y. defined(X::'a,Y) --> product(X::'a,Y,compos(X::'a,Y))) &
(\<forall>Z X Y. product(X::'a,Y,Z) --> defined(X::'a,Y)) &
(\<forall>X Xy Y Z. product(X::'a,Y,Xy) & defined(Xy::'a,Z) --> defined(Y::'a,Z)) &
(\<forall>Y Xy Z X Yz. product(X::'a,Y,Xy) & product(Y::'a,Z,Yz) & defined(Xy::'a,Z) --> defined(X::'a,Yz)) &
(\<forall>Xy Y Z X Yz Xyz. product(X::'a,Y,Xy) & product(Xy::'a,Z,Xyz) & product(Y::'a,Z,Yz) --> product(X::'a,Yz,Xyz)) &
(\<forall>Z Yz X Y. product(Y::'a,Z,Yz) & defined(X::'a,Yz) --> defined(X::'a,Y)) &
(\<forall>Y X Yz Xy Z. product(Y::'a,Z,Yz) & product(X::'a,Y,Xy) & defined(X::'a,Yz) --> defined(Xy::'a,Z)) &
(\<forall>Yz X Y Xy Z Xyz. product(Y::'a,Z,Yz) & product(X::'a,Yz,Xyz) & product(X::'a,Y,Xy) --> product(Xy::'a,Z,Xyz)) &
(\<forall>Y X Z. defined(X::'a,Y) & defined(Y::'a,Z) & identity_map(Y) --> defined(X::'a,Z)) &
(\<forall>X. identity_map(domain(X))) &
(\<forall>X. identity_map(codomain(X))) &
(\<forall>X. defined(X::'a,domain(X))) &
(\<forall>X. defined(codomain(X),X)) &
(\<forall>X. product(X::'a,domain(X),X)) &
(\<forall>X. product(codomain(X),X,X)) &
(\<forall>X Y. defined(X::'a,Y) & identity_map(X) --> product(X::'a,Y,Y)) &
(\<forall>Y X. defined(X::'a,Y) & identity_map(Y) --> product(X::'a,Y,X)) &
(\<forall>X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W))"
abbreviation "CAT001_0_eq compos defined identity_map codomain domain product equal \
(\<forall>X Y Z W. equal(X::'a,Y) & product(X::'a,Z,W) --> product(Y::'a,Z,W)) &
(\<forall>X Z Y W. equal(X::'a,Y) & product(Z::'a,X,W) --> product(Z::'a,Y,W)) &
(\<forall>X Z W Y. equal(X::'a,Y) & product(Z::'a,W,X) --> product(Z::'a,W,Y)) &
(\<forall>X Y. equal(X::'a,Y) --> equal(domain(X),domain(Y))) &
(\<forall>X Y. equal(X::'a,Y) --> equal(codomain(X),codomain(Y))) &
(\<forall>X Y. equal(X::'a,Y) & identity_map(X) --> identity_map(Y)) &
(\<forall>X Y Z. equal(X::'a,Y) & defined(X::'a,Z) --> defined(Y::'a,Z)) &
(\<forall>X Z Y. equal(X::'a,Y) & defined(Z::'a,X) --> defined(Z::'a,Y)) &
(\<forall>X Z Y. equal(X::'a,Y) --> equal(compos(Z::'a,X),compos(Z::'a,Y))) &
(\<forall>X Y Z. equal(X::'a,Y) --> equal(compos(X::'a,Z),compos(Y::'a,Z)))"
(*54288 inferences so far. Searching to depth 14. 118.0 secs*)
lemma CAT005_1:
"EQU001_0_ax equal &
CAT001_0_ax equal codomain domain identity_map compos product defined &
CAT001_0_eq compos defined identity_map codomain domain product equal &
(defined(a::'a,d)) &
(identity_map(d)) &
(~equal(domain(a),d)) --> False"
by meson
(*1728 inferences so far. Searching to depth 10. 5.8 secs*)
lemma CAT007_1:
"EQU001_0_ax equal &
CAT001_0_ax equal codomain domain identity_map compos product defined &
CAT001_0_eq compos defined identity_map codomain domain product equal &
(equal(domain(a),codomain(b))) &
(~defined(a::'a,b)) --> False"
by meson
(*82895 inferences so far. Searching to depth 13. 355 secs*)
lemma CAT018_1:
"EQU001_0_ax equal &
CAT001_0_ax equal codomain domain identity_map compos product defined &
CAT001_0_eq compos defined identity_map codomain domain product equal &
(defined(a::'a,b)) &
(defined(b::'a,c)) &
(~defined(a::'a,compos(b::'a,c))) --> False"
by meson
(*1118 inferences so far. Searching to depth 8. 2.3 secs*)
lemma COL001_2:
"EQU001_0_ax equal &
(\<forall>X Y Z. equal(apply(apply(apply(s::'a,X),Y),Z),apply(apply(X::'a,Z),apply(Y::'a,Z)))) &
(\<forall>Y X. equal(apply(apply(k::'a,X),Y),X)) &
(\<forall>X Y Z. equal(apply(apply(apply(b::'a,X),Y),Z),apply(X::'a,apply(Y::'a,Z)))) &</span>
(\<forall>X. equal(apply(i::'a,X),X)) &
(\<forall>A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &
(\<forall>X. equal(apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i)),apply(x::'a,apply(apply(apply(s::'a,apply(b::'a,X)),i),apply(apply(s::'a,apply(b::'a,X)),i))))) &
(\<forall>Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False"
by meson
(*500 inferences so far. Searching to depth 8. 0.9 secs*)
lemma COL023_1:
"EQU001_0_ax equal &
(\<forall>X Y Z. equal(apply(apply(apply(b::'a,X),Y),Z),apply(X::'a,apply(Y::'a,Z)))) &</span>
(\<forall>X Y Z. equal(apply(apply(apply(n::'a,X),Y),Z),apply(apply(apply(X::'a,Z),Y),Z))) &
(\<forall>A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &
(\<forall>Y. ~equal(Y::'a,apply(combinator::'a,Y))) --> False"
by meson
(*3018 inferences so far. Searching to depth 10. 4.3 secs*)
lemma COL032_1:
"EQU001_0_ax equal &
(\<forall>X. equal(apply(m::'a,X),apply(X::'a,X))) &
(\<forall>Y X Z. equal(apply(apply(apply(q::'a,X),Y),Z),apply(Y::'a,apply(X::'a,Z)))) &</span>
(\<forall>A B C. equal(A::'a,B) --> equal(apply(A::'a,C),apply(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(apply(F'::'a,D),apply(F'::'a,E))) &
(\<forall>G H. equal(G::'a,H) --> equal(f(G),f(H))) &
(\<forall>Y. ~equal(apply(Y::'a,f(Y)),apply(f(Y),apply(Y::'a,f(Y))))) --> False"
by meson
(*381878 inferences so far. Searching to depth 13. 670.4 secs*)
lemma COL052_2:
"EQU001_0_ax equal &
(\<forall>X Y W. equal(response(compos(X::'a,Y),W),response(X::'a,response(Y::'a,W)))) &
(\<forall>X Y. agreeable(X) --> equal(response(X::'a,common_bird(Y)),response(Y::'a,common_bird(Y)))) &
(\<forall>Z X. equal(response(X::'a,Z),response(compatible(X),Z)) --> agreeable(X)) &n>
(\<forall>A B. equal(A::'a,B) --> equal(common_bird(A),common_bird(B))) &
(\<forall>C D. equal(C::'a,D) --> equal(compatible(C),compatible(D))) &
(\<forall>Q R. equal(Q::'a,R) & agreeable(Q) --> agreeable(R)) &
(\<forall>A B C. equal(A::'a,B) --> equal(compos(A::'a,C),compos(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(compos(F'::'a,D),compos(F'::'a,E))) &
(\<forall>G H I'. equal(G::'a,H) --> equal(response(G::'a,I'),response(H::'a,I'))) &
(\<forall>J L K'. equal(J::'a,K') --> equal(response(L::'a,J),response(L::'a,K'))) &
(agreeable(c)) &
(~agreeable(a)) &
(equal(c::'a,compos(a::'a,b))) --> False"
by meson
(*13201 inferences so far. Searching to depth 11. 31.9 secs*)
lemma COL075_2:
"EQU001_0_ax equal &
(\<forall>Y X. equal(apply(apply(k::'a,X),Y),X)) &
(\<forall>X Y Z. equal(apply(apply(apply(abstraction::'a,X),Y),Z),apply(apply(X::'a,apply(k::'a,Z)),apply(Y::'a,Z)))) &
(\<forall>D E F'. equal(D::'a,E) --> equal(apply(D::'a,F'),apply(E::'a,F'))) &
(\<forall>G I' H. equal(G::'a,H) --> equal(apply(I'::'a,G),apply(I'::'a,H))) &
(\<forall>A B. equal(A::'a,B) --> equal(b(A),b(B))) &
(\<forall>C D. equal(C::'a,D) --> equal(c(C),c(D))) &
(\<forall>Y. ~equal(apply(apply(Y::'a,b(Y)),c(Y)),apply(b(Y),b(Y)))) --> False"
by meson
(*33 inferences so far. Searching to depth 7. 0.1 secs*)
lemma COM001_1:
"(\Goal_state Start_state. follows(Goal_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Goal_state Intermediate_state Start_state. succeeds(Goal_state::'a,Intermediate_state) & succeeds(Intermediate_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Start_state Label Goal_state. has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Start_state Condition Goal_state. has(Start_state::'a,ifthen(Condition::'a,Goal_state)) --> succeeds(Goal_state::'a,Start_state)) &
(labels(loop::'a,p3)) &
(has(p3::'a,ifthen(equal(register_j::'a,n),p4))) &
(has(p4::'a,goto(out))) &
(follows(p5::'a,p4)) &
(follows(p8::'a,p3)) &
(has(p8::'a,goto(loop))) &
(~succeeds(p3::'a,p3)) --> False"
by meson
(*533 inferences so far. Searching to depth 13. 0.3 secs*)
lemma COM002_1:
"(\Goal_state Start_state. follows(Goal_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Goal_state Intermediate_state Start_state. succeeds(Goal_state::'a,Intermediate_state) & succeeds(Intermediate_state::'a,Start_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Start_state Label Goal_state. has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state) --> succeeds(Goal_state::'a,Start_state)) &
(\<forall>Start_state Condition Goal_state. has(Start_state::'a,ifthen(Condition::'a,Goal_state)) --> succeeds(Goal_state::'a,Start_state)) &
(has(p1::'a,assign(register_j::'a,num0))) &
(follows(p2::'a,p1)) &
(has(p2::'a,assign(register_k::'a,num1))) &
(labels(loop::'a,p3)) &
(follows(p3::'a,p2)) &
(has(p3::'a,ifthen(equal(register_j::'a,n),p4))) &
(has(p4::'a,goto(out))) &
(follows(p5::'a,p4)) &
(follows(p6::'a,p3)) &
(has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &
(follows(p7::'a,p6)) &
(has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &
(follows(p8::'a,p7)) &
(has(p8::'a,goto(loop))) &
(~succeeds(p3::'a,p3)) --> False"
by meson
(*4821 inferences so far. Searching to depth 14. 1.3 secs*)
lemma COM002_2:
"(\Goal_state Start_state. ~(fails(Goal_state::'a,Start_state) & follows(Goal_state::'a,Start_state))) &
(\<forall>Goal_state Intermediate_state Start_state. fails(Goal_state::'a,Start_state) --> fails(Goal_state::'a,Intermediate_state) | fails(Intermediate_state::'a,Start_state)) &
(\<forall>Start_state Label Goal_state. ~(fails(Goal_state::'a,Start_state) & has(Start_state::'a,goto(Label)) & labels(Label::'a,Goal_state))) &
(\<forall>Start_state Condition Goal_state. ~(fails(Goal_state::'a,Start_state) & has(Start_state::'a,ifthen(Condition::'a,Goal_state)))) &
(has(p1::'a,assign(register_j::'a,num0))) &
(follows(p2::'a,p1)) &
(has(p2::'a,assign(register_k::'a,num1))) &
(labels(loop::'a,p3)) &
(follows(p3::'a,p2)) &
(has(p3::'a,ifthen(equal(register_j::'a,n),p4))) &
(has(p4::'a,goto(out))) &
(follows(p5::'a,p4)) &
(follows(p6::'a,p3)) &
(has(p6::'a,assign(register_k::'a,mtimes(num2::'a,register_k)))) &
(follows(p7::'a,p6)) &
(has(p7::'a,assign(register_j::'a,mplus(register_j::'a,num1)))) &
(follows(p8::'a,p7)) &
(has(p8::'a,goto(loop))) &
(fails(p3::'a,p3)) --> False"
by meson
(*98 inferences so far. Searching to depth 10. 1.1 secs*)
lemma COM003_2:
"(\X Y Z. program_decides(X) & program(Y) --> decides(X::'a,Y,Z)) &
(\<forall>X. program_decides(X) | program(f2(X))) &
(\<forall>X. decides(X::'a,f2(X),f1(X)) --> program_decides(X)) &
(\<forall>X. program_program_decides(X) --> program(X)) &
(\<forall>X. program_program_decides(X) --> program_decides(X)) &
(\<forall>X. program(X) & program_decides(X) --> program_program_decides(X)) &
(\<forall>X. algorithm_program_decides(X) --> algorithm(X)) &
(\<forall>X. algorithm_program_decides(X) --> program_decides(X)) &
(\<forall>X. algorithm(X) & program_decides(X) --> algorithm_program_decides(X)) &n>
(\<forall>Y X. program_halts2(X::'a,Y) --> program(X)) &
(\<forall>X Y. program_halts2(X::'a,Y) --> halts2(X::'a,Y)) &
(\<forall>X Y. program(X) & halts2(X::'a,Y) --> program_halts2(X::'a,Y)) &
(\<forall>W X Y Z. halts3_outputs(X::'a,Y,Z,W) --> halts3(X::'a,Y,Z)) &
(\<forall>Y Z X W. halts3_outputs(X::'a,Y,Z,W) --> outputs(X::'a,W)) &
(\<forall>Y Z X W. halts3(X::'a,Y,Z) & outputs(X::'a,W) --> halts3_outputs(X::'a,Y,Z,W)) &
(\<forall>Y X. program_not_halts2(X::'a,Y) --> program(X)) &
(\<forall>X Y. ~(program_not_halts2(X::'a,Y) & halts2(X::'a,Y))) &
(\<forall>X Y. program(X) --> program_not_halts2(X::'a,Y) | halts2(X::'a,Y)) &
(\<forall>W X Y. halts2_outputs(X::'a,Y,W) --> halts2(X::'a,Y)) &
(\<forall>Y X W. halts2_outputs(X::'a,Y,W) --> outputs(X::'a,W)) &
(\<forall>Y X W. halts2(X::'a,Y) & outputs(X::'a,W) --> halts2_outputs(X::'a,Y,W)) &n>
(\<forall>X W Y Z. program_halts2_halts3_outputs(X::'a,Y,Z,W) --> program_halts2(Y::'a,Z)) &
(\<forall>X Y Z W. program_halts2_halts3_outputs(X::'a,Y,Z,W) --> halts3_outputs(X::'a,Y,Z,W)) &
(\<forall>X Y Z W. program_halts2(Y::'a,Z) & halts3_outputs(X::'a,Y,Z,W) --> program_halts2_halts3_outputs(X::'a,Y,Z,W)) &
(\<forall>X W Y Z. program_not_halts2_halts3_outputs(X::'a,Y,Z,W) --> program_not_halts2(Y::'a,Z)) &
(\<forall>X Y Z W. program_not_halts2_halts3_outputs(X::'a,Y,Z,W) --> halts3_outputs(X::'a,Y,Z,W)) &
(\<forall>X Y Z W. program_not_halts2(Y::'a,Z) & halts3_outputs(X::'a,Y,Z,W) --> program_not_halts2_halts3_outputs(X::'a,Y,Z,W)) &
(\<forall>X W Y. program_halts2_halts2_outputs(X::'a,Y,W) --> program_halts2(Y::'a,Y)) &pan>
(\<forall>X Y W. program_halts2_halts2_outputs(X::'a,Y,W) --> halts2_outputs(X::'a,Y,W)) &</span>
(\<forall>X Y W. program_halts2(Y::'a,Y) & halts2_outputs(X::'a,Y,W) --> program_halts2_halts2_outputs(X::'a,Y,W)) &
(\<forall>X W Y. program_not_halts2_halts2_outputs(X::'a,Y,W) --> program_not_halts2(Y::'a,Y)) &
(\<forall>X Y W. program_not_halts2_halts2_outputs(X::'a,Y,W) --> halts2_outputs(X::'a,Y,W)) &
(\<forall>X Y W. program_not_halts2(Y::'a,Y) & halts2_outputs(X::'a,Y,W) --> program_not_halts2_halts2_outputs(X::'a,Y,W)) &
(\<forall>X. algorithm_program_decides(X) --> program_program_decides(c1)) &
(\<forall>W Y Z. program_program_decides(W) --> program_halts2_halts3_outputs(W::'a,Y,Z,good)) &
(\<forall>W Y Z. program_program_decides(W) --> program_not_halts2_halts3_outputs(W::'a,Y,Z,bad)) &
(\<forall>W. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program(c2)) &
(\<forall>W Y. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program_halts2_halts2_outputs(c2::'a,Y,good)) &
(\<forall>W Y. program(W) & program_halts2_halts3_outputs(W::'a,f3(W),f3(W),good) & program_not_halts2_halts3_outputs(W::'a,f3(W),f3(W),bad) --> program_not_halts2_halts2_outputs(c2::'a,Y,bad)) &
(\<forall>V. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) --> program(c3)) &
(\<forall>V Y. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) & program_halts2(Y::'a,Y) --> halts2(c3::'a,Y)) &
(\<forall>V Y. program(V) & program_halts2_halts2_outputs(V::'a,f4(V),good) & program_not_halts2_halts2_outputs(V::'a,f4(V),bad) --> program_not_halts2_halts2_outputs(c3::'a,Y,bad)) &
(algorithm_program_decides(c4)) --> False"
by meson
(*2100398 inferences so far. Searching to depth 12.
1256s (21 mins) on griffon*)
lemma COM004_1:
"EQU001_0_ax equal &
(\<forall>C D P Q X Y. failure_node(X::'a,or(C::'a,P)) & failure_node(Y::'a,or(D::'a,Q)) & contradictory(P::'a,Q) & siblings(X::'a,Y) --> failure_node(parent_of(X::'a,Y),or(C::'a,D))) &
(\<forall>X. contradictory(negate(X),X)) &
(\<forall>X. contradictory(X::'a,negate(X))) &
(\<forall>X. siblings(left_child_of(X),right_child_of(X))) &
(\<forall>D E. equal(D::'a,E) --> equal(left_child_of(D),left_child_of(E))) &
(\<forall>F' G. equal(F'::'a,G) --> equal(negate(F'),negate(G))) &
(\<forall>H I' J. equal(H::'a,I') --> equal(or(H::'a,J),or(I'::'a,J))) &
(\<forall>K' M L. equal(K'::'a,L) --> equal(or(M::'a,K'),or(M::'a,L))) &
(\<forall>N O' P. equal(N::'a,O') --> equal(parent_of(N::'a,P),parent_of(O'::'a,P))) &n>
(\<forall>Q S' R. equal(Q::'a,R) --> equal(parent_of(S'::'a,Q),parent_of(S'::'a,R))) &n>
(\<forall>T' U. equal(T'::'a,U) --> equal(right_child_of(T'),right_child_of(U))) &
(\<forall>V W X. equal(V::'a,W) & contradictory(V::'a,X) --> contradictory(W::'a,X)) &pan>
(\<forall>Y A1 Z. equal(Y::'a,Z) & contradictory(A1::'a,Y) --> contradictory(A1::'a,Z)) &
(\<forall>B1 C1 D1. equal(B1::'a,C1) & failure_node(B1::'a,D1) --> failure_node(C1::'a,D1)) &
(\<forall>E1 G1 F1. equal(E1::'a,F1) & failure_node(G1::'a,E1) --> failure_node(G1::'a,F1)) &
(\<forall>H1 I1 J1. equal(H1::'a,I1) & siblings(H1::'a,J1) --> siblings(I1::'a,J1)) &an>
(\<forall>K1 M1 L1. equal(K1::'a,L1) & siblings(M1::'a,K1) --> siblings(M1::'a,L1)) &an>
(failure_node(n_left::'a,or(EMPTY::'a,atom))) &
(failure_node(n_right::'a,or(EMPTY::'a,negate(atom)))) &
(equal(n_left::'a,left_child_of(n))) &
(equal(n_right::'a,right_child_of(n))) &
(\<forall>Z. ~failure_node(Z::'a,or(EMPTY::'a,EMPTY))) --> False"
oops
abbreviation "GEO001_0_ax continuous lower_dimension_point_3 lower_dimension_point_2
lower_dimension_point_1 extension euclid2 euclid1 outer_pasch equidistant equal between \<equiv>
(\<forall>X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) &
(\<forall>V X Y Z. between(X::'a,Y,V) & between(Y::'a,Z,V) --> between(X::'a,Y,Z)) &>
(\<forall>Y X V Z. between(X::'a,Y,Z) & between(X::'a,Y,V) --> equal(X::'a,Y) | between(X::'a,Z,V) | between(X::'a,V,Z)) &
(\<forall>Y X. equidistant(X::'a,Y,Y,X)) &
(\<forall>Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) &
(\<forall>X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) &
(\<forall>W X Z V Y. between(X::'a,W,V) & between(Y::'a,V,Z) --> between(X::'a,outer_pasch(W::'a,X,Y,Z,V),Y)) &
(\<forall>W X Y Z V. between(X::'a,W,V) & between(Y::'a,V,Z) --> between(Z::'a,W,outer_pasch(W::'a,X,Y,Z,V))) &
(\<forall>W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(X::'a,Z,euclid1(W::'a,X,Y,Z,V))) &
(\<forall>W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(X::'a,Y,euclid2(W::'a,X,Y,Z,V))) &
(\<forall>W X Y Z V. between(X::'a,V,W) & between(Y::'a,V,Z) --> equal(X::'a,V) | between(euclid1(W::'a,X,Y,Z,V),W,euclid2(W::'a,X,Y,Z,V))) &
(\<forall>X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) &
(\<forall>X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) &
(\<forall>X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) &
(~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) &
(~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) &
(~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) &
(\<forall>Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) &
(\<forall>X Y Z X1 Z1 V. equidistant(V::'a,X,V,X1) & equidistant(V::'a,Z,V,Z1) & between(V::'a,X,Z) & between(X::'a,Y,Z) --> equidistant(V::'a,Y,Z,continuous(X::'a,Y,Z,X1,Z1,V))) &
(\<forall>X Y Z X1 V Z1. equidistant(V::'a,X,V,X1) & equidistant(V::'a,Z,V,Z1) & between(V::'a,X,Z) & between(X::'a,Y,Z) --> between(X1::'a,continuous(X::'a,Y,Z,X1,Z1,V),Z1))"
abbreviation "GEO001_0_eq continuous extension euclid2 euclid1 outer_pasch equidistant
between equal \<equiv>
(\<forall>X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) &
(\<forall>X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) &
(\<forall>X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) &
(\<forall>X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) &
(\<forall>X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) &
(\<forall>X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) &
(\<forall>X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(outer_pasch(X::'a,V1,V2,V3,V4),outer_pasch(Y::'a,V1,V2,V3,V4))) &
(\<forall>X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,X,V2,V3,V4),outer_pasch(V1::'a,Y,V2,V3,V4))) &
(\<forall>X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,X,V3,V4),outer_pasch(V1::'a,V2,Y,V3,V4))) &
(\<forall>X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,X,V4),outer_pasch(V1::'a,V2,V3,Y,V4))) &
(\<forall>X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(outer_pasch(V1::'a,V2,V3,V4,X),outer_pasch(V1::'a,V2,V3,V4,Y))) &
(\<forall>A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) &
(\<forall>G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) &
(\<forall>M O' P N Q R. equal(M::'a,N) --> equal(euclid1(O'::'a,P,M,Q,R),euclid1(O'::'a,P,N,Q,R))) &
(\<forall>S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) &
(\<forall>Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) &
(\<forall>E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) &
(\<forall>K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) &
(\<forall>Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) &
(\<forall>W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) &
(\<forall>C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) &
(\<forall>X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) &
(\<forall>X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) &
(\<forall>X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) &
(\<forall>X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) &
(\<forall>X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) &
(\<forall>X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) &
(\<forall>X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) &
(\<forall>X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) &
(\<forall>X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) &
(\<forall>X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y)))"
(*179 inferences so far. Searching to depth 7. 3.9 secs*)
lemma GEO003_1:
"EQU001_0_ax equal &
GEO001_0_ax continuous lower_dimension_point_3 lower_dimension_point_2
lower_dimension_point_1 extension euclid2 euclid1 outer_pasch equidistant equal between &
GEO001_0_eq continuous extension euclid2 euclid1 outer_pasch equidistant between equal &
(~between(a::'a,b,b)) --> False"
by meson
abbreviation "GEO002_ax_eq continuous euclid2 euclid1 lower_dimension_point_3
lower_dimension_point_2 lower_dimension_point_1 inner_pasch extension
between equal equidistant \<equiv>
(\<forall>Y X. equidistant(X::'a,Y,Y,X)) &
(\<forall>X Y Z V V2 W. equidistant(X::'a,Y,Z,V) & equidistant(X::'a,Y,V2,W) --> equidistant(Z::'a,V,V2,W)) &
(\<forall>Z X Y. equidistant(X::'a,Y,Z,Z) --> equal(X::'a,Y)) &
(\<forall>X Y W V. between(X::'a,Y,extension(X::'a,Y,W,V))) &
(\<forall>X Y W V. equidistant(Y::'a,extension(X::'a,Y,W,V),W,V)) &
(\<forall>X1 Y1 X Y Z V Z1 V1. equidistant(X::'a,Y,X1,Y1) & equidistant(Y::'a,Z,Y1,Z1) & equidistant(X::'a,V,X1,V1) & equidistant(Y::'a,V,Y1,V1) & between(X::'a,Y,Z) & between(X1::'a,Y1,Z1) --> equal(X::'a,Y) | equidistant(Z::'a,V,Z1,V1)) &
(\<forall>X Y. between(X::'a,Y,X) --> equal(X::'a,Y)) &
(\<forall>U V W X Y. between(U::'a,V,W) & between(Y::'a,X,W) --> between(V::'a,inner_pasch(U::'a,V,W,X,Y),Y)) &
(\<forall>V W X Y U. between(U::'a,V,W) & between(Y::'a,X,W) --> between(X::'a,inner_pasch(U::'a,V,W,X,Y),U)) &
(~between(lower_dimension_point_1::'a,lower_dimension_point_2,lower_dimension_point_3)) &
(~between(lower_dimension_point_2::'a,lower_dimension_point_3,lower_dimension_point_1)) &
(~between(lower_dimension_point_3::'a,lower_dimension_point_1,lower_dimension_point_2)) &
(\<forall>Z X Y W V. equidistant(X::'a,W,X,V) & equidistant(Y::'a,W,Y,V) & equidistant(Z::'a,W,Z,V) --> between(X::'a,Y,Z) | between(Y::'a,Z,X) | between(Z::'a,X,Y) | equal(W::'a,V)) &
(\<forall>U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,V,euclid1(U::'a,V,W,X,Y))) &
(\<forall>U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(U::'a,X,euclid2(U::'a,V,W,X,Y))) &
(\<forall>U V W X Y. between(U::'a,W,Y) & between(V::'a,W,X) --> equal(U::'a,W) | between(euclid1(U::'a,V,W,X,Y),Y,euclid2(U::'a,V,W,X,Y))) &
(\<forall>U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> between(V1::'a,continuous(U::'a,V,V1,W,X,X1),X1)) &
(\<forall>U V V1 W X X1. equidistant(U::'a,V,U,V1) & equidistant(U::'a,X,U,X1) & between(U::'a,V,X) & between(V::'a,W,X) --> equidistant(U::'a,W,U,continuous(U::'a,V,V1,W,X,X1))) &
(\<forall>X Y W Z. equal(X::'a,Y) & between(X::'a,W,Z) --> between(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & between(W::'a,X,Z) --> between(W::'a,Y,Z)) &
(\<forall>X W Z Y. equal(X::'a,Y) & between(W::'a,Z,X) --> between(W::'a,Z,Y)) &
(\<forall>X Y V W Z. equal(X::'a,Y) & equidistant(X::'a,V,W,Z) --> equidistant(Y::'a,V,W,Z)) &
(\<forall>X V Y W Z. equal(X::'a,Y) & equidistant(V::'a,X,W,Z) --> equidistant(V::'a,Y,W,Z)) &
(\<forall>X V W Y Z. equal(X::'a,Y) & equidistant(V::'a,W,X,Z) --> equidistant(V::'a,W,Y,Z)) &
(\<forall>X V W Z Y. equal(X::'a,Y) & equidistant(V::'a,W,Z,X) --> equidistant(V::'a,W,Z,Y)) &
(\<forall>X Y V1 V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(X::'a,V1,V2,V3,V4),inner_pasch(Y::'a,V1,V2,V3,V4))) &
(\<forall>X V1 Y V2 V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,X,V2,V3,V4),inner_pasch(V1::'a,Y,V2,V3,V4))) &
(\<forall>X V1 V2 Y V3 V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,X,V3,V4),inner_pasch(V1::'a,V2,Y,V3,V4))) &
(\<forall>X V1 V2 V3 Y V4. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,X,V4),inner_pasch(V1::'a,V2,V3,Y,V4))) &
(\<forall>X V1 V2 V3 V4 Y. equal(X::'a,Y) --> equal(inner_pasch(V1::'a,V2,V3,V4,X),inner_pasch(V1::'a,V2,V3,V4,Y))) &
(\<forall>A B C D E F'. equal(A::'a,B) --> equal(euclid1(A::'a,C,D,E,F'),euclid1(B::'a,C,D,E,F'))) &
(\<forall>G I' H J K' L. equal(G::'a,H) --> equal(euclid1(I'::'a,G,J,K',L),euclid1(I'::'a,H,J,K',L))) &
(\<forall>M O' P N Q R. equal(M::'a,N) --> equal(euclid1(O'::'a,P,M,Q,R),euclid1(O'::'a,P,N,Q,R))) &
(\<forall>S' U V W T' X. equal(S'::'a,T') --> equal(euclid1(U::'a,V,W,S',X),euclid1(U::'a,V,W,T',X))) &
(\<forall>Y A1 B1 C1 D1 Z. equal(Y::'a,Z) --> equal(euclid1(A1::'a,B1,C1,D1,Y),euclid1(A1::'a,B1,C1,D1,Z))) &
(\<forall>E1 F1 G1 H1 I1 J1. equal(E1::'a,F1) --> equal(euclid2(E1::'a,G1,H1,I1,J1),euclid2(F1::'a,G1,H1,I1,J1))) &
(\<forall>K1 M1 L1 N1 O1 P1. equal(K1::'a,L1) --> equal(euclid2(M1::'a,K1,N1,O1,P1),euclid2(M1::'a,L1,N1,O1,P1))) &
(\<forall>Q1 S1 T1 R1 U1 V1. equal(Q1::'a,R1) --> equal(euclid2(S1::'a,T1,Q1,U1,V1),euclid2(S1::'a,T1,R1,U1,V1))) &
(\<forall>W1 Y1 Z1 A2 X1 B2. equal(W1::'a,X1) --> equal(euclid2(Y1::'a,Z1,A2,W1,B2),euclid2(Y1::'a,Z1,A2,X1,B2))) &
(\<forall>C2 E2 F2 G2 H2 D2. equal(C2::'a,D2) --> equal(euclid2(E2::'a,F2,G2,H2,C2),euclid2(E2::'a,F2,G2,H2,D2))) &
(\<forall>X Y V1 V2 V3. equal(X::'a,Y) --> equal(extension(X::'a,V1,V2,V3),extension(Y::'a,V1,V2,V3))) &
(\<forall>X V1 Y V2 V3. equal(X::'a,Y) --> equal(extension(V1::'a,X,V2,V3),extension(V1::'a,Y,V2,V3))) &
(\<forall>X V1 V2 Y V3. equal(X::'a,Y) --> equal(extension(V1::'a,V2,X,V3),extension(V1::'a,V2,Y,V3))) &
(\<forall>X V1 V2 V3 Y. equal(X::'a,Y) --> equal(extension(V1::'a,V2,V3,X),extension(V1::'a,V2,V3,Y))) &
(\<forall>X Y V1 V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(X::'a,V1,V2,V3,V4,V5),continuous(Y::'a,V1,V2,V3,V4,V5))) &
(\<forall>X V1 Y V2 V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,X,V2,V3,V4,V5),continuous(V1::'a,Y,V2,V3,V4,V5))) &
(\<forall>X V1 V2 Y V3 V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,X,V3,V4,V5),continuous(V1::'a,V2,Y,V3,V4,V5))) &
(\<forall>X V1 V2 V3 Y V4 V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,X,V4,V5),continuous(V1::'a,V2,V3,Y,V4,V5))) &
(\<forall>X V1 V2 V3 V4 Y V5. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,X,V5),continuous(V1::'a,V2,V3,V4,Y,V5))) &
(\<forall>X V1 V2 V3 V4 V5 Y. equal(X::'a,Y) --> equal(continuous(V1::'a,V2,V3,V4,V5,X),continuous(V1::'a,V2,V3,V4,V5,Y)))"
(*4272 inferences so far. Searching to depth 10. 29.4 secs*)
lemma GEO017_2:
"EQU001_0_ax equal &
GEO002_ax_eq continuous euclid2 euclid1 lower_dimension_point_3
lower_dimension_point_2 lower_dimension_point_1 inner_pasch extension
between equal equidistant &
(equidistant(u::'a,v,w,x)) &
(~equidistant(u::'a,v,x,w)) --> False"
by meson
(*382903 inferences so far. Searching to depth 9. 1022s (17 mins) on griffon*)
lemma GEO027_3:
"EQU001_0_ax equal &
GEO002_ax_eq continuous euclid2 euclid1 lower_dimension_point_3
lower_dimension_point_2 lower_dimension_point_1 inner_pasch extension
between equal equidistant &
(\<forall>U V. equal(reflection(U::'a,V),extension(U::'a,V,U,V))) &
(\<forall>X Y Z. equal(X::'a,Y) --> equal(reflection(X::'a,Z),reflection(Y::'a,Z))) &>
(\<forall>A1 C1 B1. equal(A1::'a,B1) --> equal(reflection(C1::'a,A1),reflection(C1::'a,B1))) &
(\<forall>U V. equidistant(U::'a,V,U,V)) &
(\<forall>W X U V. equidistant(U::'a,V,W,X) --> equidistant(W::'a,X,U,V)) &
(\<forall>V U W X. equidistant(U::'a,V,W,X) --> equidistant(V::'a,U,W,X)) &
(\<forall>U V X W. equidistant(U::'a,V,W,X) --> equidistant(U::'a,V,X,W)) &
(\<forall>V U X W. equidistant(U::'a,V,W,X) --> equidistant(V::'a,U,X,W)) &
(\<forall>W X V U. equidistant(U::'a,V,W,X) --> equidistant(W::'a,X,V,U)) &
(\<forall>X W U V. equidistant(U::'a,V,W,X) --> equidistant(X::'a,W,U,V)) &
(\<forall>X W V U. equidistant(U::'a,V,W,X) --> equidistant(X::'a,W,V,U)) &
(\<forall>W X U V Y Z. equidistant(U::'a,V,W,X) & equidistant(W::'a,X,Y,Z) --> equidistant(U::'a,V,Y,Z)) &
(\<forall>U V W. equal(V::'a,extension(U::'a,V,W,W))) &
(\<forall>W X U V Y. equal(Y::'a,extension(U::'a,V,W,X)) --> between(U::'a,V,Y)) &
(\<forall>U V. between(U::'a,V,reflection(U::'a,V))) &
(\<forall>U V. equidistant(V::'a,reflection(U::'a,V),U,V)) &
(\<forall>U V. equal(U::'a,V) --> equal(V::'a,reflection(U::'a,V))) &
(\<forall>U. equal(U::'a,reflection(U::'a,U))) &
(\<forall>U V. equal(V::'a,reflection(U::'a,V)) --> equal(U::'a,V)) &
(\<forall>U V. equidistant(U::'a,U,V,V)) &
(\<forall>V V1 U W U1 W1. equidistant(U::'a,V,U1,V1) & equidistant(V::'a,W,V1,W1) & between(U::'a,V,W) & between(U1::'a,V1,W1) --> equidistant(U::'a,W,U1,W1)) &
(\<forall>U V W X. between(U::'a,V,W) & between(U::'a,V,X) & equidistant(V::'a,W,V,X) --> equal(U::'a,V) | equal(W::'a,X)) &
(between(u::'a,v,w)) &
(~equal(u::'a,v)) &
(~equal(w::'a,extension(u::'a,v,v,w))) --> False"
oops
(*313884 inferences so far. Searching to depth 10. 887 secs: 15 mins.*)
lemma GEO058_2:
"EQU001_0_ax equal &
GEO002_ax_eq continuous euclid2 euclid1 lower_dimension_point_3
lower_dimension_point_2 lower_dimension_point_1 inner_pasch extension
between equal equidistant &
(\<forall>U V. equal(reflection(U::'a,V),extension(U::'a,V,U,V))) &
(\<forall>X Y Z. equal(X::'a,Y) --> equal(reflection(X::'a,Z),reflection(Y::'a,Z))) &>
(\<forall>A1 C1 B1. equal(A1::'a,B1) --> equal(reflection(C1::'a,A1),reflection(C1::'a,B1))) &
(equal(v::'a,reflection(u::'a,v))) &
(~equal(u::'a,v)) --> False"
oops
(*0 inferences so far. Searching to depth 0. 0.2 secs*)
lemma GEO079_1:
"(\U V W X Y Z. right_angle(U::'a,V,W) & right_angle(X::'a,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &
(\<forall>U V W X Y Z. CONGRUENT(U::'a,V,W,X,Y,Z) --> eq(U::'a,V,W,X,Y,Z)) &
(\<forall>V W U X. trapezoid(U::'a,V,W,X) --> parallel(V::'a,W,U,X)) &
(\<forall>U V X Y. parallel(U::'a,V,X,Y) --> eq(X::'a,V,U,V,X,Y)) &
(trapezoid(a::'a,b,c,d)) &
(~eq(a::'a,c,b,c,a,d)) --> False"
by meson
abbreviation "GRP003_0_ax equal multiply INVERSE identity product \
(\<forall>X. product(identity::'a,X,X)) &
(\<forall>X. product(X::'a,identity,X)) &
(\<forall>X. product(INVERSE(X),X,identity)) &
(\<forall>X. product(X::'a,INVERSE(X),identity)) &
(\<forall>X Y. product(X::'a,Y,multiply(X::'a,Y))) &
(\<forall>X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &
(\<forall>Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &
(\<forall>Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W))"
abbreviation "GRP003_0_eq product multiply INVERSE equal \
(\<forall>X Y. equal(X::'a,Y) --> equal(INVERSE(X),INVERSE(Y))) &
(\<forall>X Y W. equal(X::'a,Y) --> equal(multiply(X::'a,W),multiply(Y::'a,W))) &
(\<forall>X W Y. equal(X::'a,Y) --> equal(multiply(W::'a,X),multiply(W::'a,Y))) &
(\<forall>X Y W Z. equal(X::'a,Y) & product(X::'a,W,Z) --> product(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & product(W::'a,X,Z) --> product(W::'a,Y,Z)) &
(\<forall>X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y))"
(*2032008 inferences so far. Searching to depth 16. 658s (11 mins) on griffon*)
lemma GRP001_1:
"EQU001_0_ax equal &
GRP003_0_ax equal multiply INVERSE identity product &
GRP003_0_eq product multiply INVERSE equal &
(\<forall>X. product(X::'a,X,identity)) &
(product(a::'a,b,c)) &
(~product(b::'a,a,c)) --> False"
oops
(*2386 inferences so far. Searching to depth 11. 8.7 secs*)
lemma GRP008_1:
"EQU001_0_ax equal &
GRP003_0_ax equal multiply INVERSE identity product &
GRP003_0_eq product multiply INVERSE equal &
(\<forall>A B. equal(A::'a,B) --> equal(h(A),h(B))) &
(\<forall>C D. equal(C::'a,D) --> equal(j(C),j(D))) &
(\<forall>A B. equal(A::'a,B) & q(A) --> q(B)) &
(\<forall>B A C. q(A) & product(A::'a,B,C) --> product(B::'a,A,C)) &
(\<forall>A. product(j(A),A,h(A)) | product(A::'a,j(A),h(A)) | q(A)) &
(\<forall>A. product(j(A),A,h(A)) & product(A::'a,j(A),h(A)) --> q(A)) &
(~q(identity)) --> False"
by meson
(*8625 inferences so far. Searching to depth 11. 20 secs*)
lemma GRP013_1:
"EQU001_0_ax equal &
GRP003_0_ax equal multiply INVERSE identity product &
GRP003_0_eq product multiply INVERSE equal &
(\<forall>A. product(A::'a,A,identity)) &
(product(a::'a,b,c)) &
(product(INVERSE(a),INVERSE(b),d)) &
(\<forall>A C B. product(INVERSE(A),INVERSE(B),C) --> product(A::'a,C,B)) &
(~product(c::'a,d,identity)) --> False"
by meson
(*2448 inferences so far. Searching to depth 10. 7.2 secs*)
lemma GRP037_3:
"EQU001_0_ax equal &
GRP003_0_ax equal multiply INVERSE identity product &
GRP003_0_eq product multiply INVERSE equal &
(\<forall>A B C. subgroup_member(A) & subgroup_member(B) & product(A::'a,INVERSE(B),C) --> subgroup_member(C)) &
(\<forall>A B. equal(A::'a,B) & subgroup_member(A) --> subgroup_member(B)) &
(\<forall>A. subgroup_member(A) --> product(Gidentity::'a,A,A)) &
(\<forall>A. subgroup_member(A) --> product(A::'a,Gidentity,A)) &
(\<forall>A. subgroup_member(A) --> product(A::'a,Ginverse(A),Gidentity)) &
(\<forall>A. subgroup_member(A) --> product(Ginverse(A),A,Gidentity)) &
(\<forall>A. subgroup_member(A) --> subgroup_member(Ginverse(A))) &
(\<forall>A B. equal(A::'a,B) --> equal(Ginverse(A),Ginverse(B))) &
(\<forall>A C D B. product(A::'a,B,C) & product(A::'a,D,C) --> equal(D::'a,B)) &
(\<forall>B C D A. product(A::'a,B,C) & product(D::'a,B,C) --> equal(D::'a,A)) &
(subgroup_member(a)) &
(subgroup_member(Gidentity)) &
(~equal(INVERSE(a),Ginverse(a))) --> False"
by meson
(*163 inferences so far. Searching to depth 11. 0.3 secs*)
lemma GRP031_2:
"(\X Y. product(X::'a,Y,multiply(X::'a,Y))) &
(\<forall>X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &
(\<forall>Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &
(\<forall>Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &
(\<forall>A. product(A::'a,INVERSE(A),identity)) &
(\<forall>A. product(A::'a,identity,A)) &
(\<forall>A. ~product(A::'a,a,identity)) --> False"
by meson
(*47 inferences so far. Searching to depth 11. 0.2 secs*)
lemma GRP034_4:
"(\X Y. product(X::'a,Y,multiply(X::'a,Y))) &
(\<forall>X. product(identity::'a,X,X)) &
(\<forall>X. product(X::'a,identity,X)) &
(\<forall>X. product(X::'a,INVERSE(X),identity)) &
(\<forall>Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &
(\<forall>Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &
(\<forall>B A C. subgroup_member(A) & subgroup_member(B) & product(B::'a,INVERSE(A),C) --> subgroup_member(C)) &
(subgroup_member(a)) &
(~subgroup_member(INVERSE(a))) --> False"
by meson
(*3287 inferences so far. Searching to depth 14. 3.5 secs*)
lemma GRP047_2:
"(\X. product(identity::'a,X,X)) &
(\<forall>X. product(INVERSE(X),X,identity)) &
(\<forall>X Y. product(X::'a,Y,multiply(X::'a,Y))) &
(\<forall>X Y Z W. product(X::'a,Y,Z) & product(X::'a,Y,W) --> equal(Z::'a,W)) &
(\<forall>Y U Z X V W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(U::'a,Z,W) --> product(X::'a,V,W)) &
(\<forall>Y X V U Z W. product(X::'a,Y,U) & product(Y::'a,Z,V) & product(X::'a,V,W) --> product(U::'a,Z,W)) &
(\<forall>X W Z Y. equal(X::'a,Y) & product(W::'a,Z,X) --> product(W::'a,Z,Y)) &
(equal(a::'a,b)) &
(~equal(multiply(c::'a,a),multiply(c::'a,b))) --> False"
by meson
(*25559 inferences so far. Searching to depth 19. 16.9 secs*)
lemma GRP130_1_002:
"(group_element(e_1)) &
(group_element(e_2)) &
(~equal(e_1::'a,e_2)) &
(~equal(e_2::'a,e_1)) &
(\<forall>X Y. group_element(X) & group_element(Y) --> product(X::'a,Y,e_1) | product(X::'a,Y,e_2)) &
(\<forall>X Y W Z. product(X::'a,Y,W) & product(X::'a,Y,Z) --> equal(W::'a,Z)) &
(\<forall>X Y W Z. product(X::'a,W,Y) & product(X::'a,Z,Y) --> equal(W::'a,Z)) &
(\<forall>Y X W Z. product(W::'a,Y,X) & product(Z::'a,Y,X) --> equal(W::'a,Z)) &
(\<forall>Z1 Z2 Y X. product(X::'a,Y,Z1) & product(X::'a,Z1,Z2) --> product(Z2::'a,Y,X)) --> False"
by meson
abbreviation "GRP004_0_ax INVERSE identity multiply equal \
(\<forall>X. equal(multiply(identity::'a,X),X)) &
(\<forall>X. equal(multiply(INVERSE(X),X),identity)) &
(\<forall>X Y Z. equal(multiply(multiply(X::'a,Y),Z),multiply(X::'a,multiply(Y::'a,Z)))) &
(\<forall>A B. equal(A::'a,B) --> equal(INVERSE(A),INVERSE(B))) &
(\<forall>C D E. equal(C::'a,D) --> equal(multiply(C::'a,E),multiply(D::'a,E))) &
(\<forall>F' H G. equal(F'::'a,G) --> equal(multiply(H::'a,F'),multiply(H::'a,G)))"
abbreviation "GRP004_2_ax multiply least_upper_bound greatest_lower_bound equal \
(\<forall>Y X. equal(greatest_lower_bound(X::'a,Y),greatest_lower_bound(Y::'a,X))) &pan>
(\<forall>Y X. equal(least_upper_bound(X::'a,Y),least_upper_bound(Y::'a,X))) &
(\<forall>X Y Z. equal(greatest_lower_bound(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(greatest_lower_bound(X::'a,Y),Z))) &
(\<forall>X Y Z. equal(least_upper_bound(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(least_upper_bound(X::'a,Y),Z))) &
(\<forall>X. equal(least_upper_bound(X::'a,X),X)) &
(\<forall>X. equal(greatest_lower_bound(X::'a,X),X)) &
(\<forall>Y X. equal(least_upper_bound(X::'a,greatest_lower_bound(X::'a,Y)),X)) &>
(\<forall>Y X. equal(greatest_lower_bound(X::'a,least_upper_bound(X::'a,Y)),X)) &>
(\<forall>Y X Z. equal(multiply(X::'a,least_upper_bound(Y::'a,Z)),least_upper_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) &
(\<forall>Y X Z. equal(multiply(X::'a,greatest_lower_bound(Y::'a,Z)),greatest_lower_bound(multiply(X::'a,Y),multiply(X::'a,Z)))) &
(\<forall>Y Z X. equal(multiply(least_upper_bound(Y::'a,Z),X),least_upper_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) &
(\<forall>Y Z X. equal(multiply(greatest_lower_bound(Y::'a,Z),X),greatest_lower_bound(multiply(Y::'a,X),multiply(Z::'a,X)))) &
(\<forall>A B C. equal(A::'a,B) --> equal(greatest_lower_bound(A::'a,C),greatest_lower_bound(B::'a,C))) &
(\<forall>A C B. equal(A::'a,B) --> equal(greatest_lower_bound(C::'a,A),greatest_lower_bound(C::'a,B))) &
(\<forall>A B C. equal(A::'a,B) --> equal(least_upper_bound(A::'a,C),least_upper_bound(B::'a,C))) &
(\<forall>A C B. equal(A::'a,B) --> equal(least_upper_bound(C::'a,A),least_upper_bound(C::'a,B))) &
(\<forall>A B C. equal(A::'a,B) --> equal(multiply(A::'a,C),multiply(B::'a,C))) &
(\<forall>A C B. equal(A::'a,B) --> equal(multiply(C::'a,A),multiply(C::'a,B)))"
(*3468 inferences so far. Searching to depth 10. 9.1 secs*)
lemma GRP156_1:
"EQU001_0_ax equal &
GRP004_0_ax INVERSE identity multiply equal &
GRP004_2_ax multiply least_upper_bound greatest_lower_bound equal &
(equal(least_upper_bound(a::'a,b),b)) &
(~equal(greatest_lower_bound(multiply(a::'a,c),multiply(b::'a,c)),multiply(a::'a,c))) --> False"
by meson
(*4394 inferences so far. Searching to depth 10. 8.2 secs*)
lemma GRP168_1:
"EQU001_0_ax equal &
GRP004_0_ax INVERSE identity multiply equal &
GRP004_2_ax multiply least_upper_bound greatest_lower_bound equal &
(equal(least_upper_bound(a::'a,b),b)) &
(~equal(least_upper_bound(multiply(INVERSE(c),multiply(a::'a,c)),multiply(INVERSE(c),multiply(b::'a,c))),multiply(INVERSE(c),multiply(b::'a,c)))) --> False"
by meson
abbreviation "HEN002_0_ax identity Zero Divide equal mless_equal \
(\<forall>X Y. mless_equal(X::'a,Y) --> equal(Divide(X::'a,Y),Zero)) &
(\<forall>X Y. equal(Divide(X::'a,Y),Zero) --> mless_equal(X::'a,Y)) &
(\<forall>Y X. mless_equal(Divide(X::'a,Y),X)) &
(\<forall>X Y Z. mless_equal(Divide(Divide(X::'a,Z),Divide(Y::'a,Z)),Divide(Divide(X::'a,Y),Z))) &
(\<forall>X. mless_equal(Zero::'a,X)) &
(\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) &
(\<forall>X. mless_equal(X::'a,identity))"
abbreviation "HEN002_0_eq mless_equal Divide equal \
(\<forall>A B C. equal(A::'a,B) --> equal(Divide(A::'a,C),Divide(B::'a,C))) &
(\<forall>D F' E. equal(D::'a,E) --> equal(Divide(F'::'a,D),Divide(F'::'a,E))) &
(\<forall>G H I'. equal(G::'a,H) & mless_equal(G::'a,I') --> mless_equal(H::'a,I')) &an>
(\<forall>J L K'. equal(J::'a,K') & mless_equal(L::'a,J) --> mless_equal(L::'a,K'))"
(*250258 inferences so far. Searching to depth 16. 406.2 secs*)
lemma HEN003_3:
"EQU001_0_ax equal &
HEN002_0_ax identity Zero Divide equal mless_equal &
HEN002_0_eq mless_equal Divide equal &
(~equal(Divide(a::'a,a),Zero)) --> False"
by meson
(*202177 inferences so far. Searching to depth 14. 451 secs*)
lemma HEN007_2:
"EQU001_0_ax equal &
(\<forall>X Y. mless_equal(X::'a,Y) --> quotient(X::'a,Y,Zero)) &
(\<forall>X Y. quotient(X::'a,Y,Zero) --> mless_equal(X::'a,Y)) &
(\<forall>Y Z X. quotient(X::'a,Y,Z) --> mless_equal(Z::'a,X)) &
(\<forall>Y X V3 V2 V1 Z V4 V5. quotient(X::'a,Y,V1) & quotient(Y::'a,Z,V2) & quotient(X::'a,Z,V3) & quotient(V3::'a,V2,V4) & quotient(V1::'a,Z,V5) --> mless_equal(V4::'a,V5)) &
(\<forall>X. mless_equal(Zero::'a,X)) &
(\<forall>X Y. mless_equal(X::'a,Y) & mless_equal(Y::'a,X) --> equal(X::'a,Y)) &
(\<forall>X. mless_equal(X::'a,identity)) &
(\<forall>X Y. quotient(X::'a,Y,Divide(X::'a,Y))) &
(\<forall>X Y Z W. quotient(X::'a,Y,Z) & quotient(X::'a,Y,W) --> equal(Z::'a,W)) &
(\<forall>X Y W Z. equal(X::'a,Y) & quotient(X::'a,W,Z) --> quotient(Y::'a,W,Z)) &
(\<forall>X W Y Z. equal(X::'a,Y) & quotient(W::'a,X,Z) --> quotient(W::'a,Y,Z)) &
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.640 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
