diff options
Diffstat (limited to 'assignment6/B.prf')
| -rw-r--r-- | assignment6/B.prf | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/assignment6/B.prf b/assignment6/B.prf new file mode 100644 index 0000000..7cd3e82 --- /dev/null +++ b/assignment6/B.prf @@ -0,0 +1,79 @@ +(th_B + (B_0 0 + (B_0-1 nil 3666686678 ("" (flatten) (("" (inst -1 "a") nil nil)) nil) + ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil)) + shostak)) + (B_1 0 + (B_1-1 nil 3666686733 + ("" (flatten) (("" (inst -1 "a") (("" (assert) nil nil)) nil)) nil) + ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil)) + shostak)) + (B_2 0 + (B_2-1 nil 3666686753 + ("" (flatten) (("" (inst 1 "a") (("" (inst -1 "a") nil nil)) nil)) + nil) + ((U nonempty-type-decl nil th_B nil) (a const-decl "U" th_B nil)) + shostak)) + (B_3 0 + (B_3-1 nil 3666686845 + ("" (flatten) (("" (skolem 1 "B") (("" (inst 2 "B") nil nil)) nil)) + nil) + ((U nonempty-type-decl nil th_B nil)) shostak)) + (B_4 0 + (B_4-1 nil 3666686921 + ("" (split) + (("1" (flatten) + (("1" (skolem 1 "A") (("1" (inst 2 "A") nil nil)) nil)) nil) + ("2" (flatten) + (("2" (skolem -1 "A") (("2" (inst -1 "A") nil nil)) nil)) nil)) + nil) + ((U nonempty-type-decl nil th_B nil)) shostak)) + (B_5 0 + (B_5-1 nil 3666687393 + ("" (split) + (("1" (flatten) + (("1" (skolem 2 "A") (("1" (inst 1 "A") nil nil)) nil)) nil) + ("2" (flatten) + (("2" (skolem -2 "A") (("2" (inst -1 "A") nil nil)) nil)) nil)) + nil) + ((U nonempty-type-decl nil th_B nil)) shostak)) + (B_6 0 + (B_6-1 nil 3666687440 + ("" (split) + (("1" (flatten) + (("1" (skolem 1 "A") + (("1" (split) + (("1" (inst -1 "A") nil nil) ("2" (inst -2 "A") nil nil)) + nil)) + nil)) + nil) + ("2" (flatten) + (("2" (split) + (("1" (skolem 1 "A") + (("1" (inst -1 "A") (("1" (flatten -1) nil nil)) nil)) nil) + ("2" (skolem 1 "A") + (("2" (inst -1 "A") (("2" (flatten -1) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((U nonempty-type-decl nil th_B nil)) shostak)) + (B_7 0 + (B_7-1 nil 3666687512 + ("" (split) + (("1" (flatten) + (("1" (split -1) + (("1" (skolem -1 "A") + (("1" (inst 1 "A") (("1" (flatten 1) nil nil)) nil)) nil) + ("2" (skolem -1 "A") + (("2" (inst 1 "A") (("2" (flatten 1) nil nil)) nil)) nil)) + nil)) + nil) + ("2" (flatten) + (("2" (skolem -1 "A") + (("2" (split -1) + (("1" (inst 1 "A") nil nil) ("2" (inst 2 "A") nil nil)) nil)) + nil)) + nil)) + nil) + ((U nonempty-type-decl nil th_B nil)) shostak))) + |