src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.certs

clarified code setup

35b253bd6d27f6991af73e29ed1030cb74b50ab2 11 0
unsat
(assume conjecture0 (not (! (= (! (- c$ b$) :named @p_2) a$) :named @p_1)))
(assume hypothesis1 (! (= c$ (+ a$ b$)) :named @p_6))
(step t3 (cl (or @p_1 (! (not (! (<= @p_2 a$) :named @p_5)) :named @p_3) (! (not (! (<= a$ @p_2) :named @p_7)) :named @p_4))) :rule la_disequality)
(step t4 (cl @p_1 @p_3 @p_4) :rule or :premises (t3))
(step t5 (cl @p_3 @p_4) :rule resolution :premises (t4 conjecture0))
(step t6 (cl @p_5 (! (not @p_6) :named @p_8)) :rule la_generic :args (1 (- 1)))
(step t7 (cl @p_5) :rule resolution :premises (t6 hypothesis1))
(step t8 (cl @p_4) :rule resolution :premises (t5 t7))
(step t9 (cl @p_7 @p_8) :rule la_generic :args (1 1))
(step t10 (cl) :rule resolution :premises (t9 hypothesis1 t8))
882414839a017a484227974e42bc9854cb971d88 49 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x49 (* (- 1) a$)))
(let ((?x36 (* (- 1) b$)))
(let ((?x50 (+ c$ ?x36 ?x49)))
(let (($x92 (= ?x50 0)))
(let (($x114 (not $x92)))
(let ((@x128 (rewrite (= (not true) false))))
(let (($x55 (>= ?x50 0)))
(let (($x89 (not $x55)))
(let (($x51 (<= ?x50 0)))
(let (($x86 (not $x51)))
(let (($x101 (or $x92 $x86 $x89)))
(let (($x57 (and $x51 $x55)))
(let ((@x59 (monotonicity (rewrite (= (<= (+ c$ ?x36) a$) $x51)) (rewrite (= (<= a$ (+ c$ ?x36)) $x55)) (= (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36))) $x57))))
(let ((?x29 (- c$ b$)))
(let (($x32 (<= a$ ?x29)))
(let (($x31 (<= ?x29 a$)))
(let (($x33 (and $x31 $x32)))
(let ((@x39 (rewrite (= ?x29 (+ c$ ?x36)))))
(let ((@x48 (monotonicity (monotonicity @x39 (= $x31 (<= (+ c$ ?x36) a$))) (monotonicity @x39 (= $x32 (<= a$ (+ c$ ?x36)))) (= $x33 (and (<= (+ c$ ?x36) a$) (<= a$ (+ c$ ?x36)))))))
(let ((@x64 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x55)))
(let ((@x132 (monotonicity (iff-true @x64 (= $x55 true)) (= $x89 (not true)))))
(let ((@x63 (and-elim (mp (asserted $x33) (trans @x48 @x59 (= $x33 $x57)) $x57) $x51)))
(let ((@x126 (monotonicity (iff-true @x63 (= $x51 true)) (= $x86 (not true)))))
(let ((@x137 (monotonicity (trans @x126 @x128 (= $x86 false)) (trans @x132 @x128 (= $x89 false)) (= $x101 (or $x92 false false)))))
(let ((@x141 (trans @x137 (rewrite (= (or $x92 false false) $x92)) (= $x101 $x92))))
(let ((?x37 (+ c$ ?x36)))
(let (($x43 (<= a$ ?x37)))
(let (($x77 (not $x43)))
(let (($x40 (<= ?x37 a$)))
(let (($x74 (not $x40)))
(let (($x80 (or $x74 $x77)))
(let (($x71 (= ?x37 a$)))
(let (($x83 (or $x71 $x80)))
(let ((@x97 (monotonicity (monotonicity (rewrite (= $x40 $x51)) (= $x74 $x86)) (monotonicity (rewrite (= $x43 $x55)) (= $x77 $x89)) (= $x80 (or $x86 $x89)))))
(let ((@x100 (monotonicity (rewrite (= $x71 $x92)) @x97 (= $x83 (or $x92 (or $x86 $x89))))))
(let ((@x105 (trans @x100 (rewrite (= (or $x92 (or $x86 $x89)) $x101)) (= $x83 $x101))))
(let ((@x79 (monotonicity (monotonicity @x39 (= $x32 $x43)) (= (not $x32) $x77))))
(let ((@x76 (monotonicity (monotonicity @x39 (= $x31 $x40)) (= (not $x31) $x74))))
(let ((@x85 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (monotonicity @x76 @x79 (= (or (not $x31) (not $x32)) $x80)) (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x83))))
(let ((@x107 (trans @x85 @x105 (= (or (= ?x29 a$) (or (not $x31) (not $x32))) $x101))))
(let ((@x108 (mp (asserted (or (= ?x29 a$) (or (not $x31) (not $x32)))) @x107 $x101)))
(let ((@x146 (monotonicity (iff-true (mp @x108 @x141 $x92) (= $x92 true)) (= $x114 (not true)))))
(let ((@x113 (monotonicity (monotonicity @x39 (= (= ?x29 a$) $x71)) (= (not (= ?x29 a$)) (not $x71)))))
(let ((@x118 (trans @x113 (monotonicity (rewrite (= $x71 $x92)) (= (not $x71) $x114)) (= (not (= ?x29 a$)) $x114))))
(mp (mp (asserted (not (= ?x29 a$))) @x118 $x114) (trans @x146 @x128 (= $x114 false)) false)))))))))))))))))))))))))))))))))))))))))))))))

