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