Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/SMT/Examples/cert/z3_hol_01.proof
author boehmes
Fri, 11 Dec 2009 15:36:05 +0100
changeset 34069 c1fd26512f6d
parent 33010 39f73a59e855
permissions -rw-r--r--
updated dependencies
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     1
 
#2 := false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     2
 
decl uf_1 :: (-> T1 T2 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     3
 
decl uf_3 :: T2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     4
 
#22 := uf_3
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     5
 
decl uf_6 :: T1
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     6
 
#30 := uf_6
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     7
 
#36 := (uf_1 uf_6 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     8
 
decl uf_2 :: (-> T1 T2 T3 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     9
 
decl uf_8 :: T3
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    10
 
#33 := uf_8
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    11
 
decl uf_5 :: T2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    12
 
#26 := uf_5
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    13
 
decl uf_7 :: T3
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    14
 
#31 := uf_7
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    15
 
decl uf_4 :: T2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    16
 
#23 := uf_4
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    17
 
#32 := (uf_2 uf_6 uf_4 uf_7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    18
 
#34 := (uf_2 #32 uf_5 uf_8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    19
 
#35 := (uf_1 #34 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    20
 
#37 := (= #35 #36)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    21
 
#223 := (uf_1 #32 uf_4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    22
 
#214 := (uf_2 uf_6 uf_4 #223)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    23
 
#552 := (uf_1 #214 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    24
 
#555 := (= #552 #36)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    25
 
#560 := (= #36 #552)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    26
 
#556 := (= #223 #552)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    27
 
#24 := (= uf_3 uf_4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    28
 
#561 := (ite #24 #556 #560)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    29
 
#8 := (:var 0 T2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    30
 
#6 := (:var 1 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    31
 
#5 := (:var 2 T2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    32
 
#4 := (:var 3 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    33
 
#7 := (uf_2 #4 #5 #6)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    34
 
#9 := (uf_1 #7 #8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    35
 
#575 := (pattern #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    36
 
#11 := (uf_1 #4 #8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    37
 
#100 := (= #9 #11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    38
 
#99 := (= #6 #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    39
 
#55 := (= #5 #8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    40
 
#83 := (ite #55 #99 #100)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    41
 
#576 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) (:pat #575) #83)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    42
 
#90 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #83)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    43
 
#579 := (iff #90 #576)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    44
 
#577 := (iff #83 #83)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    45
 
#578 := [refl]: #577
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    46
 
#580 := [quant-intro #578]: #579
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    47
 
#58 := (ite #55 #6 #11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    48
 
#61 := (= #9 #58)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    49
 
#64 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #61)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    50
 
#87 := (iff #64 #90)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    51
 
#84 := (iff #61 #83)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    52
 
#89 := [rewrite]: #84
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    53
 
#88 := [quant-intro #89]: #87
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    54
 
#93 := (~ #64 #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    55
 
#91 := (~ #61 #61)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    56
 
#92 := [refl]: #91
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    57
 
#94 := [nnf-pos #92]: #93
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    58
 
#10 := (= #8 #5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    59
 
#12 := (ite #10 #6 #11)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    60
 
#13 := (= #9 #12)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    61
 
#14 := (forall (vars (?x1 T1) (?x2 T2) (?x3 T3) (?x4 T2)) #13)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    62
 
#65 := (iff #14 #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    63
 
#62 := (iff #13 #61)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    64
 
#59 := (= #12 #58)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    65
 
#56 := (iff #10 #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    66
 
#57 := [rewrite]: #56
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    67
 
#60 := [monotonicity #57]: #59
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    68
 
#63 := [monotonicity #60]: #62
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    69
 
#66 := [quant-intro #63]: #65
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    70
 
#54 := [asserted]: #14
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    71
 
#69 := [mp #54 #66]: #64
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    72
 
#95 := [mp~ #69 #94]: #64
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    73
 
#85 := [mp #95 #88]: #90
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    74
 
#581 := [mp #85 #580]: #576
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    75
 
#250 := (not #576)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    76
 
#548 := (or #250 #561)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    77
 
#551 := (= uf_4 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    78
 
#557 := (ite #551 #556 #555)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    79
 
#549 := (or #250 #557)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    80
 
#271 := (iff #549 #548)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    81
 
#273 := (iff #548 #548)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    82
 
#259 := [rewrite]: #273
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    83
 
#559 := (iff #557 #561)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    84
 
#198 := (iff #555 #560)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    85
 
#199 := [rewrite]: #198
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    86
 
#193 := (iff #551 #24)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    87
 
#558 := [rewrite]: #193
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    88
 
#562 := [monotonicity #558 #199]: #559
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    89
 
#272 := [monotonicity #562]: #271
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    90
 
#274 := [trans #272 #259]: #271
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    91
 
#255 := [quant-inst]: #549
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    92
 
#165 := [mp #255 #274]: #548
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    93
 
#510 := [unit-resolution #165 #581]: #561
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    94
 
#544 := (not #561)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    95
 
#497 := (or #544 #560)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    96
 
#25 := (not #24)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    97
 
#27 := (= uf_3 uf_5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    98
 
#28 := (not #27)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    99
 
#29 := (and #25 #28)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   100
 
#75 := [asserted]: #29
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   101
 
#79 := [and-elim #75]: #25
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   102
 
#268 := (or #544 #24 #560)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   103
 
#542 := [def-axiom]: #268
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   104
 
#499 := [unit-resolution #542 #79]: #497
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   105
 
#491 := [unit-resolution #499 #510]: #560
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   106
 
#493 := [symm #491]: #555
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   107
 
#494 := (= #35 #552)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   108
 
#157 := (uf_1 #32 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   109
 
#503 := (= #157 #552)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   110
 
#502 := (= #552 #157)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   111
 
#509 := (= #214 #32)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   112
 
#415 := (= #223 uf_7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   113
 
#566 := (= uf_7 #223)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   114
 
#17 := (:var 0 T3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   115
 
#16 := (:var 1 T2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   116
 
#15 := (:var 2 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   117
 
#18 := (uf_2 #15 #16 #17)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   118
 
#582 := (pattern #18)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   119
 
#19 := (uf_1 #18 #16)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   120
 
#68 := (= #17 #19)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   121
 
#584 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) (:pat #582) #68)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   122
 
#72 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #68)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   123
 
#583 := (iff #72 #584)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   124
 
#586 := (iff #584 #584)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   125
 
#587 := [rewrite]: #586
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   126
 
#585 := [rewrite]: #583
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   127
 
#588 := [trans #585 #587]: #583
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   128
 
#82 := (~ #72 #72)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   129
 
#96 := (~ #68 #68)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   130
 
#97 := [refl]: #96
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   131
 
#78 := [nnf-pos #97]: #82
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   132
 
#20 := (= #19 #17)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   133
 
#21 := (forall (vars (?x5 T1) (?x6 T2) (?x7 T3)) #20)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   134
 
#73 := (iff #21 #72)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   135
 
#70 := (iff #20 #68)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   136
 
#71 := [rewrite]: #70
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   137
 
#74 := [quant-intro #71]: #73
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   138
 
#67 := [asserted]: #21
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   139
 
#77 := [mp #67 #74]: #72
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   140
 
#98 := [mp~ #77 #78]: #72
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   141
 
#589 := [mp #98 #588]: #584
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   142
 
#211 := (not #584)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   143
 
#212 := (or #211 #566)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   144
 
#213 := [quant-inst]: #212
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   145
 
#414 := [unit-resolution #213 #589]: #566
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   146
 
#416 := [symm #414]: #415
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   147
 
#506 := [monotonicity #416]: #509
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   148
 
#498 := [monotonicity #506]: #502
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   149
 
#492 := [symm #498]: #503
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   150
 
#244 := (= #35 #157)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   151
 
#158 := (= uf_8 #35)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   152
 
#248 := (ite #27 #158 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   153
 
#247 := (or #250 #248)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   154
 
#245 := (= uf_5 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   155
 
#159 := (ite #245 #158 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   156
 
#251 := (or #250 #159)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   157
 
#567 := (iff #251 #247)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   158
 
#224 := (iff #247 #247)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   159
 
#356 := [rewrite]: #224
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   160
 
#249 := (iff #159 #248)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   161
 
#246 := (iff #245 #27)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   162
 
#237 := [rewrite]: #246
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   163
 
#177 := [monotonicity #237]: #249
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   164
 
#569 := [monotonicity #177]: #567
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   165
 
#563 := [trans #569 #356]: #567
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   166
 
#230 := [quant-inst]: #251
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   167
 
#235 := [mp #230 #563]: #247
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   168
 
#488 := [unit-resolution #235 #581]: #248
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   169
 
#236 := (not #248)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   170
 
#490 := (or #236 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   171
 
#80 := [and-elim #75]: #28
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   172
 
#572 := (or #236 #27 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   173
 
#573 := [def-axiom]: #572
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   174
 
#500 := [unit-resolution #573 #80]: #490
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   175
 
#501 := [unit-resolution #500 #488]: #244
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   176
 
#495 := [trans #501 #492]: #494
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   177
 
#489 := [trans #495 #493]: #37
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   178
 
#38 := (not #37)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   179
 
#76 := [asserted]: #38
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   180
 
[unit-resolution #76 #489]: false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   181
 
unsat
isabelle