src/HOL/SMT/Examples/cert/z3_fol_03.proof
author bulwahn
Wed, 20 Jan 2010 18:08:08 +0100
changeset 34953 a053ad2a7a72
parent 33010 39f73a59e855
permissions -rw-r--r--
adopting Sequences
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 up_1 :: (-> T1 T2 bool)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     3
#5 := (:var 0 T2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     4
decl uf_4 :: T1
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     5
#18 := uf_4
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     6
#19 := (up_1 uf_4 #5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     7
#635 := (pattern #19)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     8
#116 := (not #19)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     9
#636 := (forall (vars (?x6 T2)) (:pat #635) #116)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    10
decl uf_3 :: T2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    11
#14 := uf_3
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    12
#21 := (up_1 uf_4 uf_3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    13
decl uf_2 :: T1
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    14
#7 := uf_2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    15
#195 := (= uf_2 uf_4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    16
#602 := (iff #21 #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    17
#4 := (:var 1 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    18
#6 := (up_1 #4 #5)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    19
#612 := (pattern #6)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    20
#8 := (= #4 uf_2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    21
#9 := (iff #6 #8)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    22
#613 := (forall (vars (?x1 T1) (?x2 T2)) (:pat #612) #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    23
#10 := (forall (vars (?x1 T1) (?x2 T2)) #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    24
#616 := (iff #10 #613)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    25
#614 := (iff #9 #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    26
#615 := [refl]: #614
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    27
#617 := [quant-intro #615]: #616
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    28
#56 := (~ #10 #10)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    29
#54 := (~ #9 #9)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    30
#55 := [refl]: #54
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    31
#57 := [nnf-pos #55]: #56
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    32
#39 := [asserted]: #10
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    33
#58 := [mp~ #39 #57]: #10
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    34
#618 := [mp #58 #617]: #613
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    35
#286 := (not #613)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    36
#244 := (or #286 #602)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    37
#194 := (= uf_4 uf_2)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    38
#264 := (iff #21 #194)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    39
#587 := (or #286 #264)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    40
#249 := (iff #587 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    41
#251 := (iff #244 #244)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    42
#589 := [rewrite]: #251
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    43
#260 := (iff #264 #602)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    44
#282 := (iff #194 #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    45
#196 := [rewrite]: #282
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    46
#603 := [monotonicity #196]: #260
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    47
#250 := [monotonicity #603]: #249
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    48
#590 := [trans #250 #589]: #249
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    49
#248 := [quant-inst]: #587
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    50
#591 := [mp #248 #590]: #244
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    51
#598 := [unit-resolution #591 #618]: #602
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    52
decl ?x6!3 :: T2
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    53
#63 := ?x6!3
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    54
#64 := (up_1 uf_4 ?x6!3)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    55
#283 := (iff #64 #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    56
#214 := (or #286 #283)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    57
#281 := (iff #64 #194)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    58
#287 := (or #286 #281)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    59
#288 := (iff #287 #214)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    60
#604 := (iff #214 #214)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    61
#606 := [rewrite]: #604
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    62
#274 := (iff #281 #283)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    63
#285 := [monotonicity #196]: #274
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    64
#267 := [monotonicity #285]: #288
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    65
#261 := [trans #267 #606]: #288
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    66
#284 := [quant-inst]: #287
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    67
#393 := [mp #284 #261]: #214
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    68
#596 := [unit-resolution #393 #618]: #283
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    69
#600 := (not #283)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    70
#586 := (or #600 #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    71
#122 := (not #21)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    72
#599 := [hypothesis]: #122
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    73
#127 := (or #21 #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    74
#119 := (forall (vars (?x6 T2)) #116)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    75
#128 := (or #122 #119)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    76
#135 := (and #127 #128)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    77
#129 := (and #128 #127)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    78
#136 := (iff #129 #135)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    79
#137 := [rewrite]: #136
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    80
#20 := (exists (vars (?x6 T2)) #19)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    81
#42 := (not #20)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    82
#43 := (iff #21 #42)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    83
#130 := (~ #43 #129)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    84
#120 := (~ #42 #119)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    85
#117 := (~ #116 #116)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    86
#118 := [refl]: #117
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    87
#121 := [nnf-neg #118]: #120
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    88
#113 := (not #42)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    89
#114 := (~ #113 #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    90
#88 := (~ #20 #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    91
#89 := [sk]: #88
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    92
#115 := [nnf-neg #89]: #114
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    93
#125 := (~ #21 #21)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    94
#126 := [refl]: #125
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    95
#123 := (~ #122 #122)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    96
#124 := [refl]: #123
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    97
#131 := [nnf-pos #124 #126 #115 #121]: #130
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    98
#22 := (iff #20 #21)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    99
#23 := (not #22)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   100
#44 := (iff #23 #43)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   101
#45 := [rewrite]: #44
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   102
#41 := [asserted]: #23
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   103
#48 := [mp #41 #45]: #43
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   104
#132 := [mp~ #48 #131]: #129
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   105
#133 := [mp #132 #137]: #135
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   106
#134 := [and-elim #133]: #127
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   107
#585 := [unit-resolution #134 #599]: #64
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   108
#608 := (not #64)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   109
#609 := (or #600 #608 #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   110
#610 := [def-axiom]: #609
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   111
#292 := [unit-resolution #610 #585]: #586
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   112
#308 := [unit-resolution #292 #596]: #195
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   113
#272 := (not #195)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   114
#592 := (not #602)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   115
#309 := (or #592 #272)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   116
#593 := (or #592 #21 #272)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   117
#588 := [def-axiom]: #593
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   118
#310 := [unit-resolution #588 #599]: #309
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   119
#296 := [unit-resolution #310 #308 #598]: false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   120
#311 := [lemma #296]: #21
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   121
#641 := (or #122 #636)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   122
#642 := (iff #128 #641)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   123
#639 := (iff #119 #636)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   124
#637 := (iff #116 #116)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   125
#638 := [refl]: #637
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   126
#640 := [quant-intro #638]: #639
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   127
#643 := [monotonicity #640]: #642
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   128
#138 := [and-elim #133]: #128
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   129
#644 := [mp #138 #643]: #641
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   130
#594 := [unit-resolution #644 #311]: #636
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   131
#595 := (not #636)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   132
#597 := (or #595 #122)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   133
#235 := [quant-inst]: #597
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   134
[unit-resolution #235 #311 #594]: false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
   135
unsat