Assignment 6

7 files changed, 624 insertions, 0 deletions

diff --git a/assignment6/A.prf b/assignment6/A.prf
new file mode 100644
index 0000000..fa3f6cb
--- /dev/null
+++ b/assignment6/A.prf
@@ -0,0 +1,109 @@
+(th_A
+ (A_0 0
+  (A_0-1 nil 3666631220
+   ("" (flatten)
+    (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
+    nil)
+   nil shostak))
+ (A_1 0
+  (A_1-1 nil 3666631598
+   ("" (flatten)
+    (("" (split)
+      (("1" (propax) nil nil) ("2" (propax) nil nil)
+       ("3" (propax) nil nil))
+      nil))
+    nil)
+   nil shostak))
+ (A_2 0
+  (A_2-1 nil 3666631791
+   ("" (split)
+    (("1" (flatten)
+      (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+        nil))
+      nil)
+     ("2" (flatten)
+      (("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+        nil))
+      nil))
+    nil)
+   nil shostak))
+ (A_3 0
+  (A_3-1 nil 3666631839
+   ("" (split)
+    (("1" (flatten)
+      (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+        nil))
+      nil)
+     ("2" (flatten)
+      (("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+        nil))
+      nil))
+    nil)
+   nil shostak))
+ (A_4 0
+  (A_4-1 nil 3666631883
+   ("" (split)
+    (("1" (flatten)
+      (("1" (split)
+        (("1" (propax) nil nil) ("2" (propax) nil nil)
+         ("3" (propax) nil nil))
+        nil))
+      nil)
+     ("2" (flatten)
+      (("2" (split)
+        (("1" (propax) nil nil) ("2" (propax) nil nil)
+         ("3" (propax) nil nil))
+        nil))
+      nil))
+    nil)
+   nil shostak))
+ (A_5 0
+  (A_5-1 nil 3666632405
+   ("" (split)
+    (("1" (flatten)
+      (("1" (split)
+        (("1" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+          nil)
+         ("2" (split)
+          (("1" (propax) nil nil)
+           ("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+            nil))
+          nil))
+        nil))
+      nil)
+     ("2" (flatten)
+      (("2" (split)
+        (("1" (split) (("1" (flatten) nil nil) ("2" (flatten) nil nil))
+          nil)
+         ("2" (flatten)
+          (("2" (split)
+            (("1" (propax) nil nil) ("2" (flatten) nil nil)) nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   nil shostak))
+ (A_6 0
+  (A_6-1 nil 3666632493
+   ("" (split)
+    (("1" (flatten)
+      (("1" (split)
+        (("1" (split) (("1" (flatten) nil nil) ("2" (flatten) nil nil))
+          nil)
+         ("2" (split) (("1" (flatten) nil nil) ("2" (flatten) nil nil))
+          nil))
+        nil))
+      nil)
+     ("2" (flatten)
+      (("2" (split)
+        (("1" (propax) nil nil)
+         ("2" (split)
+          (("1" (propax) nil nil)
+           ("2" (split) (("1" (propax) nil nil) ("2" (propax) nil nil))
+            nil))
+          nil))
+        nil))
+      nil))
+    nil)
+   nil shostak)))
+
diff --git a/assignment6/A.pvs b/assignment6/A.pvs
new file mode 100644
index 0000000..844e867
--- /dev/null
+++ b/assignment6/A.pvs
@@ -0,0 +1,58 @@
+%%%
+%%%    NAME/LOGIN-ID _____________________/______________________
+%%%
+%%%    ACKNOWLEDGMENTS:
+%%%      * List the names of people whom you worked with or who helped you
+%%%        with this assignment
+%%%      * Cite any references you used to complete this work
+%%%
+%%%    ===================
+%%%    Propositional Logic
+%%%    ===================
+%%%    
+%%%    Prove these theorems using only the (SPLIT) and (FLATTEN) commands
+%%%                               ~~~~
+
+th_A: Theory
+
+BEGIN
+
+%%% Elementary propositions.
+%%%
+
+p,q,r: bool
+
+%%% 
+%%% Propositional Formulas
+%%%
+%%%   (CLAIM, CONJECTURE, ..., THEOREM all mean the same thing)
+%%% 
+
+A_0: CLAIM  ((p => q) AND p) => q
+
+A_1: CONJECTURE  ((p AND q) AND r) => (p AND (q AND r))
+
+A_2: COROLLARY  NOT (p OR q) IFF (NOT p AND NOT q)
+
+A_3: FACT  NOT (p AND q) IFF (NOT p OR NOT q)
+
+A_4: FORMULA  (p => (q => r)) IFF (p AND q => r)
+
+A_5: LAW  (p AND (q OR r)) IFF (p AND q) OR (p AND r)
+
+A_6: LEMMA  (p OR (q AND r)) IFF (p OR q) AND (p OR r)
+
+A_7: PROPOSITION  ((p => q) AND (p => r)) IFF (p => (q AND r))
+
+A_8: SUBLEMMA  ((p => q) => (p AND q)) IFF ((NOT p => q) AND (q => p))
+
+A_9: THEOREM  ((p OR q) AND r) => (p AND (q AND r))
+
+A_10: CLAIM p => (q => p)
+
+A_11: CLAIM ((p => (q => r)) => ((p => q) => (p => r)))
+
+A_12: CLAIM ((NOT q) => (NOT p)) => (((NOT q) => p) => q)
+
+END th_A
+
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)))
+
diff --git a/assignment6/B.pvs b/assignment6/B.pvs
new file mode 100644
index 0000000..d4aad00
--- /dev/null
+++ b/assignment6/B.pvs
@@ -0,0 +1,44 @@
+%%%    NAME/LOGIN-ID    _____________________/______________________
+%%%    ACKNOWLEDGMENTS:
+
+%%%
+%%%    ===============
+%%%    Predicate Logic -  Propositional formulas involving quantifiers
+%%%    ===============
+%%%
+%%%   Prove these using only (SPLIT), (FLATTEN), (INST) and (SKOLEM) commands
+%%%                     ~~~~
+
+
+th_B: THEORY
+BEGIN
+
+U: TYPE+                        % Arbitrary nonempty type
+
+a,b,c: U                        % Constants of type U
+
+x,y,z: VAR U                    % Variables of type U
+
+P,Q,R: [U -> bool]              % Predicate names
+
+
+B_0: LEMMA  (FORALL x: P(x)) => P(a)
+
+B_1: LEMMA  ((FORALL x: P(x) => Q(x)) AND P(a)) => Q(a)
+
+B_2: LEMMA  (FORALL x: P(x)) => (EXISTS y: P(y))
+
+B_3: LEMMA  (FORALL x: P(x)) OR (EXISTS y: NOT P(y))
+
+B_4: LEMMA  NOT (FORALL x: P(x)) IFF (EXISTS x: NOT P(x))
+
+B_5: LEMMA  NOT (EXISTS x: P(x)) IFF (FORALL x: NOT P(x))
+
+B_6: LEMMA  (FORALL x: P(x)) AND (FORALL x: Q(x))
+                  IFF (FORALL x: P(x) AND Q(x))
+
+B_7: LEMMA  (EXISTS x: P(x)) OR (EXISTS x: Q(x))
+                  IFF (EXISTS x: P(x) OR Q(x))
+                  
+
+END th_B
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)))
+
diff --git a/assignment6/C.pvs b/assignment6/C.pvs
new file mode 100644
index 0000000..add36e3
--- /dev/null
+++ b/assignment6/C.pvs
@@ -0,0 +1,80 @@
+%%%    Name/LOGIN-ID    Camil Staps / s4498062
+%%%    ACKNOWLEDGMENTS:
+
+th_C: THEORY
+%%%
+%%%   Prove using only (SPLIT), (FLATTEN), (INST), (SKOLEM), (LEMMA), (ASSERT)
+%%%               ~~~~
+
+BEGIN
+
+%%%
+%%% Andy, Bob, Cindy, Dinah, Eve, Fred, and Gary live in the seven houses,
+%%% numbered 1 through 7, on Maple Steet.  Gary's address is 5 greater than
+%%% Bob's.  Bob's address is greater than Andy's.  Dinah's address is
+%%% less than Eve's, whose address is 2 less than Gary's.  Cindy's address
+%%% is less than either Dinah's or Fred's. Who lives where?
+%%%
+
+people: TYPE = {A, B, C, D, E, F, G}
+address: [people -> int]
+
+p,q: VAR people
+
+%%%
+%%% The axiom below asserts that each person's address is between 1 and 7.
+%%%
+Range: AXIOM address(p) = 1
+          or address(p) = 2
+          or address(p) = 3
+          or address(p) = 4
+          or address(p) = 5
+          or address(p) = 6
+          or address(p) = 7
+
+%%%
+%%% The axiom below states that each person's address is unique
+%%%
+
+Unique: AXIOM address(p) = address(q) implies p = q
+
+%%%
+%%% AXIOMs "clue1" through "clue7" translate the problem.
+%%% The lemmas, together, give a solution.  Each lemma
+%%% is introduced as it becomes provable.
+%%%
+
+clue1: AXIOM address(B) + 5 = address(G)
+
+L1: LEMMA address(B) = 1 or address(B) = 2
+
+clue2: AXIOM address(B) > address(A)
+
+L2: LEMMA address(B) = 2
+L3: LEMMA address(A) = 1
+L4: LEMMA address(G) = 7
+
+clue3: AXIOM address(D) < address(E)
+clue4: AXIOM address(E) + 2 = address(G)
+
+L5: LEMMA address(E) = 5
+L6: LEMMA address(D) = 3 or address(D) = 4
+
+clue5: AXIOM address(C) < address(D)
+
+L7: LEMMA address(C) = 3 and address(D) = 4
+
+clue7: AXIOM address(C) < address(F)
+
+L8: LEMMA address(F) = 6
+
+END th_C
+
+
+
+
+
+
+
+
+
diff --git a/assignment6/C.status b/assignment6/C.status
new file mode 100644
index 0000000..4db8b50
--- /dev/null
+++ b/assignment6/C.status
@@ -0,0 +1,12 @@
+ Proof summary for theory th_C
+    L1....................................proved - complete   [shostak](0.13 s)
+    L2....................................proved - complete   [shostak](0.03 s)
+    L3....................................proved - complete   [shostak](0.01 s)
+    L4....................................proved - complete   [shostak](0.02 s)
+    L5....................................proved - complete   [shostak](0.01 s)
+    L6....................................proved - complete   [shostak](0.09 s)
+    L7....................................proved - complete   [shostak](0.07 s)
+    L8....................................proved - complete   [shostak](0.08 s)
+    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.44 s)
+
+Grand Totals: 8 proofs, 8 attempted, 8 succeeded (0.44 s)