Assignment 6

1 files changed, 242 insertions, 0 deletions

diff --git a/assignment6/C.prf b/assignment6/C.prf
new file mode 100644
index 0000000..783a5dc
--- /dev/null
+++ b/assignment6/C.prf
@@ -0,0 +1,242 @@
+(th_C
+ (L1 0
+  (L1-1 nil 3666632956
+   ("" (flatten 1)
+    (("" (lemma "Range")
+      (("" (inst -1 "B")
+        (("" (split -1)
+          (("1" (propax) nil nil) ("2" (propax) nil nil)
+           ("3" (lemma "clue1")
+            (("3" (lemma "Range")
+              (("3" (inst -1 "G")
+                (("3" (split -1)
+                  (("1" (assert) nil nil) ("2" (assert) nil nil)
+                   ("3" (assert) nil nil) ("4" (assert) nil nil)
+                   ("5" (assert) nil nil) ("6" (assert) nil nil)
+                   ("7" (assert) nil nil))
+                  nil))
+                nil))
+              nil))
+            nil)
+           ("4" (lemma "Range")
+            (("4" (lemma "clue1")
+              (("4" (inst -2 "G") (("4" (assert) nil nil)) nil)) nil))
+            nil)
+           ("5" (lemma "clue1")
+            (("5" (lemma "Range")
+              (("5" (inst -1 "G") (("5" (assert) nil nil)) nil)) nil))
+            nil)
+           ("6" (lemma "Range")
+            (("6" (lemma "clue1")
+              (("6" (inst -2 "G") (("6" (assert) nil nil)) nil)) nil))
+            nil)
+           ("7" (lemma "Range")
+            (("7" (lemma "clue1")
+              (("7" (inst -2 "G") (("7" (assert) nil nil)) nil)) nil))
+            nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   ((Range formula-decl nil th_C nil)
+    (int_plus_int_is_int application-judgement "int" integers nil)
+    (G? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (G adt-constructor-decl "(G?)" th_C nil)
+    (clue1 formula-decl nil th_C nil)
+    (B adt-constructor-decl "(B?)" th_C nil)
+    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (people type-decl nil th_C nil))
+   shostak))
+ (L2 0
+  (L2-1 nil 3666633277
+   ("" (lemma "clue2")
+    (("" (lemma "Range")
+      (("" (inst -1 "A")
+        (("" (lemma "L1") (("" (assert) nil nil)) nil)) nil))
+      nil))
+    nil)
+   ((Range formula-decl nil th_C nil) (L1 formula-decl nil th_C nil)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (A adt-constructor-decl "(A?)" th_C nil)
+    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (people type-decl nil th_C nil) (clue2 formula-decl nil th_C nil))
+   shostak))
+ (L3 0
+  (L3-1 nil 3666633369
+   ("" (lemma "clue2")
+    (("" (lemma "L2")
+      (("" (lemma "Range")
+        (("" (inst -1 "A") (("" (assert) nil nil)) nil)) nil))
+      nil))
+    nil)
+   ((L2 formula-decl nil th_C nil) (people type-decl nil th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (A adt-constructor-decl "(A?)" th_C nil)
+    (real_gt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (Range formula-decl nil th_C nil)
+    (clue2 formula-decl nil th_C nil))
+   shostak))
+ (L4 0
+  (L4-1 nil 3666633417
+   ("" (lemma "clue1") (("" (lemma "L2") (("" (assert) nil nil)) nil))
+    nil)
+   ((L2 formula-decl nil th_C nil)
+    (int_plus_int_is_int application-judgement "int" integers nil)
+    (clue1 formula-decl nil th_C nil))
+   shostak))
+ (L5 0
+  (L5-1 nil 3666633441
+   ("" (lemma "clue4") (("" (lemma "L4") (("" (assert) nil nil)) nil))
+    nil)
+   ((L4 formula-decl nil th_C nil)
+    (int_plus_int_is_int application-judgement "int" integers nil)
+    (clue4 formula-decl nil th_C nil))
+   shostak))
+ (L6 0
+  (L6-1 nil 3666633467
+   ("" (lemma "Range")
+    (("" (lemma "Unique")
+      (("" (inst -2 "D")
+        (("" (assert)
+          (("" (split -2)
+            (("1" (lemma "L3")
+              (("1" (inst -3 "A" "D") (("1" (assert) nil nil)) nil))
+              nil)
+             ("2" (lemma "L2")
+              (("2" (inst -3 "B" "D") (("2" (assert) nil nil)) nil))
+              nil)
+             ("3" (assert) nil nil) ("4" (assert) nil nil)
+             ("5" (lemma "L5")
+              (("5" (inst -3 "D" "E") (("5" (assert) nil nil)) nil))
+              nil)
+             ("6" (lemma "clue3")
+              (("6" (lemma "L5") (("6" (assert) nil nil)) nil)) nil)
+             ("7" (lemma "clue3")
+              (("7" (lemma "L5") (("7" (assert) nil nil)) nil)) nil))
+            nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   ((Unique formula-decl nil th_C nil)
+    (clue3 formula-decl nil th_C nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (L5 formula-decl nil th_C nil)
+    (E? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (E adt-constructor-decl "(E?)" th_C nil)
+    (L2 formula-decl nil th_C nil)
+    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (B adt-constructor-decl "(B?)" th_C nil)
+    (L3 formula-decl nil th_C nil)
+    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (A adt-constructor-decl "(A?)" th_C nil)
+    (D adt-constructor-decl "(D?)" th_C nil)
+    (D? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (people type-decl nil th_C nil) (Range formula-decl nil th_C nil))
+   shostak))
+ (L7 0
+  (L7-1 nil 3666633596
+   ("" (lemma "clue5")
+    (("" (lemma "L6")
+      (("" (lemma "Range")
+        (("" (lemma "Unique")
+          (("" (inst -2 "C")
+            (("" (split -2)
+              (("1" (lemma "L3")
+                (("1" (inst -3 "A" "C") (("1" (assert) nil nil)) nil))
+                nil)
+               ("2" (lemma "L2")
+                (("2" (inst -3 "B" "C") (("2" (assert) nil nil)) nil))
+                nil)
+               ("3" (assert) nil nil) ("4" (assert) nil nil)
+               ("5" (assert) nil nil) ("6" (assert) nil nil)
+               ("7" (assert) nil nil))
+              nil))
+            nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   ((L6 formula-decl nil th_C nil) (Unique formula-decl nil th_C nil)
+    (A adt-constructor-decl "(A?)" th_C nil)
+    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (L3 formula-decl nil th_C nil)
+    (B adt-constructor-decl "(B?)" th_C nil)
+    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L2 formula-decl nil th_C nil)
+    (C adt-constructor-decl "(C?)" th_C nil)
+    (C? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (people type-decl nil th_C nil) (Range formula-decl nil th_C nil)
+    (clue5 formula-decl nil th_C nil))
+   shostak))
+ (L8 0
+  (L8-1 nil 3666634180
+   ("" (lemma "Unique")
+    (("" (lemma "Range")
+      (("" (inst -1 "F")
+        (("" (split -1)
+          (("1" (lemma "L3")
+            (("1" (inst -3 "A" "F") (("1" (assert) nil nil)) nil)) nil)
+           ("2" (lemma "L2")
+            (("2" (inst -3 "B" "F") (("2" (assert) nil nil)) nil)) nil)
+           ("3" (lemma "L7")
+            (("3" (inst -3 "C" "F")
+              (("3" (assert)
+                (("3" (flatten -1)
+                  (("3" (lemma "Unique")
+                    (("3" (inst -1 "C" "F") (("3" (assert) nil nil))
+                      nil))
+                    nil))
+                  nil))
+                nil))
+              nil))
+            nil)
+           ("4" (lemma "L7")
+            (("4" (flatten -1)
+              (("4" (inst -4 "D" "F") (("4" (assert) nil nil)) nil))
+              nil))
+            nil)
+           ("5" (lemma "L5")
+            (("5" (inst -3 "E" "F") (("5" (assert) nil nil)) nil)) nil)
+           ("6" (propax) nil nil)
+           ("7" (lemma "L4")
+            (("7" (inst -3 "F" "G") (("7" (assert) nil nil)) nil))
+            nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   ((Range formula-decl nil th_C nil)
+    (A adt-constructor-decl "(A?)" th_C nil)
+    (A? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L3 formula-decl nil th_C nil)
+    (B adt-constructor-decl "(B?)" th_C nil)
+    (B? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L2 formula-decl nil th_C nil)
+    (C adt-constructor-decl "(C?)" th_C nil)
+    (C? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L7 formula-decl nil th_C nil)
+    (D? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (D adt-constructor-decl "(D?)" th_C nil)
+    (E adt-constructor-decl "(E?)" th_C nil)
+    (E? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L5 formula-decl nil th_C nil)
+    (G adt-constructor-decl "(G?)" th_C nil)
+    (G? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (L4 formula-decl nil th_C nil)
+    (F adt-constructor-decl "(F?)" th_C nil)
+    (F? adt-recognizer-decl "[people -> boolean]" th_C nil)
+    (boolean nonempty-type-decl nil booleans nil)
+    (people type-decl nil th_C nil) (Unique formula-decl nil th_C nil))
+   shostak)))
+