src/HOL/ex/Argo_Examples.thy
 author boehmes Thu Sep 29 20:54:44 2016 +0200 (2016-09-29) changeset 63960 3daf02070be5 child 64927 a5a09855e424 permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
```     1 (*  Title:      HOL/ex/Argo_Examples.thy
```
```     2     Author:     Sascha Boehme
```
```     3 *)
```
```     4
```
```     5 section \<open>Argo\<close>
```
```     6
```
```     7 theory Argo_Examples
```
```     8 imports Complex_Main
```
```     9 begin
```
```    10
```
```    11 text \<open>
```
```    12   This theory is intended to showcase and test different features of the \<open>argo\<close> proof method.
```
```    13
```
```    14   The \<open>argo\<close> proof method can be applied to propositional problems, problems involving equality
```
```    15   reasoning and problems of linear real arithmetic.
```
```    16
```
```    17   The \<open>argo\<close> proof method provides two options. To specify an upper limit of the proof methods
```
```    18   run time in seconds, use the option \<open>argo_timeout\<close>. To specify the amount of output, use the
```
```    19   option \<open>argo_trace\<close> with value \<open>none\<close> for no tracing output, value \<open>basic\<close> for viewing the
```
```    20   underlying propositions and some timings, and value \<open>full\<close> for additionally inspecting the
```
```    21   proof replay steps.
```
```    22 \<close>
```
```    23
```
```    24 declare[[argo_trace = full]]
```
```    25
```
```    26 subsection \<open>Propositional logic\<close>
```
```    27
```
```    28 notepad
```
```    29 begin
```
```    30   have "True" by argo
```
```    31 next
```
```    32   have "~False" by argo
```
```    33 next
```
```    34   fix P :: bool
```
```    35   assume "False"
```
```    36   then have "P" by argo
```
```    37 next
```
```    38   fix P :: bool
```
```    39   assume "~True"
```
```    40   then have "P" by argo
```
```    41 next
```
```    42   fix P :: bool
```
```    43   assume "P"
```
```    44   then have "P" by argo
```
```    45 next
```
```    46   fix P :: bool
```
```    47   assume "~~P"
```
```    48   then have "P" by argo
```
```    49 next
```
```    50   fix P Q R :: bool
```
```    51   assume "P & Q & R"
```
```    52   then have "R & P & Q" by argo
```
```    53 next
```
```    54   fix P Q R :: bool
```
```    55   assume "P & (Q & True & R) & (Q & P) & True"
```
```    56   then have "R & P & Q" by argo
```
```    57 next
```
```    58   fix P Q1 Q2 Q3 Q4 Q5 :: bool
```
```    59   assume "Q1 & (Q2 & P & Q3) & (Q4 & ~P & Q5)"
```
```    60   then have "~True" by argo
```
```    61 next
```
```    62   fix P Q1 Q2 Q3  :: bool
```
```    63   assume "(Q1 & False) & Q2 & Q3"
```
```    64   then have "P::bool" by argo
```
```    65 next
```
```    66   fix P Q R :: bool
```
```    67   assume "P | Q | R"
```
```    68   then have "R | P | Q" by argo
```
```    69 next
```
```    70   fix P Q R :: bool
```
```    71   assume "P | (Q | False | R) | (Q | P) | False"
```
```    72   then have "R | P | Q" by argo
```
```    73 next
```
```    74   fix P Q1 Q2 Q3 Q4 :: bool
```
```    75   have "(Q1 & P & Q2) --> False | (Q3 | (Q4 | P) | False)" by argo
```
```    76 next
```
```    77   fix Q1 Q2 Q3 Q4 :: bool
```
```    78   have "Q1 | (Q2 | True | Q3) | Q4" by argo
```
```    79 next
```
```    80   fix P Q R :: bool
```
```    81   assume "(P & Q) | (P & ~Q) | (P & R) | (P & ~R)"
```
```    82   then have "P" by argo
```
```    83 next
```
```    84   fix P :: bool
```
```    85   assume "P = True"
```
```    86   then have "P" by argo
```
```    87 next
```
```    88   fix P :: bool
```
```    89   assume "False = P"
```
```    90   then have "~P" by argo
```
```    91 next
```
```    92   fix P Q :: bool
```
```    93   assume "P = (~P)"
```
```    94   then have "Q" by argo
```
```    95 next
```
```    96   fix P :: bool
```
```    97   have "(~P) = (~P)" by argo
```
```    98 next
```
```    99   fix P Q :: bool
```
```   100   assume "P" and "~Q"
```
```   101   then have "P = (~Q)" by argo
```
```   102 next
```
```   103   fix P Q :: bool
```
```   104   assume "((P::bool) = Q) | (Q = P)"
```
```   105   then have "(P --> Q) & (Q --> P)" by argo
```
```   106 next
```
```   107   fix P Q :: bool
```
```   108   assume "(P::bool) = Q"
```
```   109   then have "Q = P" by argo
```
```   110 next
```
```   111   fix P Q R :: bool
```
```   112   assume "if P then Q else R"
```
```   113   then have "Q | R" by argo
```
```   114 next
```
```   115   fix P Q :: bool
```
```   116   assume "P | Q"
```
```   117      and "P | ~Q"
```
```   118      and "~P | Q"
```
```   119      and "~P | ~Q"
```
```   120   then have "False" by argo
```
```   121 next
```
```   122   fix P Q R :: bool
```
```   123   assume "P | Q | R"
```
```   124      and "P | Q | ~R"
```
```   125      and "P | ~Q | R"
```
```   126      and "P | ~Q | ~R"
```
```   127      and "~P | Q | R"
```
```   128      and "~P | Q | ~R"
```
```   129      and "~P | ~Q | R"
```
```   130      and "~P | ~Q | ~R"
```
```   131   then have "False" by argo
```
```   132 next
```
```   133   fix a b c d e f g h i j k l m n p q :: bool
```
```   134   assume "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
```
```   135   then have "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)" by argo
```
```   136 next
```
```   137   fix P :: bool
```
```   138   have "P=P=P=P=P=P=P=P=P=P" by argo
```
```   139 next
```
```   140   fix a b c d e f p q x :: bool
```
```   141   assume "a | b | c | d"
```
```   142      and "e | f | (a & d)"
```
```   143      and "~(a | (c & ~c)) | b"
```
```   144      and "~(b & (x | ~x)) | c"
```
```   145      and "~(d | False) | c"
```
```   146      and "~(c | (~p & (p | (q & ~q))))"
```
```   147   then have "False" by argo
```
```   148 end
```
```   149
```
```   150
```
```   151 subsection \<open>Equality, congruence and predicates\<close>
```
```   152
```
```   153 notepad
```
```   154 begin
```
```   155   fix t :: "'a"
```
```   156   have "t = t" by argo
```
```   157 next
```
```   158   fix t u :: "'a"
```
```   159   assume "t = u"
```
```   160   then have "u = t" by argo
```
```   161 next
```
```   162   fix s t u :: "'a"
```
```   163   assume "s = t" and "t = u"
```
```   164   then have "s = u" by argo
```
```   165 next
```
```   166   fix s t u v :: "'a"
```
```   167   assume "s = t" and "t = u" and "u = v" and "u = s"
```
```   168   then have "s = v" by argo
```
```   169 next
```
```   170   fix s t u v w :: "'a"
```
```   171   assume "s = t" and "t = u" and "s = v" and "v = w"
```
```   172   then have "w = u" by argo
```
```   173 next
```
```   174   fix s t u a b c :: "'a"
```
```   175   assume "s = t" and "t = u" and "a = b" and "b = c"
```
```   176   then have "s = a --> c = u" by argo
```
```   177 next
```
```   178   fix a b c d :: "'a"
```
```   179   assume "(a = b & b = c) | (a = d & d = c)"
```
```   180   then have "a = c" by argo
```
```   181 next
```
```   182   fix a b1 b2 b3 b4 c d :: "'a"
```
```   183   assume "(a = b1 & ((b1 = b2 & b2 = b3) | (b1 = b4 & b4 = b3)) & b3 = c) | (a = d & d = c)"
```
```   184   then have "a = c" by argo
```
```   185 next
```
```   186   fix a b :: "'a"
```
```   187   have "(if True then a else b) = a" by argo
```
```   188 next
```
```   189   fix a b :: "'a"
```
```   190   have "(if False then a else b) = b" by argo
```
```   191 next
```
```   192   fix a b :: "'a"
```
```   193   have "(if \<not>True then a else b) = b" by argo
```
```   194 next
```
```   195   fix a b :: "'a"
```
```   196   have "(if \<not>False then a else b) = a" by argo
```
```   197 next
```
```   198   fix P :: "bool"
```
```   199   fix a :: "'a"
```
```   200   have "(if P then a else a) = a" by argo
```
```   201 next
```
```   202   fix P :: "bool"
```
```   203   fix a b c :: "'a"
```
```   204   assume "P" and "a = c"
```
```   205   then have "(if P then a else b) = c" by argo
```
```   206 next
```
```   207   fix P :: "bool"
```
```   208   fix a b c :: "'a"
```
```   209   assume "~P" and "b = c"
```
```   210   then have "(if P then a else b) = c" by argo
```
```   211 next
```
```   212   fix P Q :: "bool"
```
```   213   fix a b c d :: "'a"
```
```   214   assume "P" and "Q" and "a = d"
```
```   215   then have "(if P then (if Q then a else b) else c) = d" by argo
```
```   216 next
```
```   217   fix a b c :: "'a"
```
```   218   assume "a \<noteq> b" and "b = c"
```
```   219   then have "a \<noteq> c" by argo
```
```   220 next
```
```   221   fix a b c :: "'a"
```
```   222   assume "a \<noteq> b" and "a = c"
```
```   223   then have "c \<noteq> b" by argo
```
```   224 next
```
```   225   fix a b c d :: "'a"
```
```   226   assume "a = b" and "c = d" and "b \<noteq> d"
```
```   227   then have "a \<noteq> c" by argo
```
```   228 next
```
```   229   fix a b c d :: "'a"
```
```   230   assume "a = b" and "c = d" and "d \<noteq> b"
```
```   231   then have "a \<noteq> c" by argo
```
```   232 next
```
```   233   fix a b c d :: "'a"
```
```   234   assume "a = b" and "c = d" and "b \<noteq> d"
```
```   235   then have "c \<noteq> a" by argo
```
```   236 next
```
```   237   fix a b c d :: "'a"
```
```   238   assume "a = b" and "c = d" and "d \<noteq> b"
```
```   239   then have "c \<noteq> a" by argo
```
```   240 next
```
```   241   fix a b c d e f :: "'a"
```
```   242   assume "a \<noteq> b" and "b = c" and "b = d" and "d = e" and "a = f"
```
```   243   then have "f \<noteq> e" by argo
```
```   244 next
```
```   245   fix a b :: "'a" and f :: "'a \<Rightarrow> 'a"
```
```   246   assume "a = b"
```
```   247   then have "f a = f b" by argo
```
```   248 next
```
```   249   fix a b c :: "'a" and f :: "'a \<Rightarrow> 'a"
```
```   250   assume "f a = f b" and "b = c"
```
```   251   then have "f a = f c" by argo
```
```   252 next
```
```   253   fix a :: "'a" and f :: "'a \<Rightarrow> 'a"
```
```   254   assume "f a = a"
```
```   255   then have "f (f a) = a" by argo
```
```   256 next
```
```   257   fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
```
```   258   assume "a = b"
```
```   259   then have "g (f a) = g (f b)" by argo
```
```   260 next
```
```   261   fix a b :: "'a" and f g :: "'a \<Rightarrow> 'a"
```
```   262   assume "f a = b" and "g b = a"
```
```   263   then have "f (g (f a)) = b" by argo
```
```   264 next
```
```   265   fix a b :: "'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```   266   assume "a = b"
```
```   267   then have "g a b = g b a" by argo
```
```   268 next
```
```   269   fix a b :: "'a" and f :: "'a \<Rightarrow> 'a" and g :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```   270   assume "f a = b"
```
```   271   then have "g (f a) b = g b (f a)" by argo
```
```   272 next
```
```   273   fix a b c d e g h :: "'a" and f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
```
```   274   assume "c = d" and "e = c" and "e = b" and "b = h" and "f g h = d" and "f g d = a"
```
```   275   then have "a = b" by argo
```
```   276 next
```
```   277   fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
```
```   278   assume "P a" and "a = b"
```
```   279   then have "P b" by argo
```
```   280 next
```
```   281   fix a b :: "'a" and P :: "'a \<Rightarrow> bool"
```
```   282   assume "~ P a" and "a = b"
```
```   283   then have "~ P b" by argo
```
```   284 next
```
```   285   fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   286   assume "P a b" and "a = c" and "b = d"
```
```   287   then have "P c d" by argo
```
```   288 next
```
```   289   fix a b c d :: "'a" and P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   290   assume "~ P a b" and "a = c" and "b = d"
```
```   291   then have "~ P c d" by argo
```
```   292 end
```
```   293
```
```   294
```
```   295 subsection \<open>Linear real arithmetic\<close>
```
```   296
```
```   297 subsubsection \<open>Negation and subtraction\<close>
```
```   298
```
```   299 notepad
```
```   300 begin
```
```   301   fix a b :: real
```
```   302   have
```
```   303     "-a = -1 * a"
```
```   304     "-(-a) = a"
```
```   305     "a - b = a + -1 * b"
```
```   306     "a - (-b) = a + b"
```
```   307     by argo+
```
```   308 end
```
```   309
```
```   310
```
```   311 subsubsection \<open>Multiplication\<close>
```
```   312
```
```   313 notepad
```
```   314 begin
```
```   315   fix a b c d :: real
```
```   316   have
```
```   317     "(2::real) * 3 = 6"
```
```   318     "0 * a = 0"
```
```   319     "a * 0 = 0"
```
```   320     "1 * a = a"
```
```   321     "a * 1 = a"
```
```   322     "2 * a = a * 2"
```
```   323     "2 * a * 3 = 6 * a"
```
```   324     "2 * a * 3 * 5 = 30 * a"
```
```   325     "a * 0 * b = 0"
```
```   326     "a * (0 * b) = 0"
```
```   327     "a * (b * c) = (a * b) * c"
```
```   328     "a * (b * (c * d)) = ((a * b) * c) * d"
```
```   329     "a * (b + c + d) = a * b + a * c + a * d"
```
```   330     by argo+
```
```   331 end
```
```   332
```
```   333
```
```   334 subsubsection \<open>Division\<close>
```
```   335
```
```   336 notepad
```
```   337 begin
```
```   338   fix a b c :: real
```
```   339   have
```
```   340     "(6::real) / 2 = 3"
```
```   341     "a / 0 = a / 0"
```
```   342     "a / 0 <= a / 0"
```
```   343     "~(a / 0 < a / 0)"
```
```   344     "0 / a = 0"
```
```   345     "a / 1 = a"
```
```   346     "a / 3 = 1/3 * a"
```
```   347     "6 * a / 2 = 3 * a"
```
```   348     "a / ((5 * b) / 2) = 2/5 * a / b"
```
```   349     "a / (5 * (b / 2)) = 2/5 * a / b"
```
```   350     "(a / 5) * (b / 2) = 1/10 * a * b"
```
```   351     "a / (3 * b) = 1/3 * a / b"
```
```   352     "(a + b) / 5 = 1/5 * a + 1/5 * b"
```
```   353     "a / (5 * 1/5) = a"
```
```   354     by argo+
```
```   355 end
```
```   356
```
```   357
```
```   358 subsubsection \<open>Addition\<close>
```
```   359
```
```   360 notepad
```
```   361 begin
```
```   362   fix a b c d :: real
```
```   363   have
```
```   364     "a + b = b + a"
```
```   365     "a + b + c = c + b + a"
```
```   366     "a + b + c + d = d + c + b + a"
```
```   367     "a + (b + (c + d)) = ((a + b) + c) + d"
```
```   368     "(5::real) + -3 = 2"
```
```   369     "(3::real) + 5 + -1 = 7"
```
```   370     "2 + a = a + 2"
```
```   371     "a + b + a = b + 2 * a"
```
```   372     "-1 + a + -1 + 2 + b + 5/3 + b + 1/3 + 5 * b + 2/3 = 8/3 + a + 7 * b"
```
```   373     "1 + b + b + 5 * b + 3 * a + 7 + a + 2 = 10 + 4 * a + 7 * b"
```
```   374     by argo+
```
```   375 end
```
```   376
```
```   377
```
```   378 subsubsection \<open>Minimum and maximum\<close>
```
```   379
```
```   380 notepad
```
```   381 begin
```
```   382   fix a b :: real
```
```   383   have
```
```   384     "min (3::real) 5 = 3"
```
```   385     "min (5::real) 3 = 3"
```
```   386     "min (3::real) (-5) = -5"
```
```   387     "min (-5::real) 3 = -5"
```
```   388     "min a a = a"
```
```   389     "a \<le> b \<longrightarrow> min a b = a"
```
```   390     "a > b \<longrightarrow> min a b = b"
```
```   391     "min a b \<le> a"
```
```   392     "min a b \<le> b"
```
```   393     "min a b = min b a"
```
```   394     by argo+
```
```   395 next
```
```   396   fix a b :: real
```
```   397   have
```
```   398     "max (3::real) 5 = 5"
```
```   399     "max (5::real) 3 = 5"
```
```   400     "max (3::real) (-5) = 3"
```
```   401     "max (-5::real) 3 = 3"
```
```   402     "max a a = a"
```
```   403     "a \<le> b \<longrightarrow> max a b = b"
```
```   404     "a > b \<longrightarrow> max a b = a"
```
```   405     "a \<le> max a b"
```
```   406     "b \<le> max a b"
```
```   407     "max a b = max b a"
```
```   408     by argo+
```
```   409 next
```
```   410   fix a b :: real
```
```   411   have
```
```   412     "min a b \<le> max a b"
```
```   413     "min a b + max a b = a + b"
```
```   414     "a < b \<longrightarrow> min a b < max a b"
```
```   415     by argo+
```
```   416 end
```
```   417
```
```   418
```
```   419 subsubsection \<open>Absolute value\<close>
```
```   420
```
```   421 notepad
```
```   422 begin
```
```   423   fix a :: real
```
```   424   have
```
```   425     "abs (3::real) = 3"
```
```   426     "abs (-3::real) = 3"
```
```   427     "0 \<le> abs a"
```
```   428     "a \<le> abs a"
```
```   429     "a \<ge> 0 \<longrightarrow> abs a = a"
```
```   430     "a < 0 \<longrightarrow> abs a = -a"
```
```   431     "abs (abs a) = abs a"
```
```   432     by argo+
```
```   433 end
```
```   434
```
```   435
```
```   436 subsubsection \<open>Equality\<close>
```
```   437
```
```   438 notepad
```
```   439 begin
```
```   440   fix a b c d :: real
```
```   441   have
```
```   442     "(3::real) = 3"
```
```   443     "~((3::real) = 4)"
```
```   444     "~((4::real) = 3)"
```
```   445     "3 * a = 5 --> a = 5/3"
```
```   446     "-3 * a = 5 --> -5/3 = a"
```
```   447     "5 = 3 * a --> 5/3  = a "
```
```   448     "5 = -3 * a --> a = -5/3"
```
```   449     "2 + 3 * a = 4 --> a = 2/3"
```
```   450     "4 = 2 + 3 * a --> 2/3 = a"
```
```   451     "2 + 3 * a + 5 * b + c = 4 --> 3 * a + 5 * b + c = 2"
```
```   452     "4 = 2 + 3 * a + 5 * b + c --> 2 = 3 * a + 5 * b + c"
```
```   453     "-2 * a + b + -3 * c = 7 --> -7 = 2 * a + -1 * b + 3 * c"
```
```   454     "7 = -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c = -7"
```
```   455     "-2 * a + b + -3 * c + 4 * d = 7 --> -7 = 2 * a + -1 * b + 3 * c + -4 * d"
```
```   456     "7 = -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d = -7"
```
```   457     "a + 3 * b = 5 * c + b --> a + 2 * b + -5 * c = 0"
```
```   458     by argo+
```
```   459 end
```
```   460
```
```   461
```
```   462 subsubsection \<open>Less-equal\<close>
```
```   463
```
```   464 notepad
```
```   465 begin
```
```   466   fix a b c d :: real
```
```   467   have
```
```   468     "(3::real) <= 3"
```
```   469     "(3::real) <= 4"
```
```   470     "~((4::real) <= 3)"
```
```   471     "3 * a <= 5 --> a <= 5/3"
```
```   472     "-3 * a <= 5 --> -5/3 <= a"
```
```   473     "5 <= 3 * a --> 5/3  <= a "
```
```   474     "5 <= -3 * a --> a <= -5/3"
```
```   475     "2 + 3 * a <= 4 --> a <= 2/3"
```
```   476     "4 <= 2 + 3 * a --> 2/3 <= a"
```
```   477     "2 + 3 * a + 5 * b + c <= 4 --> 3 * a + 5 * b + c <= 2"
```
```   478     "4 <= 2 + 3 * a + 5 * b + c --> 2 <= 3 * a + 5 * b + c"
```
```   479     "-2 * a + b + -3 * c <= 7 --> -7 <= 2 * a + -1 * b + 3 * c"
```
```   480     "7 <= -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c <= -7"
```
```   481     "-2 * a + b + -3 * c + 4 * d <= 7 --> -7 <= 2 * a + -1 * b + 3 * c + -4 * d"
```
```   482     "7 <= -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d <= -7"
```
```   483     "a + 3 * b <= 5 * c + b --> a + 2 * b + -5 * c <= 0"
```
```   484     by argo+
```
```   485 end
```
```   486
```
```   487 subsubsection \<open>Less\<close>
```
```   488
```
```   489 notepad
```
```   490 begin
```
```   491   fix a b c d :: real
```
```   492   have
```
```   493     "(3::real) < 4"
```
```   494     "~((3::real) < 3)"
```
```   495     "~((4::real) < 3)"
```
```   496     "3 * a < 5 --> a < 5/3"
```
```   497     "-3 * a < 5 --> -5/3 < a"
```
```   498     "5 < 3 * a --> 5/3  < a "
```
```   499     "5 < -3 * a --> a < -5/3"
```
```   500     "2 + 3 * a < 4 --> a < 2/3"
```
```   501     "4 < 2 + 3 * a --> 2/3 < a"
```
```   502     "2 + 3 * a + 5 * b + c < 4 --> 3 * a + 5 * b + c < 2"
```
```   503     "4 < 2 + 3 * a + 5 * b + c --> 2 < 3 * a + 5 * b + c"
```
```   504     "-2 * a + b + -3 * c < 7 --> -7 < 2 * a + -1 * b + 3 * c"
```
```   505     "7 < -2 * a + b + -3 * c --> 2 * a + -1 * b + 3 * c < -7"
```
```   506     "-2 * a + b + -3 * c + 4 * d < 7 --> -7 < 2 * a + -1 * b + 3 * c + -4 * d"
```
```   507     "7 < -2 * a + b + -3 * c + 4 * d --> 2 * a + -1 * b + 3 * c + -4 * d < -7"
```
```   508     "a + 3 * b < 5 * c + b --> a + 2 * b + -5 * c < 0"
```
```   509     by argo+
```
```   510 end
```
```   511
```
```   512
```
```   513 subsubsection \<open>Other examples\<close>
```
```   514
```
```   515 notepad
```
```   516 begin
```
```   517   have
```
```   518     "(0::real) < 1"
```
```   519     "(47::real) + 11 < 8 * 15"
```
```   520     by argo+
```
```   521 next
```
```   522   fix a :: real
```
```   523   assume "a < 3"
```
```   524   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
```
```   525 next
```
```   526   fix a :: real
```
```   527   assume "a <= 3"
```
```   528   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
```
```   529 next
```
```   530   fix a :: real
```
```   531   assume "~(3 < a)"
```
```   532   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
```
```   533 next
```
```   534   fix a :: real
```
```   535   assume "~(3 <= a)"
```
```   536   then have "a < 5" "a <= 5" "~(5 < a)" "~(5 <= a)" by argo+
```
```   537 next
```
```   538   fix a :: real
```
```   539   have "a < 3 | a = 3 | a > 3" by argo
```
```   540 next
```
```   541   fix a b :: real
```
```   542   assume "0 < a" and "a < b"
```
```   543   then have "0 < b" by argo
```
```   544 next
```
```   545   fix a b :: real
```
```   546   assume "0 < a" and "a \<le> b"
```
```   547   then have "0 \<le> b" by argo
```
```   548 next
```
```   549   fix a b :: real
```
```   550   assume "0 \<le> a" and "a < b"
```
```   551   then have "0 \<le> b" by argo
```
```   552 next
```
```   553   fix a b :: real
```
```   554   assume "0 \<le> a" and "a \<le> b"
```
```   555   then have "0 \<le> b" by argo
```
```   556 next
```
```   557   fix a b c :: real
```
```   558   assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
```
```   559   then have "-2 * a + -3 * b + 5 * c < 13" by argo
```
```   560 next
```
```   561   fix a b c :: real
```
```   562   assume "2 \<le> a" and "3 \<le> b" and "c \<le> 5"
```
```   563   then have "-2 * a + -3 * b + 5 * c \<le> 12" by argo
```
```   564 next
```
```   565   fix a b :: real
```
```   566   assume "a = 2" and "b = 3"
```
```   567   then have "a + b > 5 \<or> a < b" by argo
```
```   568 next
```
```   569   fix a b c :: real
```
```   570   assume "5 < b + c" and "a + c < 0" and "a > 0"
```
```   571   then have "b > 0" by argo
```
```   572 next
```
```   573   fix a b c :: real
```
```   574   assume "a + b < 7" and "5 < b + c" and "a + c < 0" and "a > 0"
```
```   575   then have "0 < b \<and> b < 7" by argo
```
```   576 next
```
```   577   fix a b c :: real
```
```   578   assume "a < b" and "b < c" and "c < a"
```
```   579   then have "False" by argo
```
```   580 next
```
```   581   fix a b :: real
```
```   582   assume "a - 5 > b"
```
```   583   then have "b < a" by argo
```
```   584 next
```
```   585   fix a b :: real
```
```   586   have "(a - b) - a = (a - a) - b" by argo
```
```   587 next
```
```   588   fix n m n' m' :: real
```
```   589   have "
```
```   590     (n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
```
```   591     (n = n' & n' < m) | (n = m & m < n') |
```
```   592     (n' < m & m < n) | (n' < m & m = n) |
```
```   593     (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
```
```   594     (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
```
```   595     (m = n & n < n') | (m = n' & n' < n) |
```
```   596     (n' = m & m = n)"
```
```   597     by argo
```
```   598 end
```
```   599
```
```   600
```
```   601 subsection \<open>Larger examples\<close>
```
```   602
```
```   603 declare[[argo_trace = basic, argo_timeout = 60]]
```
```   604
```
```   605
```
```   606 text \<open>Translated from TPTP problem library: PUZ015-2.006.dimacs\<close>
```
```   607
```
```   608 lemma assumes 1: "~x0"
```
```   609   and 2: "~x30"
```
```   610   and 3: "~x29"
```
```   611   and 4: "~x59"
```
```   612   and 5: "x1 | x31 | x0"
```
```   613   and 6: "x2 | x32 | x1"
```
```   614   and 7: "x3 | x33 | x2"
```
```   615   and 8: "x4 | x34 | x3"
```
```   616   and 9: "x35 | x4"
```
```   617   and 10: "x5 | x36 | x30"
```
```   618   and 11: "x6 | x37 | x5 | x31"
```
```   619   and 12: "x7 | x38 | x6 | x32"
```
```   620   and 13: "x8 | x39 | x7 | x33"
```
```   621   and 14: "x9 | x40 | x8 | x34"
```
```   622   and 15: "x41 | x9 | x35"
```
```   623   and 16: "x10 | x42 | x36"
```
```   624   and 17: "x11 | x43 | x10 | x37"
```
```   625   and 18: "x12 | x44 | x11 | x38"
```
```   626   and 19: "x13 | x45 | x12 | x39"
```
```   627   and 20: "x14 | x46 | x13 | x40"
```
```   628   and 21: "x47 | x14 | x41"
```
```   629   and 22: "x15 | x48 | x42"
```
```   630   and 23: "x16 | x49 | x15 | x43"
```
```   631   and 24: "x17 | x50 | x16 | x44"
```
```   632   and 25: "x18 | x51 | x17 | x45"
```
```   633   and 26: "x19 | x52 | x18 | x46"
```
```   634   and 27: "x53 | x19 | x47"
```
```   635   and 28: "x20 | x54 | x48"
```
```   636   and 29: "x21 | x55 | x20 | x49"
```
```   637   and 30: "x22 | x56 | x21 | x50"
```
```   638   and 31: "x23 | x57 | x22 | x51"
```
```   639   and 32: "x24 | x58 | x23 | x52"
```
```   640   and 33: "x59 | x24 | x53"
```
```   641   and 34: "x25 | x54"
```
```   642   and 35: "x26 | x25 | x55"
```
```   643   and 36: "x27 | x26 | x56"
```
```   644   and 37: "x28 | x27 | x57"
```
```   645   and 38: "x29 | x28 | x58"
```
```   646   and 39: "~x1 | ~x31"
```
```   647   and 40: "~x1 | ~x0"
```
```   648   and 41: "~x31 | ~x0"
```
```   649   and 42: "~x2 | ~x32"
```
```   650   and 43: "~x2 | ~x1"
```
```   651   and 44: "~x32 | ~x1"
```
```   652   and 45: "~x3 | ~x33"
```
```   653   and 46: "~x3 | ~x2"
```
```   654   and 47: "~x33 | ~x2"
```
```   655   and 48: "~x4 | ~x34"
```
```   656   and 49: "~x4 | ~x3"
```
```   657   and 50: "~x34 | ~x3"
```
```   658   and 51: "~x35 | ~x4"
```
```   659   and 52: "~x5 | ~x36"
```
```   660   and 53: "~x5 | ~x30"
```
```   661   and 54: "~x36 | ~x30"
```
```   662   and 55: "~x6 | ~x37"
```
```   663   and 56: "~x6 | ~x5"
```
```   664   and 57: "~x6 | ~x31"
```
```   665   and 58: "~x37 | ~x5"
```
```   666   and 59: "~x37 | ~x31"
```
```   667   and 60: "~x5 | ~x31"
```
```   668   and 61: "~x7 | ~x38"
```
```   669   and 62: "~x7 | ~x6"
```
```   670   and 63: "~x7 | ~x32"
```
```   671   and 64: "~x38 | ~x6"
```
```   672   and 65: "~x38 | ~x32"
```
```   673   and 66: "~x6 | ~x32"
```
```   674   and 67: "~x8 | ~x39"
```
```   675   and 68: "~x8 | ~x7"
```
```   676   and 69: "~x8 | ~x33"
```
```   677   and 70: "~x39 | ~x7"
```
```   678   and 71: "~x39 | ~x33"
```
```   679   and 72: "~x7 | ~x33"
```
```   680   and 73: "~x9 | ~x40"
```
```   681   and 74: "~x9 | ~x8"
```
```   682   and 75: "~x9 | ~x34"
```
```   683   and 76: "~x40 | ~x8"
```
```   684   and 77: "~x40 | ~x34"
```
```   685   and 78: "~x8 | ~x34"
```
```   686   and 79: "~x41 | ~x9"
```
```   687   and 80: "~x41 | ~x35"
```
```   688   and 81: "~x9 | ~x35"
```
```   689   and 82: "~x10 | ~x42"
```
```   690   and 83: "~x10 | ~x36"
```
```   691   and 84: "~x42 | ~x36"
```
```   692   and 85: "~x11 | ~x43"
```
```   693   and 86: "~x11 | ~x10"
```
```   694   and 87: "~x11 | ~x37"
```
```   695   and 88: "~x43 | ~x10"
```
```   696   and 89: "~x43 | ~x37"
```
```   697   and 90: "~x10 | ~x37"
```
```   698   and 91: "~x12 | ~x44"
```
```   699   and 92: "~x12 | ~x11"
```
```   700   and 93: "~x12 | ~x38"
```
```   701   and 94: "~x44 | ~x11"
```
```   702   and 95: "~x44 | ~x38"
```
```   703   and 96: "~x11 | ~x38"
```
```   704   and 97: "~x13 | ~x45"
```
```   705   and 98: "~x13 | ~x12"
```
```   706   and 99: "~x13 | ~x39"
```
```   707   and 100: "~x45 | ~x12"
```
```   708   and 101: "~x45 | ~x39"
```
```   709   and 102: "~x12 | ~x39"
```
```   710   and 103: "~x14 | ~x46"
```
```   711   and 104: "~x14 | ~x13"
```
```   712   and 105: "~x14 | ~x40"
```
```   713   and 106: "~x46 | ~x13"
```
```   714   and 107: "~x46 | ~x40"
```
```   715   and 108: "~x13 | ~x40"
```
```   716   and 109: "~x47 | ~x14"
```
```   717   and 110: "~x47 | ~x41"
```
```   718   and 111: "~x14 | ~x41"
```
```   719   and 112: "~x15 | ~x48"
```
```   720   and 113: "~x15 | ~x42"
```
```   721   and 114: "~x48 | ~x42"
```
```   722   and 115: "~x16 | ~x49"
```
```   723   and 116: "~x16 | ~x15"
```
```   724   and 117: "~x16 | ~x43"
```
```   725   and 118: "~x49 | ~x15"
```
```   726   and 119: "~x49 | ~x43"
```
```   727   and 120: "~x15 | ~x43"
```
```   728   and 121: "~x17 | ~x50"
```
```   729   and 122: "~x17 | ~x16"
```
```   730   and 123: "~x17 | ~x44"
```
```   731   and 124: "~x50 | ~x16"
```
```   732   and 125: "~x50 | ~x44"
```
```   733   and 126: "~x16 | ~x44"
```
```   734   and 127: "~x18 | ~x51"
```
```   735   and 128: "~x18 | ~x17"
```
```   736   and 129: "~x18 | ~x45"
```
```   737   and 130: "~x51 | ~x17"
```
```   738   and 131: "~x51 | ~x45"
```
```   739   and 132: "~x17 | ~x45"
```
```   740   and 133: "~x19 | ~x52"
```
```   741   and 134: "~x19 | ~x18"
```
```   742   and 135: "~x19 | ~x46"
```
```   743   and 136: "~x52 | ~x18"
```
```   744   and 137: "~x52 | ~x46"
```
```   745   and 138: "~x18 | ~x46"
```
```   746   and 139: "~x53 | ~x19"
```
```   747   and 140: "~x53 | ~x47"
```
```   748   and 141: "~x19 | ~x47"
```
```   749   and 142: "~x20 | ~x54"
```
```   750   and 143: "~x20 | ~x48"
```
```   751   and 144: "~x54 | ~x48"
```
```   752   and 145: "~x21 | ~x55"
```
```   753   and 146: "~x21 | ~x20"
```
```   754   and 147: "~x21 | ~x49"
```
```   755   and 148: "~x55 | ~x20"
```
```   756   and 149: "~x55 | ~x49"
```
```   757   and 150: "~x20 | ~x49"
```
```   758   and 151: "~x22 | ~x56"
```
```   759   and 152: "~x22 | ~x21"
```
```   760   and 153: "~x22 | ~x50"
```
```   761   and 154: "~x56 | ~x21"
```
```   762   and 155: "~x56 | ~x50"
```
```   763   and 156: "~x21 | ~x50"
```
```   764   and 157: "~x23 | ~x57"
```
```   765   and 158: "~x23 | ~x22"
```
```   766   and 159: "~x23 | ~x51"
```
```   767   and 160: "~x57 | ~x22"
```
```   768   and 161: "~x57 | ~x51"
```
```   769   and 162: "~x22 | ~x51"
```
```   770   and 163: "~x24 | ~x58"
```
```   771   and 164: "~x24 | ~x23"
```
```   772   and 165: "~x24 | ~x52"
```
```   773   and 166: "~x58 | ~x23"
```
```   774   and 167: "~x58 | ~x52"
```
```   775   and 168: "~x23 | ~x52"
```
```   776   and 169: "~x59 | ~x24"
```
```   777   and 170: "~x59 | ~x53"
```
```   778   and 171: "~x24 | ~x53"
```
```   779   and 172: "~x25 | ~x54"
```
```   780   and 173: "~x26 | ~x25"
```
```   781   and 174: "~x26 | ~x55"
```
```   782   and 175: "~x25 | ~x55"
```
```   783   and 176: "~x27 | ~x26"
```
```   784   and 177: "~x27 | ~x56"
```
```   785   and 178: "~x26 | ~x56"
```
```   786   and 179: "~x28 | ~x27"
```
```   787   and 180: "~x28 | ~x57"
```
```   788   and 181: "~x27 | ~x57"
```
```   789   and 182: "~x29 | ~x28"
```
```   790   and 183: "~x29 | ~x58"
```
```   791   and 184: "~x28 | ~x58"
```
```   792   shows "False"
```
```   793     using assms
```
```   794     by argo
```
```   795
```
```   796
```
```   797 text \<open>Translated from TPTP problem library: MSC007-1.008.dimacs\<close>
```
```   798
```
```   799 lemma assumes 1: "x0 | x1 | x2 | x3 | x4 | x5 | x6"
```
```   800   and 2: "x7 | x8 | x9 | x10 | x11 | x12 | x13"
```
```   801   and 3: "x14 | x15 | x16 | x17 | x18 | x19 | x20"
```
```   802   and 4: "x21 | x22 | x23 | x24 | x25 | x26 | x27"
```
```   803   and 5: "x28 | x29 | x30 | x31 | x32 | x33 | x34"
```
```   804   and 6: "x35 | x36 | x37 | x38 | x39 | x40 | x41"
```
```   805   and 7: "x42 | x43 | x44 | x45 | x46 | x47 | x48"
```
```   806   and 8: "x49 | x50 | x51 | x52 | x53 | x54 | x55"
```
```   807   and 9: "~x0 | ~x7"
```
```   808   and 10: "~x0 | ~x14"
```
```   809   and 11: "~x0 | ~x21"
```
```   810   and 12: "~x0 | ~x28"
```
```   811   and 13: "~x0 | ~x35"
```
```   812   and 14: "~x0 | ~x42"
```
```   813   and 15: "~x0 | ~x49"
```
```   814   and 16: "~x7 | ~x14"
```
```   815   and 17: "~x7 | ~x21"
```
```   816   and 18: "~x7 | ~x28"
```
```   817   and 19: "~x7 | ~x35"
```
```   818   and 20: "~x7 | ~x42"
```
```   819   and 21: "~x7 | ~x49"
```
```   820   and 22: "~x14 | ~x21"
```
```   821   and 23: "~x14 | ~x28"
```
```   822   and 24: "~x14 | ~x35"
```
```   823   and 25: "~x14 | ~x42"
```
```   824   and 26: "~x14 | ~x49"
```
```   825   and 27: "~x21 | ~x28"
```
```   826   and 28: "~x21 | ~x35"
```
```   827   and 29: "~x21 | ~x42"
```
```   828   and 30: "~x21 | ~x49"
```
```   829   and 31: "~x28 | ~x35"
```
```   830   and 32: "~x28 | ~x42"
```
```   831   and 33: "~x28 | ~x49"
```
```   832   and 34: "~x35 | ~x42"
```
```   833   and 35: "~x35 | ~x49"
```
```   834   and 36: "~x42 | ~x49"
```
```   835   and 37: "~x1 | ~x8"
```
```   836   and 38: "~x1 | ~x15"
```
```   837   and 39: "~x1 | ~x22"
```
```   838   and 40: "~x1 | ~x29"
```
```   839   and 41: "~x1 | ~x36"
```
```   840   and 42: "~x1 | ~x43"
```
```   841   and 43: "~x1 | ~x50"
```
```   842   and 44: "~x8 | ~x15"
```
```   843   and 45: "~x8 | ~x22"
```
```   844   and 46: "~x8 | ~x29"
```
```   845   and 47: "~x8 | ~x36"
```
```   846   and 48: "~x8 | ~x43"
```
```   847   and 49: "~x8 | ~x50"
```
```   848   and 50: "~x15 | ~x22"
```
```   849   and 51: "~x15 | ~x29"
```
```   850   and 52: "~x15 | ~x36"
```
```   851   and 53: "~x15 | ~x43"
```
```   852   and 54: "~x15 | ~x50"
```
```   853   and 55: "~x22 | ~x29"
```
```   854   and 56: "~x22 | ~x36"
```
```   855   and 57: "~x22 | ~x43"
```
```   856   and 58: "~x22 | ~x50"
```
```   857   and 59: "~x29 | ~x36"
```
```   858   and 60: "~x29 | ~x43"
```
```   859   and 61: "~x29 | ~x50"
```
```   860   and 62: "~x36 | ~x43"
```
```   861   and 63: "~x36 | ~x50"
```
```   862   and 64: "~x43 | ~x50"
```
```   863   and 65: "~x2 | ~x9"
```
```   864   and 66: "~x2 | ~x16"
```
```   865   and 67: "~x2 | ~x23"
```
```   866   and 68: "~x2 | ~x30"
```
```   867   and 69: "~x2 | ~x37"
```
```   868   and 70: "~x2 | ~x44"
```
```   869   and 71: "~x2 | ~x51"
```
```   870   and 72: "~x9 | ~x16"
```
```   871   and 73: "~x9 | ~x23"
```
```   872   and 74: "~x9 | ~x30"
```
```   873   and 75: "~x9 | ~x37"
```
```   874   and 76: "~x9 | ~x44"
```
```   875   and 77: "~x9 | ~x51"
```
```   876   and 78: "~x16 | ~x23"
```
```   877   and 79: "~x16 | ~x30"
```
```   878   and 80: "~x16 | ~x37"
```
```   879   and 81: "~x16 | ~x44"
```
```   880   and 82: "~x16 | ~x51"
```
```   881   and 83: "~x23 | ~x30"
```
```   882   and 84: "~x23 | ~x37"
```
```   883   and 85: "~x23 | ~x44"
```
```   884   and 86: "~x23 | ~x51"
```
```   885   and 87: "~x30 | ~x37"
```
```   886   and 88: "~x30 | ~x44"
```
```   887   and 89: "~x30 | ~x51"
```
```   888   and 90: "~x37 | ~x44"
```
```   889   and 91: "~x37 | ~x51"
```
```   890   and 92: "~x44 | ~x51"
```
```   891   and 93: "~x3 | ~x10"
```
```   892   and 94: "~x3 | ~x17"
```
```   893   and 95: "~x3 | ~x24"
```
```   894   and 96: "~x3 | ~x31"
```
```   895   and 97: "~x3 | ~x38"
```
```   896   and 98: "~x3 | ~x45"
```
```   897   and 99: "~x3 | ~x52"
```
```   898   and 100: "~x10 | ~x17"
```
```   899   and 101: "~x10 | ~x24"
```
```   900   and 102: "~x10 | ~x31"
```
```   901   and 103: "~x10 | ~x38"
```
```   902   and 104: "~x10 | ~x45"
```
```   903   and 105: "~x10 | ~x52"
```
```   904   and 106: "~x17 | ~x24"
```
```   905   and 107: "~x17 | ~x31"
```
```   906   and 108: "~x17 | ~x38"
```
```   907   and 109: "~x17 | ~x45"
```
```   908   and 110: "~x17 | ~x52"
```
```   909   and 111: "~x24 | ~x31"
```
```   910   and 112: "~x24 | ~x38"
```
```   911   and 113: "~x24 | ~x45"
```
```   912   and 114: "~x24 | ~x52"
```
```   913   and 115: "~x31 | ~x38"
```
```   914   and 116: "~x31 | ~x45"
```
```   915   and 117: "~x31 | ~x52"
```
```   916   and 118: "~x38 | ~x45"
```
```   917   and 119: "~x38 | ~x52"
```
```   918   and 120: "~x45 | ~x52"
```
```   919   and 121: "~x4 | ~x11"
```
```   920   and 122: "~x4 | ~x18"
```
```   921   and 123: "~x4 | ~x25"
```
```   922   and 124: "~x4 | ~x32"
```
```   923   and 125: "~x4 | ~x39"
```
```   924   and 126: "~x4 | ~x46"
```
```   925   and 127: "~x4 | ~x53"
```
```   926   and 128: "~x11 | ~x18"
```
```   927   and 129: "~x11 | ~x25"
```
```   928   and 130: "~x11 | ~x32"
```
```   929   and 131: "~x11 | ~x39"
```
```   930   and 132: "~x11 | ~x46"
```
```   931   and 133: "~x11 | ~x53"
```
```   932   and 134: "~x18 | ~x25"
```
```   933   and 135: "~x18 | ~x32"
```
```   934   and 136: "~x18 | ~x39"
```
```   935   and 137: "~x18 | ~x46"
```
```   936   and 138: "~x18 | ~x53"
```
```   937   and 139: "~x25 | ~x32"
```
```   938   and 140: "~x25 | ~x39"
```
```   939   and 141: "~x25 | ~x46"
```
```   940   and 142: "~x25 | ~x53"
```
```   941   and 143: "~x32 | ~x39"
```
```   942   and 144: "~x32 | ~x46"
```
```   943   and 145: "~x32 | ~x53"
```
```   944   and 146: "~x39 | ~x46"
```
```   945   and 147: "~x39 | ~x53"
```
```   946   and 148: "~x46 | ~x53"
```
```   947   and 149: "~x5 | ~x12"
```
```   948   and 150: "~x5 | ~x19"
```
```   949   and 151: "~x5 | ~x26"
```
```   950   and 152: "~x5 | ~x33"
```
```   951   and 153: "~x5 | ~x40"
```
```   952   and 154: "~x5 | ~x47"
```
```   953   and 155: "~x5 | ~x54"
```
```   954   and 156: "~x12 | ~x19"
```
```   955   and 157: "~x12 | ~x26"
```
```   956   and 158: "~x12 | ~x33"
```
```   957   and 159: "~x12 | ~x40"
```
```   958   and 160: "~x12 | ~x47"
```
```   959   and 161: "~x12 | ~x54"
```
```   960   and 162: "~x19 | ~x26"
```
```   961   and 163: "~x19 | ~x33"
```
```   962   and 164: "~x19 | ~x40"
```
```   963   and 165: "~x19 | ~x47"
```
```   964   and 166: "~x19 | ~x54"
```
```   965   and 167: "~x26 | ~x33"
```
```   966   and 168: "~x26 | ~x40"
```
```   967   and 169: "~x26 | ~x47"
```
```   968   and 170: "~x26 | ~x54"
```
```   969   and 171: "~x33 | ~x40"
```
```   970   and 172: "~x33 | ~x47"
```
```   971   and 173: "~x33 | ~x54"
```
```   972   and 174: "~x40 | ~x47"
```
```   973   and 175: "~x40 | ~x54"
```
```   974   and 176: "~x47 | ~x54"
```
```   975   and 177: "~x6 | ~x13"
```
```   976   and 178: "~x6 | ~x20"
```
```   977   and 179: "~x6 | ~x27"
```
```   978   and 180: "~x6 | ~x34"
```
```   979   and 181: "~x6 | ~x41"
```
```   980   and 182: "~x6 | ~x48"
```
```   981   and 183: "~x6 | ~x55"
```
```   982   and 184: "~x13 | ~x20"
```
```   983   and 185: "~x13 | ~x27"
```
```   984   and 186: "~x13 | ~x34"
```
```   985   and 187: "~x13 | ~x41"
```
```   986   and 188: "~x13 | ~x48"
```
```   987   and 189: "~x13 | ~x55"
```
```   988   and 190: "~x20 | ~x27"
```
```   989   and 191: "~x20 | ~x34"
```
```   990   and 192: "~x20 | ~x41"
```
```   991   and 193: "~x20 | ~x48"
```
```   992   and 194: "~x20 | ~x55"
```
```   993   and 195: "~x27 | ~x34"
```
```   994   and 196: "~x27 | ~x41"
```
```   995   and 197: "~x27 | ~x48"
```
```   996   and 198: "~x27 | ~x55"
```
```   997   and 199: "~x34 | ~x41"
```
```   998   and 200: "~x34 | ~x48"
```
```   999   and 201: "~x34 | ~x55"
```
```  1000   and 202: "~x41 | ~x48"
```
```  1001   and 203: "~x41 | ~x55"
```
```  1002   and 204: "~x48 | ~x55"
```
```  1003   shows "False"
```
```  1004     using assms
```
```  1005     by argo
```
```  1006
```
```  1007
```
```  1008 lemma "0 \<le> (yc::real) \<and>
```
```  1009        0 \<le> yd \<and> 0 \<le> yb \<and> 0 \<le> ya \<Longrightarrow>
```
```  1010        0 \<le> yf \<and>
```
```  1011        0 \<le> xh \<and> 0 \<le> ye \<and> 0 \<le> yg \<Longrightarrow>
```
```  1012        0 \<le> yw \<and> 0 \<le> xs \<and> 0 \<le> yu \<Longrightarrow>
```
```  1013        0 \<le> aea \<and> 0 \<le> aee \<and> 0 \<le> aed \<Longrightarrow>
```
```  1014        0 \<le> zy \<and> 0 \<le> xz \<and> 0 \<le> zw \<Longrightarrow>
```
```  1015        0 \<le> zb \<and>
```
```  1016        0 \<le> za \<and> 0 \<le> yy \<and> 0 \<le> yz \<Longrightarrow>
```
```  1017        0 \<le> zp \<and> 0 \<le> zo \<and> 0 \<le> yq \<Longrightarrow>
```
```  1018        0 \<le> adp \<and> 0 \<le> aeb \<and> 0 \<le> aec \<Longrightarrow>
```
```  1019        0 \<le> acm \<and> 0 \<le> aco \<and> 0 \<le> acn \<Longrightarrow>
```
```  1020        0 \<le> abl \<Longrightarrow>
```
```  1021        0 \<le> zr \<and> 0 \<le> zq \<and> 0 \<le> abh \<Longrightarrow>
```
```  1022        0 \<le> abq \<and> 0 \<le> zd \<and> 0 \<le> abo \<Longrightarrow>
```
```  1023        0 \<le> acd \<and>
```
```  1024        0 \<le> acc \<and> 0 \<le> xi \<and> 0 \<le> acb \<Longrightarrow>
```
```  1025        0 \<le> acp \<and> 0 \<le> acr \<and> 0 \<le> acq \<Longrightarrow>
```
```  1026        0 \<le> xw \<and>
```
```  1027        0 \<le> xr \<and> 0 \<le> xv \<and> 0 \<le> xu \<Longrightarrow>
```
```  1028        0 \<le> zc \<and> 0 \<le> acg \<and> 0 \<le> ach \<Longrightarrow>
```
```  1029        0 \<le> zt \<and> 0 \<le> zs \<and> 0 \<le> xy \<Longrightarrow>
```
```  1030        0 \<le> ady \<and> 0 \<le> adw \<and> 0 \<le> zg \<Longrightarrow>
```
```  1031        0 \<le> abd \<and>
```
```  1032        0 \<le> abc \<and> 0 \<le> yr \<and> 0 \<le> abb \<Longrightarrow>
```
```  1033        0 \<le> adi \<and>
```
```  1034        0 \<le> x \<and> 0 \<le> adh \<and> 0 \<le> xa \<Longrightarrow>
```
```  1035        0 \<le> aak \<and> 0 \<le> aai \<and> 0 \<le> aad \<Longrightarrow>
```
```  1036        0 \<le> aba \<and> 0 \<le> zh \<and> 0 \<le> aay \<Longrightarrow>
```
```  1037        0 \<le> abg \<and> 0 \<le> ys \<and> 0 \<le> abe \<Longrightarrow>
```
```  1038        0 \<le> abs1 \<and>
```
```  1039        0 \<le> yt \<and> 0 \<le> abr \<and> 0 \<le> zu \<Longrightarrow>
```
```  1040        0 \<le> abv \<and>
```
```  1041        0 \<le> zn \<and> 0 \<le> abw \<and> 0 \<le> zm \<Longrightarrow>
```
```  1042        0 \<le> adl \<and> 0 \<le> adn \<Longrightarrow>
```
```  1043        0 \<le> acf \<and> 0 \<le> aca \<Longrightarrow>
```
```  1044        0 \<le> ads \<and> 0 \<le> aaq \<Longrightarrow>
```
```  1045        0 \<le> ada \<Longrightarrow>
```
```  1046        0 \<le> aaf \<and> 0 \<le> aac \<and> 0 \<le> aag \<Longrightarrow>
```
```  1047        0 \<le> aal \<and>
```
```  1048        0 \<le> acu \<and> 0 \<le> acs \<and> 0 \<le> act \<Longrightarrow>
```
```  1049        0 \<le> aas \<and> 0 \<le> xb \<and> 0 \<le> aat \<Longrightarrow>
```
```  1050        0 \<le> zk \<and> 0 \<le> zj \<and> 0 \<le> zi \<Longrightarrow>
```
```  1051        0 \<le> ack \<and>
```
```  1052        0 \<le> acj \<and> 0 \<le> xc \<and> 0 \<le> aci \<Longrightarrow>
```
```  1053        0 \<le> aav \<and> 0 \<le> aah \<and> 0 \<le> xd \<Longrightarrow>
```
```  1054        0 \<le> abt \<and>
```
```  1055        0 \<le> xo \<and> 0 \<le> abu \<and> 0 \<le> xn \<Longrightarrow>
```
```  1056        0 \<le> adc \<and>
```
```  1057        0 \<le> abz \<and> 0 \<le> adc \<and> 0 \<le> abz \<Longrightarrow>
```
```  1058        0 \<le> xt \<and>
```
```  1059        0 \<le> zz \<and> 0 \<le> aab \<and> 0 \<le> aaa \<Longrightarrow>
```
```  1060        0 \<le> adq \<and>
```
```  1061        0 \<le> xl \<and> 0 \<le> adr \<and> 0 \<le> adb \<Longrightarrow>
```
```  1062        0 \<le> zf \<and> 0 \<le> yh \<and> 0 \<le> yi \<Longrightarrow>
```
```  1063        0 \<le> aao \<and> 0 \<le> aam \<and> 0 \<le> xe \<Longrightarrow>
```
```  1064        0 \<le> abk \<and>
```
```  1065        0 \<le> aby \<and> 0 \<le> abj \<and> 0 \<le> abx \<Longrightarrow>
```
```  1066        0 \<le> yp \<Longrightarrow>
```
```  1067        0 \<le> yl \<and> 0 \<le> yj \<and> 0 \<le> ym \<Longrightarrow>
```
```  1068        0 \<le> acw \<Longrightarrow>
```
```  1069        0 \<le> adk \<and>
```
```  1070        0 \<le> adg \<and> 0 \<le> adj \<and> 0 \<le> adf \<Longrightarrow>
```
```  1071        0 \<le> adv \<and> 0 \<le> xf \<and> 0 \<le> adu \<Longrightarrow>
```
```  1072        yc + yd + yb + ya = 1 \<Longrightarrow>
```
```  1073        yf + xh + ye + yg = 1 \<Longrightarrow>
```
```  1074        yw + xs + yu = 1 \<Longrightarrow>
```
```  1075        aea + aee + aed = 1 \<Longrightarrow>
```
```  1076        zy + xz + zw = 1 \<Longrightarrow>
```
```  1077        zb + za + yy + yz = 1 \<Longrightarrow>
```
```  1078        zp + zo + yq = 1 \<Longrightarrow>
```
```  1079        adp + aeb + aec = 1 \<Longrightarrow>
```
```  1080        acm + aco + acn = 1 \<Longrightarrow>
```
```  1081        abl + abl = 1 \<Longrightarrow>
```
```  1082        zr + zq + abh = 1 \<Longrightarrow>
```
```  1083        abq + zd + abo = 1 \<Longrightarrow>
```
```  1084        acd + acc + xi + acb = 1 \<Longrightarrow>
```
```  1085        acp + acr + acq = 1 \<Longrightarrow>
```
```  1086        xw + xr + xv + xu = 1 \<Longrightarrow>
```
```  1087        zc + acg + ach = 1 \<Longrightarrow>
```
```  1088        zt + zs + xy = 1 \<Longrightarrow>
```
```  1089        ady + adw + zg = 1 \<Longrightarrow>
```
```  1090        abd + abc + yr + abb = 1 \<Longrightarrow>
```
```  1091        adi + x + adh + xa = 1 \<Longrightarrow>
```
```  1092        aak + aai + aad = 1 \<Longrightarrow>
```
```  1093        aba + zh + aay = 1 \<Longrightarrow>
```
```  1094        abg + ys + abe = 1 \<Longrightarrow>
```
```  1095        abs1 + yt + abr + zu = 1 \<Longrightarrow>
```
```  1096        abv + zn + abw + zm = 1 \<Longrightarrow>
```
```  1097        adl + adn = 1 \<Longrightarrow>
```
```  1098        acf + aca = 1 \<Longrightarrow>
```
```  1099        ads + aaq = 1 \<Longrightarrow>
```
```  1100        ada + ada = 1 \<Longrightarrow>
```
```  1101        aaf + aac + aag = 1 \<Longrightarrow>
```
```  1102        aal + acu + acs + act = 1 \<Longrightarrow>
```
```  1103        aas + xb + aat = 1 \<Longrightarrow>
```
```  1104        zk + zj + zi = 1 \<Longrightarrow>
```
```  1105        ack + acj + xc + aci = 1 \<Longrightarrow>
```
```  1106        aav + aah + xd = 1 \<Longrightarrow>
```
```  1107        abt + xo + abu + xn = 1 \<Longrightarrow>
```
```  1108        adc + abz + adc + abz = 1 \<Longrightarrow>
```
```  1109        xt + zz + aab + aaa = 1 \<Longrightarrow>
```
```  1110        adq + xl + adr + adb = 1 \<Longrightarrow>
```
```  1111        zf + yh + yi = 1 \<Longrightarrow>
```
```  1112        aao + aam + xe = 1 \<Longrightarrow>
```
```  1113        abk + aby + abj + abx = 1 \<Longrightarrow>
```
```  1114        yp + yp = 1 \<Longrightarrow>
```
```  1115        yl + yj + ym = 1 \<Longrightarrow>
```
```  1116        acw + acw + acw + acw = 1 \<Longrightarrow>
```
```  1117        adk + adg + adj + adf = 1 \<Longrightarrow>
```
```  1118        adv + xf + adu = 1 \<Longrightarrow>
```
```  1119        yd = 0 \<or> yb = 0 \<Longrightarrow>
```
```  1120        xh = 0 \<or> ye = 0 \<Longrightarrow>
```
```  1121        yy = 0 \<or> za = 0 \<Longrightarrow>
```
```  1122        acc = 0 \<or> xi = 0 \<Longrightarrow>
```
```  1123        xv = 0 \<or> xr = 0 \<Longrightarrow>
```
```  1124        yr = 0 \<or> abc = 0 \<Longrightarrow>
```
```  1125        zn = 0 \<or> abw = 0 \<Longrightarrow>
```
```  1126        xo = 0 \<or> abu = 0 \<Longrightarrow>
```
```  1127        xl = 0 \<or> adr = 0 \<Longrightarrow>
```
```  1128        (yr + abd < abl \<or>
```
```  1129         yr + (abd + abb) < 1) \<or>
```
```  1130        yr + abd = abl \<and>
```
```  1131        yr + (abd + abb) = 1 \<Longrightarrow>
```
```  1132        adb + adr < xn + abu \<or>
```
```  1133        adb + adr = xn + abu \<Longrightarrow>
```
```  1134        (abl < abt \<or> abl < abt + xo) \<or>
```
```  1135        abl = abt \<and> abl = abt + xo \<Longrightarrow>
```
```  1136        yd + yc < abc + abd \<or>
```
```  1137        yd + yc = abc + abd \<Longrightarrow>
```
```  1138        aca < abb + yr \<or> aca = abb + yr \<Longrightarrow>
```
```  1139        acb + acc < xu + xv \<or>
```
```  1140        acb + acc = xu + xv \<Longrightarrow>
```
```  1141        (yq < xu + xr \<or>
```
```  1142         yq + zp < xu + (xr + xw)) \<or>
```
```  1143        yq = xu + xr \<and>
```
```  1144        yq + zp = xu + (xr + xw) \<Longrightarrow>
```
```  1145        (zw < xw \<or>
```
```  1146         zw < xw + xv \<or>
```
```  1147         zw + zy < xw + (xv + xu)) \<or>
```
```  1148        zw = xw \<and>
```
```  1149        zw = xw + xv \<and>
```
```  1150        zw + zy = xw + (xv + xu) \<Longrightarrow>
```
```  1151        xs + yw < zs + zt \<or>
```
```  1152        xs + yw = zs + zt \<Longrightarrow>
```
```  1153        aab + xt < ye + yf \<or>
```
```  1154        aab + xt = ye + yf \<Longrightarrow>
```
```  1155        (ya + yb < yg + ye \<or>
```
```  1156         ya + (yb + yc) < yg + (ye + yf)) \<or>
```
```  1157        ya + yb = yg + ye \<and>
```
```  1158        ya + (yb + yc) = yg + (ye + yf) \<Longrightarrow>
```
```  1159        (xu + xv < acb + acc \<or>
```
```  1160         xu + (xv + xw) < acb + (acc + acd)) \<or>
```
```  1161        xu + xv = acb + acc \<and>
```
```  1162        xu + (xv + xw) = acb + (acc + acd) \<Longrightarrow>
```
```  1163        (zs < xz + zy \<or>
```
```  1164         zs + xy < xz + (zy + zw)) \<or>
```
```  1165        zs = xz + zy \<and>
```
```  1166        zs + xy = xz + (zy + zw) \<Longrightarrow>
```
```  1167        (zs + zt < xz + zy \<or>
```
```  1168         zs + (zt + xy) < xz + (zy + zw)) \<or>
```
```  1169        zs + zt = xz + zy \<and>
```
```  1170        zs + (zt + xy) = xz + (zy + zw) \<Longrightarrow>
```
```  1171        yg + ye < ya + yb \<or>
```
```  1172        yg + ye = ya + yb \<Longrightarrow>
```
```  1173        (abd < yc \<or> abd + abc < yc + yd) \<or>
```
```  1174        abd = yc \<and> abd + abc = yc + yd \<Longrightarrow>
```
```  1175        (ye + yf < adr + adq \<or>
```
```  1176         ye + (yf + yg) < adr + (adq + adb)) \<or>
```
```  1177        ye + yf = adr + adq \<and>
```
```  1178        ye + (yf + yg) = adr + (adq + adb) \<Longrightarrow>
```
```  1179        yh + yi < ym + yj \<or>
```
```  1180        yh + yi = ym + yj \<Longrightarrow>
```
```  1181        (abq < yl \<or> abq + abo < yl + ym) \<or>
```
```  1182        abq = yl \<and> abq + abo = yl + ym \<Longrightarrow>
```
```  1183        (yp < zp \<or>
```
```  1184         yp < zp + zo \<or> 1 < zp + (zo + yq)) \<or>
```
```  1185        yp = zp \<and>
```
```  1186        yp = zp + zo \<and> 1 = zp + (zo + yq) \<Longrightarrow>
```
```  1187        (abb + yr < aca \<or>
```
```  1188         abb + (yr + abd) < aca + acf) \<or>
```
```  1189        abb + yr = aca \<and>
```
```  1190        abb + (yr + abd) = aca + acf \<Longrightarrow>
```
```  1191        adw + zg < abe + ys \<or>
```
```  1192        adw + zg = abe + ys \<Longrightarrow>
```
```  1193        zd + abq < ys + abg \<or>
```
```  1194        zd + abq = ys + abg \<Longrightarrow>
```
```  1195        yt + abs1 < aby + abk \<or>
```
```  1196        yt + abs1 = aby + abk \<Longrightarrow>
```
```  1197        (yu < abx \<or>
```
```  1198         yu < abx + aby \<or>
```
```  1199         yu + yw < abx + (aby + abk)) \<or>
```
```  1200        yu = abx \<and>
```
```  1201        yu = abx + aby \<and>
```
```  1202        yu + yw = abx + (aby + abk) \<Longrightarrow>
```
```  1203        aaf < adv \<or> aaf = adv \<Longrightarrow>
```
```  1204        abj + abk < yy + zb \<or>
```
```  1205        abj + abk = yy + zb \<Longrightarrow>
```
```  1206        (abb < yz \<or>
```
```  1207         abb + abc < yz + za \<or>
```
```  1208         abb + (abc + abd) < yz + (za + zb)) \<or>
```
```  1209        abb = yz \<and>
```
```  1210        abb + abc = yz + za \<and>
```
```  1211        abb + (abc + abd) = yz + (za + zb) \<Longrightarrow>
```
```  1212        (acg + zc < zd + abq \<or>
```
```  1213         acg + (zc + ach)
```
```  1214         < zd + (abq + abo)) \<or>
```
```  1215        acg + zc = zd + abq \<and>
```
```  1216        acg + (zc + ach) =
```
```  1217        zd + (abq + abo) \<Longrightarrow>
```
```  1218        zf < acm \<or> zf = acm \<Longrightarrow>
```
```  1219        (zg + ady < acn + acm \<or>
```
```  1220         zg + (ady + adw)
```
```  1221         < acn + (acm + aco)) \<or>
```
```  1222        zg + ady = acn + acm \<and>
```
```  1223        zg + (ady + adw) =
```
```  1224        acn + (acm + aco) \<Longrightarrow>
```
```  1225        aay + zh < zi + zj \<or>
```
```  1226        aay + zh = zi + zj \<Longrightarrow>
```
```  1227        zy < zk \<or> zy = zk \<Longrightarrow>
```
```  1228        (adn < zm + zn \<or>
```
```  1229         adn + adl < zm + (zn + abv)) \<or>
```
```  1230        adn = zm + zn \<and>
```
```  1231        adn + adl = zm + (zn + abv) \<Longrightarrow>
```
```  1232        zo + zp < zs + zt \<or>
```
```  1233        zo + zp = zs + zt \<Longrightarrow>
```
```  1234        zq + zr < zs + zt \<or>
```
```  1235        zq + zr = zs + zt \<Longrightarrow>
```
```  1236        (aai < adi \<or> aai < adi + adh) \<or>
```
```  1237        aai = adi \<and> aai = adi + adh \<Longrightarrow>
```
```  1238        (abr < acj \<or>
```
```  1239         abr + (abs1 + zu)
```
```  1240         < acj + (aci + ack)) \<or>
```
```  1241        abr = acj \<and>
```
```  1242        abr + (abs1 + zu) =
```
```  1243        acj + (aci + ack) \<Longrightarrow>
```
```  1244        (abl < zw \<or> 1 < zw + zy) \<or>
```
```  1245        abl = zw \<and> 1 = zw + zy \<Longrightarrow>
```
```  1246        (zz + aaa < act + acu \<or>
```
```  1247         zz + (aaa + aab)
```
```  1248         < act + (acu + aal)) \<or>
```
```  1249        zz + aaa = act + acu \<and>
```
```  1250        zz + (aaa + aab) =
```
```  1251        act + (acu + aal) \<Longrightarrow>
```
```  1252        (aam < aac \<or> aam + aao < aac + aaf) \<or>
```
```  1253        aam = aac \<and> aam + aao = aac + aaf \<Longrightarrow>
```
```  1254        (aak < aaf \<or> aak + aad < aaf + aag) \<or>
```
```  1255        aak = aaf \<and> aak + aad = aaf + aag \<Longrightarrow>
```
```  1256        (aah < aai \<or> aah + aav < aai + aak) \<or>
```
```  1257        aah = aai \<and> aah + aav = aai + aak \<Longrightarrow>
```
```  1258        act + (acu + aal) < aam + aao \<or>
```
```  1259        act + (acu + aal) = aam + aao \<Longrightarrow>
```
```  1260        (ads < aat \<or> 1 < aat + aas) \<or>
```
```  1261        ads = aat \<and> 1 = aat + aas \<Longrightarrow>
```
```  1262        (aba < aas \<or> aba + aay < aas + aat) \<or>
```
```  1263        aba = aas \<and> aba + aay = aas + aat \<Longrightarrow>
```
```  1264        acm < aav \<or> acm = aav \<Longrightarrow>
```
```  1265        (ada < aay \<or> 1 < aay + aba) \<or>
```
```  1266        ada = aay \<and> 1 = aay + aba \<Longrightarrow>
```
```  1267        abb + (abc + abd) < abe + abg \<or>
```
```  1268        abb + (abc + abd) = abe + abg \<Longrightarrow>
```
```  1269        (abh < abj \<or> abh < abj + abk) \<or>
```
```  1270        abh = abj \<and> abh = abj + abk \<Longrightarrow>
```
```  1271        1 < abo + abq \<or> 1 = abo + abq \<Longrightarrow>
```
```  1272        (acj < abr \<or> acj + aci < abr + abs1) \<or>
```
```  1273        acj = abr \<and> acj + aci = abr + abs1 \<Longrightarrow>
```
```  1274        (abt < abv \<or> abt + abu < abv + abw) \<or>
```
```  1275        abt = abv \<and> abt + abu = abv + abw \<Longrightarrow>
```
```  1276        (abx < adc \<or> abx + aby < adc + abz) \<or>
```
```  1277        abx = adc \<and> abx + aby = adc + abz \<Longrightarrow>
```
```  1278        (acf < acd \<or>
```
```  1279         acf < acd + acc \<or>
```
```  1280         1 < acd + (acc + acb)) \<or>
```
```  1281        acf = acd \<and>
```
```  1282        acf = acd + acc \<and>
```
```  1283        1 = acd + (acc + acb) \<Longrightarrow>
```
```  1284        acc + acd < acf \<or> acc + acd = acf \<Longrightarrow>
```
```  1285        (acg < acq \<or> acg + ach < acq + acr) \<or>
```
```  1286        acg = acq \<and> acg + ach = acq + acr \<Longrightarrow>
```
```  1287        aci + (acj + ack) < acr + acp \<or>
```
```  1288        aci + (acj + ack) = acr + acp \<Longrightarrow>
```
```  1289        (acm < acp \<or>
```
```  1290         acm + acn < acp + acq \<or>
```
```  1291         acm + (acn + aco)
```
```  1292         < acp + (acq + acr)) \<or>
```
```  1293        acm = acp \<and>
```
```  1294        acm + acn = acp + acq \<and>
```
```  1295        acm + (acn + aco) =
```
```  1296        acp + (acq + acr) \<Longrightarrow>
```
```  1297        (acs + act < acw + acw \<or>
```
```  1298         acs + (act + acu)
```
```  1299         < acw + (acw + acw)) \<or>
```
```  1300        acs + act = acw + acw \<and>
```
```  1301        acs + (act + acu) =
```
```  1302        acw + (acw + acw) \<Longrightarrow>
```
```  1303        (ada < adb + adr \<or>
```
```  1304         1 < adb + (adr + adq)) \<or>
```
```  1305        ada = adb + adr \<and>
```
```  1306        1 = adb + (adr + adq) \<Longrightarrow>
```
```  1307        (adc + adc < adf + adg \<or>
```
```  1308         adc + (adc + abz)
```
```  1309         < adf + (adg + adk)) \<or>
```
```  1310        adc + adc = adf + adg \<and>
```
```  1311        adc + (adc + abz) =
```
```  1312        adf + (adg + adk) \<Longrightarrow>
```
```  1313        adh + adi < adj + adk \<or>
```
```  1314        adh + adi = adj + adk \<Longrightarrow>
```
```  1315        (adl < aec \<or> 1 < aec + adp) \<or>
```
```  1316        adl = aec \<and> 1 = aec + adp \<Longrightarrow>
```
```  1317        (adq < ads \<or> adq + adr < ads) \<or>
```
```  1318        adq = ads \<and> adq + adr = ads \<Longrightarrow>
```
```  1319        adu + adv < aed + aea \<or>
```
```  1320        adu + adv = aed + aea \<Longrightarrow>
```
```  1321        (adw < aee \<or> adw + ady < aee + aea) \<or>
```
```  1322        adw = aee \<and> adw + ady = aee + aea \<Longrightarrow>
```
```  1323        (aeb < aed \<or> aeb + aec < aed + aee) \<or>
```
```  1324        aeb = aed \<and> aeb + aec = aed + aee \<Longrightarrow>
```
```  1325        False"
```
```  1326        by argo
```
```  1327
```
```  1328 end
```