## Electronic Appendix

*A Logical Framework for Systems Biology*, Elisabetta de Maria,
Joëlle Despeyroux, and Amy P. Felty, in
*Proceedings of the First International Conference Formal Methods
in Macro-Biology (FMMB)*,
Springer-Verlag LNCS,
September 2014.
### Appendices A and B

### Extended Report

An extended version is available here. It
contains the sequent proofs of all 4 properties.
### Coq Files

The files run in Coq V8.4pl2.
They must be compiled in the order they are listed.
### Lambda Prolog Files

Tactic proof scripts for HyLL proofs of the 4 properties described in
the paper. (These scripts are read in by the Lambda Prolog prover and
translated to Coq script, which is imported and then fine-tuned to
complete the above Coq proof development.)
- property1.hyll: Property 1, version 1
- property1a.hyll: Property 1, version
2, subgoal 1
- property1b.hyll: Property 1, version
2, subgoal 2
- property2.hyll: Property 2
- property3_0.hyll: Property 3, base
case
- property3_1.hyll: Property 3, case
for rule 1
- property3_2.hyll: Property 3, case
for rule 2
- property3_3.hyll: Property 3, case
for rule 3
- property3_4.hyll: Property 3, case
for rule 4
- property3_5.hyll: Property 3, case
for rule 5
- property3_6.hyll: Property 3, case
for rule 6
- property4_1.hyll: Property 4, case
for rule 1
- property4_2.hyll: Property 4, case
for rule 2
- property4_3.hyll: Property 4, case
for rule 3
- property4_4.hyll: Property 4, case
for rule 4
- property4_5.hyll: Property 4, case
for rule 5
- property4_6.hyll: Property 4, case
for rule 6

The prover is available as a zip file. It runs in the trunk version
of the Teyjus implementation
of Lambda Prolog.