f2541774823d4fd4ada0de04dcf1ccc81465be15 38 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x69 (* (- 1) a$)))
(let ((?x41 (* (- 1) b$)))
(let ((?x70 (+ c$ ?x41 ?x69)))
(let (($x78 (>= ?x70 0)))
(let (($x80 (not $x78)))
(let (($x71 (<= ?x70 0)))
(let (($x74 (not $x71)))
(let (($x83 (= ?x70 0)))
(let (($x92 (or $x83 $x74 $x80)))
(let (($x97 (not $x92)))
(let (($x37 (or (= (- c$ b$) a$) (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))))))
(let (($x38 (not $x37)))
(let ((?x42 (+ c$ ?x41)))
(let (($x54 (<= a$ ?x42)))
(let (($x57 (not $x54)))
(let (($x48 (<= ?x42 a$)))
(let (($x51 (not $x48)))
(let (($x60 (or $x51 $x57)))
(let (($x45 (= ?x42 a$)))
(let (($x63 (or $x45 $x60)))
(let ((@x88 (monotonicity (monotonicity (rewrite (= $x48 $x71)) (= $x51 $x74)) (monotonicity (rewrite (= $x54 $x78)) (= $x57 $x80)) (= $x60 (or $x74 $x80)))))
(let ((@x91 (monotonicity (rewrite (= $x45 $x83)) @x88 (= $x63 (or $x83 (or $x74 $x80))))))
(let ((@x96 (trans @x91 (rewrite (= (or $x83 (or $x74 $x80)) $x92)) (= $x63 $x92))))
(let (($x61 (= (or (not (<= (- c$ b$) a$)) (not (<= a$ (- c$ b$)))) $x60)))
(let ((@x44 (rewrite (= (- c$ b$) ?x42))))
(let ((@x59 (monotonicity (monotonicity @x44 (= (<= a$ (- c$ b$)) $x54)) (= (not (<= a$ (- c$ b$))) $x57))))
(let ((@x53 (monotonicity (monotonicity @x44 (= (<= (- c$ b$) a$) $x48)) (= (not (<= (- c$ b$) a$)) $x51))))
(let ((@x65 (monotonicity (monotonicity @x44 (= (= (- c$ b$) a$) $x45)) (monotonicity @x53 @x59 $x61) (= $x37 $x63))))
(let ((@x101 (trans (monotonicity @x65 (= $x38 (not $x63))) (monotonicity @x96 (= (not $x63) $x97)) (= $x38 $x97))))
(let ((@x102 (mp (asserted $x38) @x101 $x97)))
(let ((@x106 (not-or-elim @x102 $x78)))
(let ((@x104 (not-or-elim @x102 (not $x83))))
(let ((@x105 (not-or-elim @x102 $x71)))
(unit-resolution ((_ th-lemma arith triangle-eq) $x92) @x105 @x104 @x106 false))))))))))))))))))))))))))))))))))))

