Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/lineariseProof.ma

    r2442 r2443  
    2020definition graph_abstract_status:
    2121 ∀p:unserialized_params.
    22   (∀F.more_sem_unserialized_params p F) →
     22  (∀F.sem_unserialized_params p F) →
    2323    joint_program (mk_graph_params p) →
    2424     abstract_status
     
    2727  joint_abstract_status
    2828   (mk_prog_params
    29     (make_sem_graph_params (mk_graph_params p) (p' ?))
    30     prog ⊥).
    31 @daemon (* I/O, TODO *)
    32 qed.
     29    (make_sem_graph_params p p')
     30    prog).
    3331
    3432definition lin_abstract_status:
    3533 ∀p:unserialized_params.
    36   (∀F.more_sem_unserialized_params p F) →
     34  (∀F.sem_unserialized_params p F) →
    3735    joint_program (mk_lin_params p) →
    3836     abstract_status
     
    4139  joint_abstract_status
    4240   (mk_prog_params
    43     (make_sem_lin_params (mk_lin_params p) (p' ?))
    44     prog ⊥).
    45 @daemon (* I/O, TODO *)
    46 qed.
     41    (make_sem_lin_params p p')
     42    prog).
    4743
    4844definition linearise_status_rel:
Note: See TracChangeset for help on using the changeset viewer.