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_03.proof
author boehmes
Thu, 03 Dec 2009 15:56:06 +0100
changeset 34010 ac78f5cdc430
parent 33010 39f73a59e855
permissions -rw-r--r--
faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization), custom-made (top-down) atomize_conv, store predicate and function symbols in a table instead of a list for faster lookup, updated certificates
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     1
 
#2 := false
34010
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     2
 
decl up_2 :: (-> T2 bool)
33010
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
 
#10 := uf_3
34010
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     5
 
#17 := (up_2 uf_3)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     6
 
#78 := (not #17)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     7
 
decl uf_1 :: (-> T1 T1)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     8
 
decl uf_4 :: T1
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
     9
 
#14 := uf_4
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    10
 
#15 := (uf_1 uf_4)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    11
 
#46 := (= uf_4 #15)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    12
 
#79 := (not #46)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    13
 
#145 := [hypothesis]: #79
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    14
 
#4 := (:var 0 T1)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    15
 
#5 := (uf_1 #4)
34010
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    16
 
#563 := (pattern #5)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    17
 
#37 := (= #4 #5)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    18
 
#564 := (forall (vars (?x1 T1)) (:pat #563) #37)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    19
 
#40 := (forall (vars (?x1 T1)) #37)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    20
 
#567 := (iff #40 #564)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    21
 
#565 := (iff #37 #37)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    22
 
#566 := [refl]: #565
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    23
 
#568 := [quant-intro #566]: #567
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    24
 
#72 := (~ #40 #40)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    25
 
#70 := (~ #37 #37)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    26
 
#71 := [refl]: #70
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    27
 
#73 := [nnf-pos #71]: #72
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    28
 
#6 := (= #5 #4)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    29
 
#7 := (forall (vars (?x1 T1)) #6)
34010
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    30
 
#41 := (iff #7 #40)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    31
 
#38 := (iff #6 #37)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    32
 
#39 := [rewrite]: #38
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    33
 
#42 := [quant-intro #39]: #41
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    34
 
#36 := [asserted]: #7
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    35
 
#45 := [mp #36 #42]: #40
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    36
 
#74 := [mp~ #45 #73]: #40
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    37
 
#569 := [mp #74 #568]: #564
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    38
 
#146 := (not #564)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    39
 
#233 := (or #146 #46)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    40
 
#147 := [quant-inst]: #233
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    41
 
#232 := [unit-resolution #147 #569 #145]: false
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    42
 
#234 := [lemma #232]: #46
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    43
 
#66 := (or #78 #79)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    44
 
#54 := (and #17 #46)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    45
 
#59 := (not #54)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    46
 
#85 := (iff #59 #66)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    47
 
#67 := (not #66)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    48
 
#80 := (not #67)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    49
 
#83 := (iff #80 #66)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    50
 
#84 := [rewrite]: #83
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    51
 
#81 := (iff #59 #80)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    52
 
#68 := (iff #54 #67)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    53
 
#69 := [rewrite]: #68
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    54
 
#82 := [monotonicity #69]: #81
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    55
 
#86 := [trans #82 #84]: #85
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    56
 
#1 := true
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    57
 
#18 := (iff #17 true)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    58
 
#16 := (= #15 uf_4)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    59
 
#19 := (and #16 #18)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    60
 
#20 := (not #19)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    61
 
#60 := (iff #20 #59)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    62
 
#57 := (iff #19 #54)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    63
 
#51 := (and #46 #17)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    64
 
#55 := (iff #51 #54)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    65
 
#56 := [rewrite]: #55
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    66
 
#52 := (iff #19 #51)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    67
 
#49 := (iff #18 #17)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    68
 
#50 := [rewrite]: #49
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    69
 
#47 := (iff #16 #46)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    70
 
#48 := [rewrite]: #47
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    71
 
#53 := [monotonicity #48 #50]: #52
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    72
 
#58 := [trans #53 #56]: #57
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    73
 
#61 := [monotonicity #58]: #60
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    74
 
#44 := [asserted]: #20
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    75
 
#64 := [mp #44 #61]: #59
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    76
 
#87 := [mp #64 #86]: #66
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    77
 
#561 := [unit-resolution #87 #234]: #78
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    78
 
#8 := (:var 0 T2)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    79
 
#9 := (up_2 #8)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    80
 
#570 := (pattern #9)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    81
 
#11 := (= #8 uf_3)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    82
 
#12 := (iff #9 #11)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    83
 
#571 := (forall (vars (?x2 T2)) (:pat #570) #12)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    84
 
#13 := (forall (vars (?x2 T2)) #12)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    85
 
#574 := (iff #13 #571)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    86
 
#572 := (iff #12 #12)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    87
 
#573 := [refl]: #572
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    88
 
#575 := [quant-intro #573]: #574
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    89
 
#65 := (~ #13 #13)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    90
 
#75 := (~ #12 #12)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    91
 
#76 := [refl]: #75
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    92
 
#62 := [nnf-pos #76]: #65
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    93
 
#43 := [asserted]: #13
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    94
 
#77 := [mp~ #43 #62]: #13
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    95
 
#576 := [mp #77 #575]: #571
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    96
 
#555 := (not #571)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    97
 
#557 := (or #555 #17)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    98
 
#225 := (= uf_3 uf_3)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
    99
 
#236 := (iff #17 #225)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   100
 
#212 := (or #555 #236)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   101
 
#551 := (iff #212 #557)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   102
 
#224 := (iff #557 #557)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   103
 
#558 := [rewrite]: #224
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   104
 
#239 := (iff #236 #17)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   105
 
#238 := (iff #236 #18)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   106
 
#237 := (iff #225 true)
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   107
 
#165 := [rewrite]: #237
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   108
 
#235 := [monotonicity #165]: #238
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   109
 
#218 := [trans #235 #50]: #239
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   110
 
#223 := [monotonicity #218]: #551
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   111
 
#559 := [trans #223 #558]: #551
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   112
 
#344 := [quant-inst]: #212
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   113
 
#560 := [mp #344 #559]: #557
ac78f5cdc430 faster preprocessing: before applying a step, test if it is applicable (normalization of binders, unfolding of abs/min/max definitions, lambda lifting, explicit application, monomorphization),
boehmes
parents: 33010
diff changeset 
   114
 
[unit-resolution #560 #576 #561]: false
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
   115
 
unsat
isabelle