38c94308bfb0b4491339a6c117e29fba807f290a 27 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x41 (* (- 1) c$)))
(let ((?x42 (+ a$ ?x41 b$)))
(let (($x43 (<= ?x42 0)))
(let (($x55 (>= ?x42 0)))
(let (($x69 (and $x55 $x43)))
(let (($x72 (not $x69)))
(let ((@x40 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) (<= a$ (+ c$ (* (- 1) b$)))))))
(let ((@x47 (trans @x40 (rewrite (= (<= a$ (+ c$ (* (- 1) b$))) $x43)) (= (<= a$ (- c$ b$)) $x43))))
(let ((@x79 (iff-true (mp (asserted (<= a$ (- c$ b$))) @x47 $x43) (= $x43 true))))
(let ((@x53 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) (<= (+ c$ (* (- 1) b$)) a$)))))
(let ((@x58 (trans @x53 (rewrite (= (<= (+ c$ (* (- 1) b$)) a$) $x55)) (= (<= (- c$ b$) a$) $x55))))
(let ((@x81 (iff-true (mp (asserted (<= (- c$ b$) a$)) @x58 $x55) (= $x55 true))))
(let ((@x88 (trans (monotonicity @x81 @x79 (= $x69 (and true true))) (rewrite (= (and true true) true)) (= $x69 true))))
(let ((@x95 (trans (monotonicity @x88 (= $x72 (not true))) (rewrite (= (not true) false)) (= $x72 false))))
(let (($x61 (not (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))))))
(let ((?x35 (+ c$ (* (- 1) b$))))
(let (($x38 (<= a$ ?x35)))
(let (($x51 (<= ?x35 a$)))
(let (($x63 (and $x51 $x38)))
(let ((@x71 (monotonicity (rewrite (= $x51 $x55)) (rewrite (= $x38 $x43)) (= $x63 $x69))))
(let ((@x65 (monotonicity @x53 @x40 (= (and (<= (- c$ b$) a$) (<= a$ (- c$ b$))) $x63))))
(let ((@x76 (trans (monotonicity @x65 (= $x61 (not $x63))) (monotonicity @x71 (= (not $x63) $x72)) (= $x61 $x72))))
(mp (mp (asserted $x61) @x76 $x72) @x95 false)))))))))))))))))))))))))

d40f5f06cb71bf04976dfbd768e98729d8a02410 29 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x36 (* (- 1) c$)))
(let ((?x37 (+ a$ b$ ?x36)))
(let (($x56 (<= ?x37 0)))
(let (($x38 (= ?x37 0)))
(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
(let ((@x96 (trans (monotonicity @x89 (= (or $x56 (not $x38)) (or $x56 false))) (rewrite (= (or $x56 false) $x56)) (= (or $x56 (not $x38)) $x56))))
(let (($x61 (not $x38)))
(let (($x64 (or $x56 $x61)))
(let (($x43 (not (= c$ (+ a$ b$)))))
(let (($x34 (<= a$ (- c$ b$))))
(let (($x44 (or $x34 $x43)))
(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
(let ((@x66 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) @x63 (= (or (<= a$ (+ (* (- 1) b$) c$)) $x43) $x64))))
(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= a$ (+ (* (- 1) b$) c$))))))
(let ((@x55 (monotonicity @x52 (= $x44 (or (<= a$ (+ (* (- 1) b$) c$)) $x43)))))
(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x56)))
(let ((@x101 (monotonicity (iff-true @x97 (= $x56 true)) (= (not $x56) (not true)))))
(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x56) false))))
(let (($x75 (not $x56)))
(let ((@x77 (monotonicity (rewrite (= (<= a$ (+ (* (- 1) b$) c$)) $x56)) (= (not (<= a$ (+ (* (- 1) b$) c$))) $x75))))
(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= a$ (+ (* (- 1) b$) c$)))))))
(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
(mp @x80 @x103 false)))))))))))))))))))))))))))

589302410c98bf9494c2b8bba0d198d5d6fb8f30 22 0
unsat
((set-logic AUFLIA)
(proof
(let (($x58 (= (+ a$ (* (- 1) c$) b$) 0)))
(let (($x66 (not (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58)))))
(let (($x36 (not (or (<= a$ (- c$ b$)) (not (= c$ (+ a$ b$)))))))
(let (($x34 (not (= c$ (+ a$ b$)))))
(let (($x43 (<= a$ (+ c$ (* (- 1) b$)))))
(let (($x46 (or $x43 $x34)))
(let ((@x62 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x58)) (= $x34 (not $x58)))))
(let ((@x65 (monotonicity (rewrite (= $x43 (<= (+ a$ (* (- 1) c$) b$) 0))) @x62 (= $x46 (or (<= (+ a$ (* (- 1) c$) b$) 0) (not $x58))))))
(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= a$ (- c$ b$)) $x43))))
(let ((@x51 (monotonicity (monotonicity @x45 (= (or (<= a$ (- c$ b$)) $x34) $x46)) (= $x36 (not $x46)))))
(let ((@x70 (trans @x51 (monotonicity @x65 (= (not $x46) $x66)) (= $x36 $x66))))
(let ((@x75 (monotonicity (not-or-elim (mp (asserted $x36) @x70 $x66) $x58) (= (<= (+ a$ (* (- 1) c$) b$) 0) (<= 0 0)))))
(let ((@x81 (trans @x75 (rewrite (= (<= 0 0) true)) (= (<= (+ a$ (* (- 1) c$) b$) 0) true))))
(let ((@x84 (monotonicity @x81 (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) (not true)))))
(let ((@x88 (trans @x84 (rewrite (= (not true) false)) (= (not (<= (+ a$ (* (- 1) c$) b$) 0)) false))))
(let (($x54 (<= (+ a$ (* (- 1) c$) b$) 0)))
(let (($x72 (not $x54)))
(mp (not-or-elim (mp (asserted $x36) @x70 $x66) $x72) @x88 false))))))))))))))))))))

