mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
14 lines
182 B
Plaintext
14 lines
182 B
Plaintext
|
|
type 'a pointer
|
|
type 'a pset
|
|
|
|
logic P : int -> prop
|
|
logic Q : int , int -> prop
|
|
|
|
axiom a:
|
|
(forall x:int.
|
|
(P(x) <->
|
|
(exists i:int, r: int. Q(r,i))))
|
|
|
|
goal g8: Q(1,2) -> P(4)
|