Changeset 2443 for src/joint/lineariseProof.ma
- Timestamp:
- Nov 8, 2012, 2:27:54 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/lineariseProof.ma
r2442 r2443 20 20 definition graph_abstract_status: 21 21 ∀p:unserialized_params. 22 (∀F. more_sem_unserialized_params p F) →22 (∀F.sem_unserialized_params p F) → 23 23 joint_program (mk_graph_params p) → 24 24 abstract_status … … 27 27 joint_abstract_status 28 28 (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). 33 31 34 32 definition lin_abstract_status: 35 33 ∀p:unserialized_params. 36 (∀F. more_sem_unserialized_params p F) →34 (∀F.sem_unserialized_params p F) → 37 35 joint_program (mk_lin_params p) → 38 36 abstract_status … … 41 39 joint_abstract_status 42 40 (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). 47 43 48 44 definition linearise_status_rel:
Note: See TracChangeset
for help on using the changeset viewer.