a19eb65c252ea63e4442473afd12fc3c9abc7d26 29 0
unsat
((set-logic AUFLIA)
(proof
(let ((?x36 (* (- 1) c$)))
(let ((?x37 (+ a$ b$ ?x36)))
(let (($x57 (>= ?x37 0)))
(let (($x38 (= ?x37 0)))
(let ((@x41 (mp (asserted (= (+ a$ b$) c$)) (rewrite (= (= (+ a$ b$) c$) $x38)) $x38)))
(let ((@x85 (monotonicity (iff-true @x41 (= $x38 true)) (= (not $x38) (not true)))))
(let ((@x89 (trans @x85 (rewrite (= (not true) false)) (= (not $x38) false))))
(let ((@x96 (trans (monotonicity @x89 (= (or $x57 (not $x38)) (or $x57 false))) (rewrite (= (or $x57 false) $x57)) (= (or $x57 (not $x38)) $x57))))
(let (($x61 (not $x38)))
(let (($x64 (or $x57 $x61)))
(let (($x43 (not (= c$ (+ a$ b$)))))
(let (($x34 (<= (- c$ b$) a$)))
(let (($x44 (or $x34 $x43)))
(let ((@x63 (monotonicity (rewrite (= (= c$ (+ a$ b$)) $x38)) (= $x43 $x61))))
(let ((@x66 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) @x63 (= (or (<= (+ (* (- 1) b$) c$) a$) $x43) $x64))))
(let ((@x52 (monotonicity (rewrite (= (- c$ b$) (+ (* (- 1) b$) c$))) (= $x34 (<= (+ (* (- 1) b$) c$) a$)))))
(let ((@x55 (monotonicity @x52 (= $x44 (or (<= (+ (* (- 1) b$) c$) a$) $x43)))))
(let ((@x97 (mp (mp (asserted $x44) (trans @x55 @x66 (= $x44 $x64)) $x64) @x96 $x57)))
(let ((@x101 (monotonicity (iff-true @x97 (= $x57 true)) (= (not $x57) (not true)))))
(let ((@x103 (trans @x101 (rewrite (= (not true) false)) (= (not $x57) false))))
(let (($x75 (not $x57)))
(let ((@x77 (monotonicity (rewrite (= (<= (+ (* (- 1) b$) c$) a$) $x57)) (= (not (<= (+ (* (- 1) b$) c$) a$)) $x75))))
(let ((@x74 (monotonicity @x52 (= (not $x34) (not (<= (+ (* (- 1) b$) c$) a$))))))
(let ((@x80 (mp (asserted (not $x34)) (trans @x74 @x77 (= (not $x34) $x75)) $x75)))
(mp @x80 @x103 false)))))))))))))))))))))))))))

4935c5af5b588fd6e477bea2bed6285c3e17b0c6 23 0
unsat
((set-logic AUFLIA)
(proof
(let (($x63 (<= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
(let (($x81 (not $x63)))
(let (($x66 (= (+ c$ (* (- 1) b$) (* (- 1) a$)) 0)))
(let (($x75 (not (or $x63 (not $x66)))))
(let (($x36 (not (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))))))
(let (($x49 (= c$ (+ b$ a$))))
(let (($x52 (not $x49)))
(let (($x43 (<= (+ c$ (* (- 1) b$)) a$)))
(let (($x55 (or $x43 $x52)))
(let ((@x74 (monotonicity (rewrite (= $x43 $x63)) (monotonicity (rewrite (= $x49 $x66)) (= $x52 (not $x66))) (= $x55 (or $x63 (not $x66))))))
(let (($x56 (= (or (<= (- c$ b$) a$) (not (= c$ (+ a$ b$)))) $x55)))
(let ((@x51 (monotonicity (rewrite (= (+ a$ b$) (+ b$ a$))) (= (= c$ (+ a$ b$)) $x49))))
(let ((@x45 (monotonicity (rewrite (= (- c$ b$) (+ c$ (* (- 1) b$)))) (= (<= (- c$ b$) a$) $x43))))
(let ((@x57 (monotonicity @x45 (monotonicity @x51 (= (not (= c$ (+ a$ b$))) $x52)) $x56)))
(let ((@x79 (trans (monotonicity @x57 (= $x36 (not $x55))) (monotonicity @x74 (= (not $x55) $x75)) (= $x36 $x75))))
(let ((@x84 (monotonicity (not-or-elim (mp (asserted $x36) @x79 $x75) $x66) (= $x63 (<= 0 0)))))
(let ((@x90 (trans @x84 (rewrite (= (<= 0 0) true)) (= $x63 true))))
(let ((@x97 (trans (monotonicity @x90 (= $x81 (not true))) (rewrite (= (not true) false)) (= $x81 false))))
(mp (not-or-elim (mp (asserted $x36) @x79 $x75) $x81) @x97 false)))))))))))))))))))))