src/HOL/Boogie/Examples/cert/Boogie_Dijkstra
changeset 33663 a84fd6385832
parent 33445 f0c78a28e18e
child 34015 5426ada71790
     1.1 --- a/src/HOL/Boogie/Examples/cert/Boogie_Dijkstra	Fri Nov 13 15:10:28 2009 +0100
     1.2 +++ b/src/HOL/Boogie/Examples/cert/Boogie_Dijkstra	Fri Nov 13 15:11:41 2009 +0100
     1.3 @@ -12,18 +12,18 @@
     1.4    (uf_10 T1 Int)
     1.5    (uf_11 T2)
     1.6    (uf_9 Int)
     1.7 -  (uf_21 T2)
     1.8 -  (uf_16 T2)
     1.9 -  (uf_20 T2)
    1.10 +  (uf_18 T2)
    1.11 +  (uf_22 T2)
    1.12 +  (uf_17 T2)
    1.13    (uf_12 T2 Int)
    1.14    (uf_14 T3)
    1.15 -  (uf_18 T2 Int)
    1.16 -  (uf_22 T3)
    1.17 -  (uf_24 T3)
    1.18 -  (uf_23 T3)
    1.19 +  (uf_24 T2 Int)
    1.20 +  (uf_19 T3)
    1.21 +  (uf_21 T3)
    1.22 +  (uf_20 T3)
    1.23    (uf_15 T4)
    1.24 -  (uf_17 T4)
    1.25 -  (uf_19 T4)
    1.26 +  (uf_23 T4)
    1.27 +  (uf_16 T4)
    1.28   )
    1.29  :extrapreds (
    1.30    (up_13 T2)
    1.31 @@ -38,6 +38,6 @@
    1.32  :assumption (< 0 uf_9)
    1.33  :assumption (forall (?x20 T2) (?x21 T2) (implies (= ?x20 ?x21) (= (uf_10 (uf_1 ?x20 ?x21)) 0)))
    1.34  :assumption (forall (?x22 T2) (?x23 T2) (implies (not (= ?x22 ?x23)) (< 0 (uf_10 (uf_1 ?x22 ?x23)))))
    1.35 -:assumption (not (implies true (implies true (implies (forall (?x24 T2) (implies (= ?x24 uf_11) (= (uf_12 ?x24) 0))) (implies (forall (?x25 T2) (implies (not (= ?x25 uf_11)) (= (uf_12 ?x25) uf_9))) (implies (forall (?x26 T2) (not (up_13 ?x26))) (implies true (and (implies (= (uf_12 uf_11) 0) (and (implies (forall (?x27 T2) (<= 0 (uf_12 ?x27))) (and (implies (forall (?x28 T2) (?x29 T2) (implies (and (up_13 ?x28) (not (up_13 ?x29))) (<= (uf_12 ?x28) (uf_12 ?x29)))) (and (implies (forall (?x30 T2) (?x31 T2) (implies (and (< (uf_10 (uf_1 ?x31 ?x30)) uf_9) (up_13 ?x31)) (<= (uf_12 ?x30) (+ (uf_12 ?x31) (uf_10 (uf_1 ?x31 ?x30)))))) (and (implies (forall (?x32 T2) (implies (and (< (uf_12 ?x32) uf_9) (not (= ?x32 uf_11))) (exists (?x33 T2) (and (= (uf_12 ?x32) (+ (uf_12 ?x33) (uf_10 (uf_1 ?x33 ?x32)))) (and (up_13 ?x33) (< (uf_12 ?x33) (uf_12 ?x32))))))) (implies true (implies true (implies (= (uf_4 uf_14 uf_11) 0) (implies (forall (?x34 T2) (<= 0 (uf_4 uf_14 ?x34))) (implies (forall (?x35 T2) (?x36 T2) (implies (and (= (uf_6 uf_15 ?x35) uf_8) (not (= (uf_6 uf_15 ?x36) uf_8))) (<= (uf_4 uf_14 ?x35) (uf_4 uf_14 ?x36)))) (implies (forall (?x37 T2) (?x38 T2) (implies (and (< (uf_10 (uf_1 ?x38 ?x37)) uf_9) (= (uf_6 uf_15 ?x38) uf_8)) (<= (uf_4 uf_14 ?x37) (+ (uf_4 uf_14 ?x38) (uf_10 (uf_1 ?x38 ?x37)))))) (implies (forall (?x39 T2) (implies (and (< (uf_4 uf_14 ?x39) uf_9) (not (= ?x39 uf_11))) (exists (?x40 T2) (and (= (uf_4 uf_14 ?x39) (+ (uf_4 uf_14 ?x40) (uf_10 (uf_1 ?x40 ?x39)))) (and (= (uf_6 uf_15 ?x40) uf_8) (< (uf_4 uf_14 ?x40) (uf_4 uf_14 ?x39))))))) (implies true (and (implies true (implies true (implies (exists (?x41 T2) (and (< (uf_4 uf_14 ?x41) uf_9) (not (= (uf_6 uf_15 ?x41) uf_8)))) (implies (not (= (uf_6 uf_15 uf_16) uf_8)) (implies (< (uf_4 uf_14 uf_16) uf_9) (implies (forall (?x42 T2) (implies (not (= (uf_6 uf_15 ?x42) uf_8)) (<= (uf_4 uf_14 uf_16) (uf_4 uf_14 ?x42)))) (implies (= uf_17 (uf_7 uf_15 uf_16 uf_8)) (implies (forall (?x43 T2) (implies (and (< (+ (uf_4 uf_14 uf_16) (uf_10 (uf_1 uf_16 ?x43))) (uf_4 uf_14 ?x43)) (< (uf_10 (uf_1 uf_16 ?x43)) uf_9)) (= (uf_18 ?x43) (+ (uf_4 uf_14 uf_16) (uf_10 (uf_1 uf_16 ?x43)))))) (implies (forall (?x44 T2) (implies (not (and (< (+ (uf_4 uf_14 uf_16) (uf_10 (uf_1 uf_16 ?x44))) (uf_4 uf_14 ?x44)) (< (uf_10 (uf_1 uf_16 ?x44)) uf_9))) (= (uf_18 ?x44) (uf_4 uf_14 ?x44)))) (and (implies (forall (?x45 T2) (<= (uf_18 ?x45) (uf_4 uf_14 ?x45))) (and (implies (forall (?x46 T2) (implies (= (uf_6 uf_17 ?x46) uf_8) (= (uf_18 ?x46) (uf_4 uf_14 ?x46)))) (implies true (implies true (and (implies (= (uf_18 uf_11) 0) (and (implies (forall (?x47 T2) (<= 0 (uf_18 ?x47))) (and (implies (forall (?x48 T2) (?x49 T2) (implies (and (= (uf_6 uf_17 ?x48) uf_8) (not (= (uf_6 uf_17 ?x49) uf_8))) (<= (uf_18 ?x48) (uf_18 ?x49)))) (and (implies (forall (?x50 T2) (?x51 T2) (implies (and (< (uf_10 (uf_1 ?x51 ?x50)) uf_9) (= (uf_6 uf_17 ?x51) uf_8)) (<= (uf_18 ?x50) (+ (uf_18 ?x51) (uf_10 (uf_1 ?x51 ?x50)))))) (and (implies (forall (?x52 T2) (implies (and (< (uf_18 ?x52) uf_9) (not (= ?x52 uf_11))) (exists (?x53 T2) (and (= (uf_18 ?x52) (+ (uf_18 ?x53) (uf_10 (uf_1 ?x53 ?x52)))) (and (= (uf_6 uf_17 ?x53) uf_8) (< (uf_18 ?x53) (uf_18 ?x52))))))) (implies false true)) (forall (?x54 T2) (implies (and (< (uf_18 ?x54) uf_9) (not (= ?x54 uf_11))) (exists (?x55 T2) (and (= (uf_18 ?x54) (+ (uf_18 ?x55) (uf_10 (uf_1 ?x55 ?x54)))) (and (= (uf_6 uf_17 ?x55) uf_8) (< (uf_18 ?x55) (uf_18 ?x54))))))))) (forall (?x56 T2) (?x57 T2) (implies (and (< (uf_10 (uf_1 ?x57 ?x56)) uf_9) (= (uf_6 uf_17 ?x57) uf_8)) (<= (uf_18 ?x56) (+ (uf_18 ?x57) (uf_10 (uf_1 ?x57 ?x56)))))))) (forall (?x58 T2) (?x59 T2) (implies (and (= (uf_6 uf_17 ?x58) uf_8) (not (= (uf_6 uf_17 ?x59) uf_8))) (<= (uf_18 ?x58) (uf_18 ?x59)))))) (forall (?x60 T2) (<= 0 (uf_18 ?x60))))) (= (uf_18 uf_11) 0))))) (forall (?x61 T2) (implies (= (uf_6 uf_17 ?x61) uf_8) (= (uf_18 ?x61) (uf_4 uf_14 ?x61)))))) (forall (?x62 T2) (<= (uf_18 ?x62) (uf_4 uf_14 ?x62))))))))))))) (implies true (implies true (implies (not (exists (?x63 T2) (and (< (uf_4 uf_14 ?x63) uf_9) (not (= (uf_6 uf_15 ?x63) uf_8))))) (implies true (implies true (implies (= uf_19 uf_15) (implies (= uf_20 uf_21) (implies (= uf_22 uf_14) (implies (= uf_23 uf_24) (implies true (and (implies (forall (?x64 T2) (implies (and (< (uf_4 uf_22 ?x64) uf_9) (not (= ?x64 uf_11))) (exists (?x65 T2) (and (= (uf_4 uf_22 ?x64) (+ (uf_4 uf_22 ?x65) (uf_10 (uf_1 ?x65 ?x64)))) (< (uf_4 uf_22 ?x65) (uf_4 uf_22 ?x64)))))) (and (implies (forall (?x66 T2) (?x67 T2) (implies (and (< (uf_10 (uf_1 ?x67 ?x66)) uf_9) (< (uf_4 uf_22 ?x67) uf_9)) (<= (uf_4 uf_22 ?x66) (+ (uf_4 uf_22 ?x67) (uf_10 (uf_1 ?x67 ?x66)))))) (and (implies (= (uf_4 uf_22 uf_11) 0) true) (= (uf_4 uf_22 uf_11) 0))) (forall (?x68 T2) (?x69 T2) (implies (and (< (uf_10 (uf_1 ?x69 ?x68)) uf_9) (< (uf_4 uf_22 ?x69) uf_9)) (<= (uf_4 uf_22 ?x68) (+ (uf_4 uf_22 ?x69) (uf_10 (uf_1 ?x69 ?x68)))))))) (forall (?x70 T2) (implies (and (< (uf_4 uf_22 ?x70) uf_9) (not (= ?x70 uf_11))) (exists (?x71 T2) (and (= (uf_4 uf_22 ?x70) (+ (uf_4 uf_22 ?x71) (uf_10 (uf_1 ?x71 ?x70)))) (< (uf_4 uf_22 ?x71) (uf_4 uf_22 ?x70))))))))))))))))))))))))))) (forall (?x72 T2) (implies (and (< (uf_12 ?x72) uf_9) (not (= ?x72 uf_11))) (exists (?x73 T2) (and (= (uf_12 ?x72) (+ (uf_12 ?x73) (uf_10 (uf_1 ?x73 ?x72)))) (and (up_13 ?x73) (< (uf_12 ?x73) (uf_12 ?x72))))))))) (forall (?x74 T2) (?x75 T2) (implies (and (< (uf_10 (uf_1 ?x75 ?x74)) uf_9) (up_13 ?x75)) (<= (uf_12 ?x74) (+ (uf_12 ?x75) (uf_10 (uf_1 ?x75 ?x74)))))))) (forall (?x76 T2) (?x77 T2) (implies (and (up_13 ?x76) (not (up_13 ?x77))) (<= (uf_12 ?x76) (uf_12 ?x77)))))) (forall (?x78 T2) (<= 0 (uf_12 ?x78))))) (= (uf_12 uf_11) 0)))))))))
    1.36 +:assumption (not (implies true (implies true (implies (forall (?x24 T2) (implies (= ?x24 uf_11) (= (uf_12 ?x24) 0))) (implies (forall (?x25 T2) (implies (not (= ?x25 uf_11)) (= (uf_12 ?x25) uf_9))) (implies (forall (?x26 T2) (not (up_13 ?x26))) (implies true (and (= (uf_12 uf_11) 0) (implies (= (uf_12 uf_11) 0) (and (forall (?x27 T2) (<= 0 (uf_12 ?x27))) (implies (forall (?x28 T2) (<= 0 (uf_12 ?x28))) (and (forall (?x29 T2) (?x30 T2) (implies (and (not (up_13 ?x30)) (up_13 ?x29)) (<= (uf_12 ?x29) (uf_12 ?x30)))) (implies (forall (?x31 T2) (?x32 T2) (implies (and (not (up_13 ?x32)) (up_13 ?x31)) (<= (uf_12 ?x31) (uf_12 ?x32)))) (and (forall (?x33 T2) (?x34 T2) (implies (and (up_13 ?x34) (< (uf_10 (uf_1 ?x34 ?x33)) uf_9)) (<= (uf_12 ?x33) (+ (uf_12 ?x34) (uf_10 (uf_1 ?x34 ?x33)))))) (implies (forall (?x35 T2) (?x36 T2) (implies (and (up_13 ?x36) (< (uf_10 (uf_1 ?x36 ?x35)) uf_9)) (<= (uf_12 ?x35) (+ (uf_12 ?x36) (uf_10 (uf_1 ?x36 ?x35)))))) (and (forall (?x37 T2) (implies (and (not (= ?x37 uf_11)) (< (uf_12 ?x37) uf_9)) (exists (?x38 T2) (and (< (uf_12 ?x38) (uf_12 ?x37)) (and (up_13 ?x38) (= (uf_12 ?x37) (+ (uf_12 ?x38) (uf_10 (uf_1 ?x38 ?x37))))))))) (implies (forall (?x39 T2) (implies (and (not (= ?x39 uf_11)) (< (uf_12 ?x39) uf_9)) (exists (?x40 T2) (and (< (uf_12 ?x40) (uf_12 ?x39)) (and (up_13 ?x40) (= (uf_12 ?x39) (+ (uf_12 ?x40) (uf_10 (uf_1 ?x40 ?x39))))))))) (implies true (implies true (implies (= (uf_4 uf_14 uf_11) 0) (implies (forall (?x41 T2) (<= 0 (uf_4 uf_14 ?x41))) (implies (forall (?x42 T2) (?x43 T2) (implies (and (not (= (uf_6 uf_15 ?x43) uf_8)) (= (uf_6 uf_15 ?x42) uf_8)) (<= (uf_4 uf_14 ?x42) (uf_4 uf_14 ?x43)))) (implies (forall (?x44 T2) (?x45 T2) (implies (and (= (uf_6 uf_15 ?x45) uf_8) (< (uf_10 (uf_1 ?x45 ?x44)) uf_9)) (<= (uf_4 uf_14 ?x44) (+ (uf_4 uf_14 ?x45) (uf_10 (uf_1 ?x45 ?x44)))))) (implies (forall (?x46 T2) (implies (and (not (= ?x46 uf_11)) (< (uf_4 uf_14 ?x46) uf_9)) (exists (?x47 T2) (and (< (uf_4 uf_14 ?x47) (uf_4 uf_14 ?x46)) (and (= (uf_6 uf_15 ?x47) uf_8) (= (uf_4 uf_14 ?x46) (+ (uf_4 uf_14 ?x47) (uf_10 (uf_1 ?x47 ?x46))))))))) (implies true (and (implies true (implies true (implies (not (exists (?x48 T2) (and (not (= (uf_6 uf_15 ?x48) uf_8)) (< (uf_4 uf_14 ?x48) uf_9)))) (implies true (implies true (implies (= uf_16 uf_15) (implies (= uf_17 uf_18) (implies (= uf_19 uf_14) (implies (= uf_20 uf_21) (implies true (and (forall (?x49 T2) (implies (and (not (= ?x49 uf_11)) (< (uf_4 uf_19 ?x49) uf_9)) (exists (?x50 T2) (and (< (uf_4 uf_19 ?x50) (uf_4 uf_19 ?x49)) (= (uf_4 uf_19 ?x49) (+ (uf_4 uf_19 ?x50) (uf_10 (uf_1 ?x50 ?x49)))))))) (implies (forall (?x51 T2) (implies (and (not (= ?x51 uf_11)) (< (uf_4 uf_19 ?x51) uf_9)) (exists (?x52 T2) (and (< (uf_4 uf_19 ?x52) (uf_4 uf_19 ?x51)) (= (uf_4 uf_19 ?x51) (+ (uf_4 uf_19 ?x52) (uf_10 (uf_1 ?x52 ?x51)))))))) (and (forall (?x53 T2) (?x54 T2) (implies (and (< (uf_4 uf_19 ?x54) uf_9) (< (uf_10 (uf_1 ?x54 ?x53)) uf_9)) (<= (uf_4 uf_19 ?x53) (+ (uf_4 uf_19 ?x54) (uf_10 (uf_1 ?x54 ?x53)))))) (implies (forall (?x55 T2) (?x56 T2) (implies (and (< (uf_4 uf_19 ?x56) uf_9) (< (uf_10 (uf_1 ?x56 ?x55)) uf_9)) (<= (uf_4 uf_19 ?x55) (+ (uf_4 uf_19 ?x56) (uf_10 (uf_1 ?x56 ?x55)))))) (and (= (uf_4 uf_19 uf_11) 0) (implies (= (uf_4 uf_19 uf_11) 0) true)))))))))))))))) (implies true (implies true (implies (exists (?x57 T2) (and (not (= (uf_6 uf_15 ?x57) uf_8)) (< (uf_4 uf_14 ?x57) uf_9))) (implies (not (= (uf_6 uf_15 uf_22) uf_8)) (implies (< (uf_4 uf_14 uf_22) uf_9) (implies (forall (?x58 T2) (implies (not (= (uf_6 uf_15 ?x58) uf_8)) (<= (uf_4 uf_14 uf_22) (uf_4 uf_14 ?x58)))) (implies (= uf_23 (uf_7 uf_15 uf_22 uf_8)) (implies (forall (?x59 T2) (implies (and (< (uf_10 (uf_1 uf_22 ?x59)) uf_9) (< (+ (uf_4 uf_14 uf_22) (uf_10 (uf_1 uf_22 ?x59))) (uf_4 uf_14 ?x59))) (= (uf_24 ?x59) (+ (uf_4 uf_14 uf_22) (uf_10 (uf_1 uf_22 ?x59)))))) (implies (forall (?x60 T2) (implies (not (and (< (uf_10 (uf_1 uf_22 ?x60)) uf_9) (< (+ (uf_4 uf_14 uf_22) (uf_10 (uf_1 uf_22 ?x60))) (uf_4 uf_14 ?x60)))) (= (uf_24 ?x60) (uf_4 uf_14 ?x60)))) (and (forall (?x61 T2) (<= (uf_24 ?x61) (uf_4 uf_14 ?x61))) (implies (forall (?x62 T2) (<= (uf_24 ?x62) (uf_4 uf_14 ?x62))) (and (forall (?x63 T2) (implies (= (uf_6 uf_23 ?x63) uf_8) (= (uf_24 ?x63) (uf_4 uf_14 ?x63)))) (implies (forall (?x64 T2) (implies (= (uf_6 uf_23 ?x64) uf_8) (= (uf_24 ?x64) (uf_4 uf_14 ?x64)))) (implies true (implies true (and (= (uf_24 uf_11) 0) (implies (= (uf_24 uf_11) 0) (and (forall (?x65 T2) (<= 0 (uf_24 ?x65))) (implies (forall (?x66 T2) (<= 0 (uf_24 ?x66))) (and (forall (?x67 T2) (?x68 T2) (implies (and (not (= (uf_6 uf_23 ?x68) uf_8)) (= (uf_6 uf_23 ?x67) uf_8)) (<= (uf_24 ?x67) (uf_24 ?x68)))) (implies (forall (?x69 T2) (?x70 T2) (implies (and (not (= (uf_6 uf_23 ?x70) uf_8)) (= (uf_6 uf_23 ?x69) uf_8)) (<= (uf_24 ?x69) (uf_24 ?x70)))) (and (forall (?x71 T2) (?x72 T2) (implies (and (= (uf_6 uf_23 ?x72) uf_8) (< (uf_10 (uf_1 ?x72 ?x71)) uf_9)) (<= (uf_24 ?x71) (+ (uf_24 ?x72) (uf_10 (uf_1 ?x72 ?x71)))))) (implies (forall (?x73 T2) (?x74 T2) (implies (and (= (uf_6 uf_23 ?x74) uf_8) (< (uf_10 (uf_1 ?x74 ?x73)) uf_9)) (<= (uf_24 ?x73) (+ (uf_24 ?x74) (uf_10 (uf_1 ?x74 ?x73)))))) (and (forall (?x75 T2) (implies (and (not (= ?x75 uf_11)) (< (uf_24 ?x75) uf_9)) (exists (?x76 T2) (and (< (uf_24 ?x76) (uf_24 ?x75)) (and (= (uf_6 uf_23 ?x76) uf_8) (= (uf_24 ?x75) (+ (uf_24 ?x76) (uf_10 (uf_1 ?x76 ?x75))))))))) (implies (forall (?x77 T2) (implies (and (not (= ?x77 uf_11)) (< (uf_24 ?x77) uf_9)) (exists (?x78 T2) (and (< (uf_24 ?x78) (uf_24 ?x77)) (and (= (uf_6 uf_23 ?x78) uf_8) (= (uf_24 ?x77) (+ (uf_24 ?x78) (uf_10 (uf_1 ?x78 ?x77))))))))) (implies false true))))))))))))))))))))))))))))))))))))))))))))))))))))
    1.37  :formula true
    1.38  )