SSL Meson_Test.thy Sprache: Isabelle

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 or

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 Meson.simp_options_all_true ctxt prem25;
    val xsko25 = Meson.skolemize Meson.simp_options_all_true 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 Meson.simp_options_all_true ctxt prem26;
    val xsko26 = Meson.skolemize Meson.simp_options_all_true 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 Meson.simp_options_all_true ctxt prem43;
    val xsko43 = Meson.skolemize Meson.simp_options_all_true 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)) &
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ 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.0.26Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.