**Library LL:**Specification of linear logic (syntax, rules and basic proof theory)- LL.Syntax: Syntax of linear logic formulas
- LL.SequentCalculi: Focused sequent calculus for linear logic

**Library BioLL:**Definition of biological rules, automation techniques and proofs of properties of interest- BioFLL.Definitions: Encoding of biochemical rules as linear logic formulas
- BioFLL.Utils: Auxiliary results
- BioFLL.InversionTactics: Tactics that ease the proof of properties
- BioFLL.ReachabilityProperties: Reachability Properties of the system
- BioFLL.MetaLevelProperties: Properties that require reasoning on the meta-level

[DFLO18] | Joëlle Despeyroux, Amy Felty, Pietro Lio and Carlos Olarte: A Logical Framework for Modelling Breast Cancer Progression Submitted to MLCSB'18. (PDF). |

```
Lemma Property1: ∀ n t,
```

|-F- Theory ; [ E{ fun _ x ⇒ perp (TX{ var x} )} ** (C{ n; bone; 8; EPCDCDME} ⁻) ;

Atom T{ Cte t} ; Atom C{ n ; blood ; 3 ; EPCD}] ; UP [] .

```
Lemma Property2: ∀ n t,
```

|-F- Theory ; [E{ fun _ x ⇒ perp (TX{ var x} )} ** ( (C{ n ; bone ; 6 ; EPCDCDME} ⁻)

⊕ (C{n ; bone ; 7 ; EPCDCDME}⁻) ⊕ (C{n ; bone ; 8 ; EPCDCDME}⁻ )

⊕ (C{n ; bone ; 9 ; EPCDCDME}⁻) )] ;

UP [T{ Cte t} ⁺ ; C{ n ; blood ; 3 ; EPCD}⁺ & C{ n ; blood ; 4 ; EPCD}⁺ ] .

```
Lemma Property3_Seq1: ∀ n t,
```

∃ d,
|-F- Theory ; [ E{ fun _ x ⇒ perp TX{ fc1 d (var x)}} ** (C{ n; breast; 2; EP} ⁻) ;

Atom T{ Cte t} ; Atom C{ n ; breast ; 1 ; EP}] ; UP [] .

Lemma Property3_Seq2: ∀ n t,
∃ d,

|-F- Theory ; [ E{ fun _ x ⇒ perp TX{ fc1 d (var x)}} ** (C{ n; breast; 1; EP} ⁻) ;

Atom T{ Cte t} ; Atom C{ n ; breast ; 2 ; EP}] ; UP [] .

```
Proposition Property4 :
```

∀ (n t :nat) c lm ,

|-F- Theory ; [ Atom T{ Cte t} ; Atom C{ n ; c; 0 ; lm} ] ; UP [] →

∃ d, |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom A{ n } ] ; UP [].

- acquiring passenger mutations: its fitness decreases by one and the driver mutations remain unchanged;
- going to apoptosis;
- acquiring a driver mutation: its fitness increases by two;
- moving to the bone: its fitness increases by one and the driver mutations EPCAM, CD47, CD44, MET remain unchanged.

```
Definition GoalP5 (f n t m:nat) :=
```

|-F- Theory ; [ Atom T{ Cte t} ; Atom C{ n ; blood; f ; m} ] ; UP [] →

∃ (d m' :nat),

|-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;blood; f -1; m } ] ; UP [] ∨

|-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom A{ n} ] ; UP [] ∨

(|-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;blood; f +2; m' } ] ; UP [] ∧ (plusOne m m') ) ∨

(m = EPCDCDME ∧ |-F- Theory ; [ Atom T{ d s+ Cte t} ; Atom C{ n ;bone; f + 1; EPCDCDME } ] ; UP []) .

```
Proposition Property5 : ∀ (f n t m:nat) ,
```

GoalP4 f n t m.