- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
(set-logic LIA)
;(set-option :produce-proofs true)
(define-fun-rec add_via_add1 ((a Int) (b Int)) Int
(ite (= b 0) a ; if (b == 0) return a
(ite (< b 0) (- (add_via_add1 (- a) (- b))) ; if (b < 0) return add_via_add(-a,-b)
(+ (add_via_add1 a (- b 1)) 1) ; return add_via_add(a, b-1) + 1;
)
)
)
(assert
(not (forall ((a Int) (b Int))
(= (add_via_add1 a b) (+ a b))
))
)
(check-sat)
(get-model)
(exit)
Хуйня, которую SMT солверы Z3 и CVC4 доказать не могут. Надо переходить на Coq, Metamath, LEAN, Mizar или еще какую-то такую хуйню
j123123 15.09.2019 13:22 # 0
пофиксил комментарий
guest8 15.09.2019 13:23 # −999
j123123 15.09.2019 13:38 # 0
neTyx_npoTKHyTbIu 15.09.2019 15:08 # 0
Милости прошу к нашему шалашу!
PACTPOBblu_nemyx 15.09.2019 15:28 # 0
AltufyevoGovno 10.11.2021 00:23 # 0
guest8 15.09.2019 15:56 # −999
guest8 15.09.2019 15:09 # −999
guest8 15.09.2019 18:47 # −999
ropuJIJIa 15.09.2019 18:48 # 0
AltufyevoGovno 10.11.2021 00:24 # 0