Changeset 2443 for src/joint/lineariseProof.ma

Timestamp:

Nov 8, 2012, 2:27:54 PM (8 years ago)

Author:

tranquil

Message:

changed joint's stack pointer and internal stack

File:

• src/joint/lineariseProof.ma (modified) (3 diffs)

src/joint/lineariseProof.ma

@@ -20 +20 @@
 definition graph_abstract_status:
  ∀p:unserialized_params. 
-  (∀F.more_sem_unserialized_params p F) →
+  (∀F.sem_unserialized_params p F) →
     joint_program (mk_graph_params p) →
      abstract_status
@@ -27 +27 @@
   joint_abstract_status
    (mk_prog_params
-    (make_sem_graph_params (mk_graph_params p) (p' ?))
-    prog ⊥).
-@daemon (* I/O, TODO *)
-qed.
+    (make_sem_graph_params p p')
+    prog).
 
 definition lin_abstract_status:
  ∀p:unserialized_params. 
-  (∀F.more_sem_unserialized_params p F) →
+  (∀F.sem_unserialized_params p F) →
     joint_program (mk_lin_params p) →
      abstract_status
@@ -41 +39 @@
   joint_abstract_status
    (mk_prog_params
-    (make_sem_lin_params (mk_lin_params p) (p' ?))
-    prog ⊥).
-@daemon (* I/O, TODO *)
-qed.
+    (make_sem_lin_params p p')
+    prog).
 
 definition linearise_status_rel: