Library BioFLL.ReachabilityProperties

Require Import LL.SequentCalculiBasicTheory.
Require Import Definitions.
Require Import Utils.

Reachability Properties of the system

Property 1

Is it possible for a CTC, with mutations EPCAM,CD47 and fitness 3 , to become an extravasating CTC with fitness 8 ? What is the time delay for such transition ?

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 [] .
Proof with solveF .
  idtac "Proving Property 1" .
  intros.
  applyRule (blec2 3).
  applyRule (blecc2 5).
  applyRule (bleccm2 7).
  eapply tri_dec1 with (F:= E { fun (T : Type) (x : T) ⇒ perp TX { var x }} ** C { n; bone ; 8; EPCDCDME } ⁻) ...
  eapply tri_tensor ...
  eapply tri_ex with (t:= (d72 7) s + (d52 5) s + (d42 3) s + (Cte t)) ...
  eapply Init1...
  eapply Init1...
Qed.

Property 2

What is the time delay for a CTC with mutations EPCAM, CD47 and fitness 3 or 4 to become an extravasating CTC with fitness between 6 and 9 ?

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 }⁺ ] .
Proof with solveF.
  idtac "Proving Property 2" .
  intros.
  tri_negP.
  +
    applyRule (blec0 3).
    applyRule (blec2 2).
    applyRule (blecc0 4).
    applyRule (blecc2 3).
    applyRule (bleccm2 5).
    eapply tri_dec1 with (F:= E { fun _ x ⇒ perp (TX { var x } )} ** ( (Perp C { n ; bone ; 6 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 7 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 8 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 9 ; EPCDCDME }) )) ...
    eapply tri_tensor ...
    eapply tri_ex with (t:= d72 5 s + d52 3 s + d50 4 s + d42 2 s + d40 3 s + Cte t) ...
    eapply Init1...
    eapply tri_plus1 ...
    eapply tri_plus1 ...
    eapply tri_plus1 ...
    eapply Init1...
  +
    applyRule (blec0 4) .
    applyRule (blec2 3) .
    applyRule (blecc0 5) .
    applyRule (blecc2 4) .
    applyRule (bleccm2 6) .
    eapply tri_dec1 with (F:= E { fun _ x ⇒ perp (TX { var x } )} ** ( (Perp C { n ; bone ; 6 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 7 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 8 ; EPCDCDME }) ⊕ (Perp C {n ; bone ; 9 ; EPCDCDME }) )) ...
    eapply tri_tensor ...
    eapply tri_ex with (t:= d72 6 s + d52 4 s + d50 5 s + d42 3 s + d40 4 s + Cte t) ...
    eapply Init1 ...
    eapply tri_plus1 ...
    eapply tri_plus1 ...
    eapply tri_plus2 ...
    eapply Init1 ...
Qed.

Property 3

A cell in the breast, with mutation EP , might have his fitness oscillating from 1 to 2 and back ?

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 [] .
Proof with solveF .
  idtac "Property3: Proving Cycle 1" .
  intros.
  eexists.
  applyRule (bre0r 1).
  eapply tri_dec1 with (F:= E { fun (T : Type) (x : T) ⇒ perp TX { DX { d20 2, var x }}} ** C { n; breast ; 2; EP } ⁻ ) ...
  eapply tri_tensor ...
  eapply tri_ex with (t:= (Cte t)) ...
  eapply Init1...
  eapply Init1...
Qed.

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 [] .
Proof with solveF .
  idtac "Property3: Proving Cycle 2" .
  intros.
  eexists.
  applyRule (bre0 2).
  eapply tri_dec1 with (F:= E { fun (T : Type) (x : T) ⇒ perp TX { DX { d20 2, var x }}} ** C { n; breast ; 1; EP } ⁻ ) ...
  eapply tri_tensor ...
  eapply tri_ex with (t:= (Cte t)) ...
  eapply Init1...
  eapply Init1...
Qed.