From 3690c4f8e21ea6086acd025d62a2571ae6b89ac3 Mon Sep 17 00:00:00 2001
From: Gabriel <gabriel@motacilla.home>
Date: Mon, 18 Oct 2021 18:08:48 +0200
Subject: [PATCH] more examples
---
proofs/examples/Makefile | 2 ++
proofs/examples/hello.prf | 3 +++
proofs/examples/hello.pvs | 1 +
3 files changed, 6 insertions(+)
diff --git a/proofs/examples/Makefile b/proofs/examples/Makefile
index 8fb1da1..da151f9 100644
--- a/proofs/examples/Makefile
+++ b/proofs/examples/Makefile
@@ -4,3 +4,5 @@ PROVEIT ?=
.pvs.log:
${PROVEIT} --traces -l $<
+
+all: hello.log
diff --git a/proofs/examples/hello.prf b/proofs/examples/hello.prf
index ae89e03..bdd255d 100644
--- a/proofs/examples/hello.prf
+++ b/proofs/examples/hello.prf
@@ -4,5 +4,8 @@
("" (flatten)
(("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
nil)
+ nil shostak))
+ (fa 0
+ (fa-1 nil 3843548306 ("" (skolem 1 "c") (("" (flatten) nil nil)) nil)
nil shostak)))
diff --git a/proofs/examples/hello.pvs b/proofs/examples/hello.pvs
index fb4908a..753639a 100644
--- a/proofs/examples/hello.pvs
+++ b/proofs/examples/hello.pvs
@@ -2,4 +2,5 @@ hello: THEORY
BEGIN
P, Q: bool
hello: LEMMA P IMPLIES Q IMPLIES P AND Q
+ fa: LEMMA FORALL (P: bool): P IMPLIES P
END hello
--
GitLab