{-# OPTIONS --type-in-type #-}

module SigLemmas where

open import NeilPrelude
open import List hiding ([_])
open import TimeDeltaList
open import RealTime
open import SigVecs
open import Utilities
open import Properties
open import Logic
open import Maybe
open import CPLemmas
open import TimeDeltaListProps

------------------------------------------------------------------------------

ChangelessSVʳ⇒ChangelessSV : {as : SVDesc}  (s : SigVec as)  Always (ChangelessSVʳ {as} s  ChangelessSV {as} s)
ChangelessSVʳ⇒ChangelessSV s t₁ p t₂ lt = snd p t₂ lt

ChangelessSVʳ⇒Unchanging : {as : SVDesc}  (s : SigVec as)  Always (ChangelessSVʳ {as} s  Unchanging {as} s)
ChangelessSVʳ⇒Unchanging s t₁ p = fst p

------------------------------------------------------------------------------

lemS-HeqAt⇒HeqSample : {A : Set}  Stability  (s₁ s₂ : SigVec (S A))  Always (H (EqAt {S A} s₁ s₂)  H (EqSample {S A} s₁ s₂))
lemS-HeqAt⇒HeqSample stab (a₁ , cp₁) (a₂ , cp₂) t₁ Heq t₀ lt with lemCP-Hchange⇒eq cp₁ cp₂ (stab cp₁) (stab cp₂) t₁ Heq t₀ lt | Heq O (≤<ℜ₀-trans ≤ℜ₀-min lt)
... | eq | eq0 rewrite eq with reverse (cp₂ t₀)
...   | [] = just-inj eq0
...   | (δ , a)  δas = refl

lemS-HʳeqAt⇒HeqSample : {A : Set}  Stability  (s₁ s₂ : SigVec (S A))  Always ( (EqAt {S A} s₁ s₂)  EqSample {S A} s₁ s₂)
lemS-HʳeqAt⇒HeqSample stab (a₁ , cp₁) (._ , cp₂) O (refl , _) with lemCP-O-empty cp₁ (stab cp₁) | lemCP-O-empty cp₂ (stab cp₂)
... | eq₁ | eq₂ rewrite eq₁ | eq₂ = refl
lemS-HʳeqAt⇒HeqSample stab (a₁ , cp₁) (a₂ , cp₂) (t >0) Heq with lemCP-Hʳchange⇒eq cp₁ cp₂ (stab cp₁) (stab cp₂) (t >0) Heq | snd Heq O _
... | eq | eq0 rewrite eq with reverse (cp₂ (t >0))
...    | [] = just-inj eq0
...    | (δ , a)  δas = refl

lem-HeqAt⇒HeqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqAt {as} s₁ s₂)  H (EqSample {as} s₁ s₂))
lem-HeqAt⇒HeqSample {C _} stab s₁ s₂ t Heq = Heq
lem-HeqAt⇒HeqSample {E _} stab s₁ s₂ t Heq = Heq
lem-HeqAt⇒HeqSample {S _} stab s₁ s₂ t Heq = lemS-HeqAt⇒HeqSample stab s₁ s₂ t Heq
lem-HeqAt⇒HeqSample {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t Heq with ×-inj3' Heq
... | Heqa , Heqb = ×-cong3 (lem-HeqAt⇒HeqSample {as} stab sa₁ sa₂ t Heqa) (lem-HeqAt⇒HeqSample {bs} stab sb₁ sb₂ t Heqb)

lem-HʳeqAt⇒eqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always ( (EqAt {as} s₁ s₂)  EqSample {as} s₁ s₂)
lem-HʳeqAt⇒eqSample {C _} stab s₁ s₂ t Heq = fst Heq
lem-HʳeqAt⇒eqSample {E _} stab s₁ s₂ t Heq = fst Heq
lem-HʳeqAt⇒eqSample {S _} stab s₁ s₂ t Heq = lemS-HʳeqAt⇒HeqSample stab s₁ s₂ t Heq
lem-HʳeqAt⇒eqSample {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t (eq , Heq) with ×-inj eq | ×-inj3' Heq
... | eqa , eqb | Heqa , Heqb  = ×-cong (lem-HʳeqAt⇒eqSample {as} stab sa₁ sa₂ t (eqa , Heqa)) (lem-HʳeqAt⇒eqSample {bs} stab sb₁ sb₂ t (eqb , Heqb))

lem-HʳeqAt⇒HʳeqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always ( (EqAt {as} s₁ s₂)   (EqSample {as} s₁ s₂))
lem-HʳeqAt⇒HʳeqSample {as} stab s₁ s₂ t (eq , Heq) = lem-HʳeqAt⇒eqSample {as} stab s₁ s₂ t (eq , Heq) , lem-HeqAt⇒HeqSample {as} stab s₁ s₂ t Heq

lem-AlwaysEqAt→AlwaysEqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (EqAt {as} s₁ s₂)  Always (EqSample {as} s₁ s₂)
lem-AlwaysEqAt→AlwaysEqSample {as} stab s₁ s₂ eqA t = lem-HʳeqAt⇒eqSample {as} stab s₁ s₂ t (eqA t , λ t' _  eqA t')

------------------------------------------------------------------------------

-- Creating changeless signal vectors

takeChangesInclC : {A : Set}  SigVec (C A)  (t : Time)  SigVec (C A)
takeChangesInclC s t t' with compareLeq t' t
... | leq p  = s t'
... | more p = s t

takeChangesInclE : {A : Set}  SigVec (E A)  (t : Time)  SigVec (E A)
takeChangesInclE (ma , cp) t = ma ,  t'  takeIncl t (cp t'))

takeChangesInclS : {A : Set}  SigVec (S A)  (t : Time)  SigVec (S A)
takeChangesInclS (a , cp) t = a ,  t'  takeIncl t (cp t'))

takeChangesIncl : {as : SVDesc}  SigVec as  (t : Time)  SigVec as
takeChangesIncl {C _} s t = takeChangesInclC s t
takeChangesIncl {E _} s t = takeChangesInclE s t
takeChangesIncl {S _} s t = takeChangesInclS s t
takeChangesIncl {as , bs} (sa , sb) t = takeChangesIncl {as} sa t , takeChangesIncl {bs} sb t

lem-ChangelessSVTakeInclC : {A : Set}  (s : SigVec (C A))  (t : Time)  ChangelessSV {C A} (takeChangesInclC  s t) t
lem-ChangelessSVTakeInclC s t₀ t₃ lt t₁ t₂ (p , q) (r , u) with compareLeq t₁ t₀ | compareLeq t₂ t₀
... | leq lt₂  | leq lt₃  = cong s (trans (≤ℜ₀-antisym lt₂ p) (≤ℜ₀-antisym r lt₃)) 
... | leq lt₂  | more lt₃ = cong s (≤ℜ₀-antisym lt₂ p)
... | more lt₂ | leq lt₃  = cong s (≤ℜ₀-antisym r lt₃)
... | more lt₂ | more lt₃ = refl

lem-ChangelessSVTakeIncl : {as : SVDesc}  Stability  (s : SigVec as)  (t : Time)  ChangelessSV {as} (takeChangesIncl {as} s t) t
lem-ChangelessSVTakeIncl {C _} stab s t = lem-ChangelessSVTakeInclC s t
lem-ChangelessSVTakeIncl {E _} stab (a , cp) t = λ t₂ lt₁ lt₂  lemCP-stable-eq cp (stab cp) (inl lt₁)
lem-ChangelessSVTakeIncl {S _} stab (a , cp) t = λ t₂ lt₁ lt₂  lemCP-stable-eq cp (stab cp) (inl lt₁)
lem-ChangelessSVTakeIncl {as , bs} stab (sa , sb) t = lem-ChangelessSVTakeIncl {as} stab sa t &₂
                                                    lem-ChangelessSVTakeIncl {bs} stab sb t

---------------------------------------

-- Probably redundant now

-- lem-takeInclChangeHEqAtC : {A : Set} → (s : SigVec (C A)) → (t : Time) → H (EqAt {C A} s (takeChangesInclC s t)) t
-- lem-takeInclChangeHEqAtC s t₁ t₀ lt with compareLeq t₀ t₁
-- ... | leq p = refl 
-- ... | more p = absurd (<ℜ₀-asym p lt)

-- lem-takeInclChangeHEqAtE : {A : Set} → (s : SigVec (E A)) → (t : Time) → H (EqAt {E A} s (takeChangesInclE s t)) t
-- lem-takeInclChangeHEqAtE (ma , cp) t₁ O lt = refl
-- lem-takeInclChangeHEqAtE (ma , cp) t₁ (t₀ >0) lt = lemCP-lookupTaken (inl lt) cp

-- lem-takeInclChangeHEqAtS : {A : Set} → (s : SigVec (S A)) → (t : Time) → H (EqAt {S A} s (takeChangesInclS s t)) t
-- lem-takeInclChangeHEqAtS (a , cp) t₁ O lt = refl
-- lem-takeInclChangeHEqAtS (ma , cp) t₁ (t₀ >0) lt = lemCP-lookupTaken (inl lt) cp

-- lem-takeInclChangeHEqAt : {as : SVDesc} → (s : SigVec as) → (t : Time) → H (EqAt {as} s (takeChangesIncl {as} s t)) t
-- lem-takeInclChangeHEqAt {C _} s t = lem-takeInclChangeHEqAtC s t
-- lem-takeInclChangeHEqAt {E _} s t = lem-takeInclChangeHEqAtE s t
-- lem-takeInclChangeHEqAt {S _} s t = lem-takeInclChangeHEqAtS s t
-- lem-takeInclChangeHEqAt {as , bs} (sa , sb) t = ×-cong3 (lem-takeInclChangeHEqAt {as} sa t) (lem-takeInclChangeHEqAt {bs} sb t)

-- lem-takeInclChangeEqAtC : {A : Set} → (s : SigVec (C A)) → (t : Time) → EqAt {C A} s (takeChangesInclC s t) t
-- lem-takeInclChangeEqAtC s t with compareLeq t t
-- ... | leq p = refl
-- ... | more p = refl

-- lem-takeInclChangeEqAtE : {A : Set} → (s : SigVec (E A)) → (t : Time) → EqAt {E A} s (takeChangesInclE s t) t
-- lem-takeInclChangeEqAtE (ma , cp) O = refl
-- lem-takeInclChangeEqAtE (ma , cp) (t >0) = lemCP-lookupTaken {_} {t >0} (inr refl) cp

-- lem-takeInclChangeEqAtS : {A : Set} → (s : SigVec (S A)) → (t : Time) → EqAt {S A} s (takeChangesInclS s t) t
-- lem-takeInclChangeEqAtS (a , cp) O = refl
-- lem-takeInclChangeEqAtS (a , cp) (t >0) = lemCP-lookupTaken {_} {t >0} (inr refl) cp

-- lem-takeInclChangeEqAt : {as : SVDesc} → (s : SigVec as) → (t : Time) → EqAt {as} s (takeChangesIncl {as} s t) t
-- lem-takeInclChangeEqAt {C _} s t = lem-takeInclChangeEqAtC s t
-- lem-takeInclChangeEqAt {E _} s t = lem-takeInclChangeEqAtE s t
-- lem-takeInclChangeEqAt {S _} s t = lem-takeInclChangeEqAtS s t
-- lem-takeInclChangeEqAt {as , bs} (sa , sb) t = ×-cong (lem-takeInclChangeEqAt {as} sa t) (lem-takeInclChangeEqAt {bs} sb t)

-- lem-takeInclChangeHʳEqAt : {as : SVDesc} → (s : SigVec as) → (t : Time) → Hʳ (EqAt {as} s (takeChangesIncl {as} s t)) t
-- lem-takeInclChangeHʳEqAt {as} = lem-takeInclChangeEqAt {as} &₂ lem-takeInclChangeHEqAt {as}

---------------------------------------

lemC-takeInclChangeHEqRep : {A : Set}  (s : SigVec (C A))  (t : Time)  H (EqRep {C A} s (takeChangesInclC s t)) t
lemC-takeInclChangeHEqRep s t₁ t₀ lt with compareLeq t₀ t₁
... | leq p = refl 
... | more p = absurd (<ℜ₀-asym p lt)

lemE-takeInclChangeHEqRep : {A : Set}  Stability  (s : SigVec (E A))  (t : Time)  H (EqRep {E A} s (takeChangesInclE s t)) t
lemE-takeInclChangeHEqRep stab (ma , cp) t₁ t₀ lt = ×-congL (sym (lemCP-take-Beyond cp (stab cp) (inl lt)))

lemS-takeInclChangeHEqRep : {A : Set}  Stability  (s : SigVec (S A))  (t : Time)  H (EqRep {S A} s (takeChangesInclS s t)) t
lemS-takeInclChangeHEqRep stab (a , cp) t₁ t₀ lt = ×-congL (sym (lemCP-take-Beyond cp (stab cp) (inl lt)))

lem-takeInclChangeHEqRep : {as : SVDesc}  Stability  (s : SigVec as)  (t : Time)  H (EqRep {as} s (takeChangesIncl {as} s t)) t
lem-takeInclChangeHEqRep {C _} stab s t = lemC-takeInclChangeHEqRep s t
lem-takeInclChangeHEqRep {E _} stab s t = lemE-takeInclChangeHEqRep stab s t
lem-takeInclChangeHEqRep {S _} stab s t = lemS-takeInclChangeHEqRep stab s t
lem-takeInclChangeHEqRep {as , bs} stab (sa , sb) t = ×-cong3 (lem-takeInclChangeHEqRep {as} stab sa t) (lem-takeInclChangeHEqRep {bs} stab sb t)

lemC-takeInclChangeEqRep : {A : Set}  (s : SigVec (C A))  (t : Time)  EqRep {C A} s (takeChangesInclC s t) t
lemC-takeInclChangeEqRep s t with compareLeq t t
... | leq p = refl
... | more p = refl

lemE-takeInclChangeEqRep : {A : Set}  Stability  (s : SigVec (E A))  (t : Time)  EqRep {E A} s (takeChangesInclE s t) t
lemE-takeInclChangeEqRep stab (ma , cp) t = ×-congL (stab cp (inr refl))

lemS-takeInclChangeEqRep : {A : Set}  Stability  (s : SigVec (S A))  (t : Time)  EqRep {S A} s (takeChangesInclS s t) t
lemS-takeInclChangeEqRep stab (a , cp) t = ×-congL (stab cp (inr refl))

lem-takeInclChangeEqRep : {as : SVDesc}  Stability  (s : SigVec as)  (t : Time)  EqRep {as} s (takeChangesIncl {as} s t) t
lem-takeInclChangeEqRep {C _} stab s t = lemC-takeInclChangeEqRep s t
lem-takeInclChangeEqRep {E _} stab s t = lemE-takeInclChangeEqRep stab  s t
lem-takeInclChangeEqRep {S _} stab s t = lemS-takeInclChangeEqRep stab  s t
lem-takeInclChangeEqRep {as , bs} stab (sa , sb) t = ×-cong (lem-takeInclChangeEqRep {as} stab sa t) (lem-takeInclChangeEqRep {bs} stab sb t)

lem-takeInclChangeHʳEqRep : {as : SVDesc}  Stability  (s : SigVec as)  (t : Time)   (EqRep {as} s (takeChangesIncl {as} s t)) t
lem-takeInclChangeHʳEqRep {as} stab = lem-takeInclChangeEqRep {as} stab &₂ lem-takeInclChangeHEqRep {as} stab

---------------------------------------

changelessBeyond : {as : SVDesc}  Stability  (s : SigVec as)  (t : Time)  Σ (SigVec as)  s'  (ChangelessSV {as} s' t ×  (EqRep {as} s s') t))
changelessBeyond {as} stab s t = takeChangesIncl {as} s t , lem-ChangelessSVTakeIncl {as} stab s t , lem-takeInclChangeHʳEqRep {as} stab s t

------------------------------------------------------------------------------

-- Doesn't work for C Signals !!!

-- takeChangesExclC : {A : Set} → SigVec (C A) → (t : Time) → SigVec (C A)
-- takeChangesExclC s t t' with compareGeq t' t
-- ... | less p = s t'
-- ... | geq  p = s ?

------------------------------------------------------------------------------

lemE-rep-eq-stable : {A : Set}  {t₀ t₁ : Time}  Stability  (s₁ s₂ : SigVec (E A))  t₀  t₁  EqRep {E A} s₁ s₂ t₁  EqRep {E A} s₁ s₂ t₀
lemE-rep-eq-stable stab (ma₁ , cp₁) (ma₂ , cp₂) lt eq with ×-inj eq
... | eqma , eqcp = ×-cong eqma (lemCP-eq-stable cp₁ cp₂ (stab cp₁) (stab cp₂) lt eqcp)

lemS-rep-eq-stable : {A : Set}  {t₀ t₁ : Time}  Stability  (s₁ s₂ : SigVec (S A))  t₀  t₁  EqRep {S A} s₁ s₂ t₁  EqRep {S A} s₁ s₂ t₀
lemS-rep-eq-stable stab (a₁ , cp₁) (a₂ , cp₂) lt eq with ×-inj eq
... | eqa , eqcp = ×-cong eqa (lemCP-eq-stable cp₁ cp₂ (stab cp₁) (stab cp₂) lt eqcp)

------------------------------------------------------------------------------

lemE-rep-at : {A : Set}  (s₁ s₂ : SigVec (E A))  Always (EqRep {E A} s₁ s₂  EqAt {E A} s₁ s₂)
lemE-rep-at (ma₁ , cp₁) (ma₂ , cp₂) t eq with ×-inj eq
lemE-rep-at (.ma₂ , cp₁) (ma₂ , cp₂) O eq | refl , eqcp = refl
lemE-rep-at (.ma₂ , cp₁) (ma₂ , cp₂) (t >0) eq | refl , eqcp = cong2R lookupTDL⁺ eqcp

lemS-rep-at : {A : Set}  (s₁ s₂ : SigVec (S A))  Always (EqRep {S A} s₁ s₂  EqAt {S A} s₁ s₂)
lemS-rep-at (a₁ , cp₁) (a₂ , cp₂) t eq with ×-inj eq
lemS-rep-at (.a₂ , cp₁) (a₂ , cp₂) O eq | refl , eqcp = refl
lemS-rep-at (.a₂ , cp₁) (a₂ , cp₂) (t >0) eq | refl , eqcp = cong2R lookupTDL⁺ eqcp

lem-rep-at : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always (EqRep {as} s₁ s₂  EqAt {as} s₁ s₂)
lem-rep-at {C _} s₁ s₂ t eq = eq
lem-rep-at {E _} s₁ s₂ t eq = lemE-rep-at s₁ s₂ t eq
lem-rep-at {S _} s₁ s₂ t eq = lemS-rep-at s₁ s₂ t eq
lem-rep-at {as , bs} (sa₁ , sb₁) (sa₂ , sb₂) t eq with ×-inj eq
... | eqa , eqb = ×-cong (lem-rep-at {as} sa₁ sa₂ t eqa) (lem-rep-at {bs} sb₁ sb₂ t eqb)

lem-rep-Hat : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always (H (EqRep {as} s₁ s₂)  H (EqAt {as} s₁ s₂))
lem-rep-Hat {as} s₁ s₂ t eq t' lt = lem-rep-at {as} s₁ s₂ t' (eq t' lt)

lem-rep-Hʳat : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always ( (EqRep {as} s₁ s₂)   (EqAt {as} s₁ s₂))
lem-rep-Hʳat {as} s₁ s₂ t = lem-rep-at {as} s₁ s₂ t  lem-rep-Hat {as} s₁ s₂ t


------------------------------------------------------------------------------

-- FALSE!!!
-- lemE-EqRep→EqSample : {A : Set} → (s₁ s₂ : SigVec (E A)) → (t₁ t₂ : Time) → rep {E A} s₁ t₁ ≡ rep {E A} s₂ t₂ → sample (E A) s₁ t₁ ≡ sample (E A) s₂ t₂
-- lemE-EqRep→EqSample (ma₁ , cp₁) (ma₂ , cp₂) t₁ t₂ eq with ×-inj eq
-- lemE-EqRep→EqSample (ma₁ , cp₁) (.ma₁ , cp₂) t₁ t₂ eq | refl , eqcp = lemCP-occ-eq cp₁ cp₂ t₁ t₂ eqcp

-- lemS-EqRep→EqSample : {A : Set} → (s₁ s₂ : SigVec (S A)) → (t₁ t₂ : Time) → rep {S A} s₁ t₁ ≡ rep {S A} s₂ t₂ → sample (S A) s₁ t₁ ≡ sample (S A) s₂ t₂
-- lemS-EqRep→EqSample (a₁ , cp₁) (a₂ , cp₂) t₁ t₂ eq with ×-inj eq
-- lemS-EqRep→EqSample (a₁ , cp₁) (.a₁ , cp₂) t₁ t₂ eq | refl , eqcp rewrite eqcp with reverse (cp₂ t₂)
-- ... | [] = refl
-- ... | (_ , a) ∷ _ = refl 

-- lem-EqRep→EqSample : {as : SVDesc} → (s₁ s₂ : SigVec as) → (t₁ t₂ : Time) → rep {as} s₁ t₁ ≡ rep {as} s₂ t₂ → sample as s₁ t₁ ≡ sample as s₂ t₂
-- lem-EqRep→EqSample {C _} s₁ s₂ t₁ t₂ eq = eq
-- lem-EqRep→EqSample {E _} s₁ s₂ t₁ t₂ eq = lemE-EqRep→EqSample s₁ s₂ t₁ t₂ eq
-- lem-EqRep→EqSample {S _} s₁ s₂ t₁ t₂ eq = lemS-EqRep→EqSample s₁ s₂ t₁ t₂ eq
-- lem-EqRep→EqSample {as , bs} (sa₁ , sb₁) (sa₂ , sb₂) t₁ t₂ eq with ×-inj eq
-- ... | eqa , eqb = ×-cong (lem-EqRep→EqSample {as} sa₁ sa₂ t₁ t₂ eqa)
--                          (lem-EqRep→EqSample {bs} sb₁ sb₂ t₁ t₂ eqb)

lemE-EqRep→EqSample : {A : Set}  (s₁ s₂ : SigVec (E A))  Always (EqRep {E A} s₁ s₂  EqSample {E A} s₁ s₂)
lemE-EqRep→EqSample (ma₁ , cp₁) (ma₂ , cp₂) t eq with ×-inj eq
lemE-EqRep→EqSample (ma₁ , cp₁) (.ma₁ , cp₂) O eq | refl , eqcp = refl
lemE-EqRep→EqSample (ma₁ , cp₁) (.ma₁ , cp₂) (t >0) eq | refl , eqcp rewrite eqcp = refl

lemS-EqRep→EqSample : {A : Set}  (s₁ s₂ : SigVec (S A))  Always (EqRep {S A} s₁ s₂  EqSample {S A} s₁ s₂)
lemS-EqRep→EqSample (a₁ , cp₁) (a₂ , cp₂) t eq with ×-inj eq
lemS-EqRep→EqSample (a₁ , cp₁) (.a₁ , cp₂) t eq | refl , eqcp rewrite eqcp with reverse (cp₂ t)
... | [] = refl
... | ((_ , a)  _) = refl

lem-EqRep→EqSample : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always (EqRep {as} s₁ s₂  EqSample {as} s₁ s₂)
lem-EqRep→EqSample {C _} s₁ s₂ t eq = eq
lem-EqRep→EqSample {E _} s₁ s₂ t eq = lemE-EqRep→EqSample s₁ s₂ t eq 
lem-EqRep→EqSample {S _} s₁ s₂ t eq = lemS-EqRep→EqSample s₁ s₂ t eq
lem-EqRep→EqSample {as , bs} (sa₁ , sb₁) (sa₂ , sb₂) t eq with ×-inj eq
... | eqa , eqb = ×-cong (lem-EqRep→EqSample {as} sa₁ sa₂ t eqa) (lem-EqRep→EqSample {bs} sb₁ sb₂ t eqb)

------------------------------------------------------------------------------

lem-UB-rep' : {as : SVDesc}  {t₀ t₂ : Time}  t₀ < t₂  (s : SigVec as)  UnchangingBetween {as} s t₀ t₂  rep {as} s t₀  rep {as} s t₂
lem-UB-rep' {C _} lt s un = un _ _ (inr refl , inl lt) (inl lt , inr refl)
lem-UB-rep' {E _} lt (ma , cp) un = ×-congL (un lt)
lem-UB-rep' {S _} lt (a , cp)  un = ×-congL (un lt)
lem-UB-rep' {as , bs} lt (sa , sb) (una , unb) = ×-cong (lem-UB-rep' {as} lt sa una) (lem-UB-rep' {bs} lt sb unb)

lem-UB-rep : {as : SVDesc}  {t₀ t₂ : Time}  t₀  t₂  (s : SigVec as)  UnchangingBetween {as} s t₀ t₂  rep {as} s t₀  rep {as} s t₂
lem-UB-rep (inr refl) _ _ = refl
lem-UB-rep {as} (inl lt) s un = lem-UB-rep' {as} lt s un

-- False!!!
-- lem-UB-sample' : {as : SVDesc} → {t₀ t₂ : Time} → t₀ < t₂ → (s : SigVec as) → UnchangingBetween {as} s t₀ t₂ → sample as s t₀ ≡ sample as s t₂
-- lem-UB-sample' {C _} lt s ub = ub _ _ (inr refl , inl lt) (inl lt , inr refl)
-- lem-UB-sample' {E _} lt (ma , cp) ub = {!!}
-- lem-UB-sample' {S _} {_} {t₂} lt (a , cp) ub rewrite (ub lt) with reverse (cp t₂)
-- ... | [] = refl
-- ... | (_ , a') ∷ _ = refl
-- lem-UB-sample' {as , bs} lt (sa , sb) (una , unb) = ×-cong (lem-UB-sample' {as} lt sa una) (lem-UB-sample' {bs} lt sb unb)

-- lem-UB-sample : {as : SVDesc} → {t₀ t₂ : Time} → t₀ ≤ t₂ → (s : SigVec as) → UnchangingBetween {as} s t₀ t₂ → sample as s t₀ ≡ sample as s t₂
-- lem-UB-sample {as} (inl lt) s ub = lem-UB-sample' {as} lt s ub
-- lem-UB-sample (inr refl) s ub = refl

------------------------------------------------------------------------------

lemS-HʳEqAt⇒Eq : {A : Set}   Stability  (s₁ s₂ : SigVec (S A))  Always ( (EqAt {S A} s₁ s₂)  EqRep {S A} s₁ s₂)
lemS-HʳEqAt⇒Eq stab (.ma₂ , cp₁) (ma₂ , cp₂) O (refl , Heq) = ×-congL (lemCP-O-equal cp₁ cp₂ (stab cp₁) (stab cp₂))
lemS-HʳEqAt⇒Eq stab (ma₁ , cp₁) (ma₂ , cp₂) (t >0) (eq , Heq) with Heq O _
lemS-HʳEqAt⇒Eq stab (.ma₂ , cp₁) (ma₂ , cp₂) (t >0) (eq , Heq) | refl = ×-congL (lemCP-Hʳchange⇒eq cp₁ cp₂ (stab cp₁) (stab cp₂) (t >0) (eq , Heq))

lemE-HʳEqAt⇒Eq : {A : Set}  Stability  (s₁ s₂ : SigVec (E A))  Always ( (EqAt {E A} s₁ s₂)  EqRep {E A} s₁ s₂)
lemE-HʳEqAt⇒Eq stab (.ma₂ , cp₁) (ma₂ , cp₂) O (refl , Heq) = ×-congL (lemCP-O-equal cp₁ cp₂ (stab cp₁) (stab cp₂))
lemE-HʳEqAt⇒Eq stab (ma₁ , cp₁) (ma₂ , cp₂) (t >0) (eq , Heq) with Heq O _
lemE-HʳEqAt⇒Eq stab (.ma₂ , cp₁) (ma₂ , cp₂) (t >0) (eq , Heq) | refl = ×-congL (lemCP-Hʳocc⇒eq cp₁ cp₂ (stab cp₁) (stab cp₂) (t >0) (eq , Heq))

lem-HʳEqAt⇒Eq : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always ( (EqAt {as} s₁ s₂)  EqRep {as} s₁ s₂)
lem-HʳEqAt⇒Eq {C _} stab s₁ s₂ t (eq , _) = eq
lem-HʳEqAt⇒Eq {E _} stab s₁ s₂ t eq = lemE-HʳEqAt⇒Eq stab s₁ s₂ t eq
lem-HʳEqAt⇒Eq {S _} stab s₁ s₂ t eq = lemS-HʳEqAt⇒Eq stab s₁ s₂ t eq
lem-HʳEqAt⇒Eq {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t (eq , Heq) with ×-inj eq | ×-inj3' Heq
... | eqa , eqb | Heqa , Heqb = ×-cong (lem-HʳEqAt⇒Eq {as} stab sa₁ sa₂ t (eqa , Heqa)) (lem-HʳEqAt⇒Eq {bs} stab sb₁ sb₂ t (eqb , Heqb))

lem-HEqAt⇒EqH : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqAt {as} s₁ s₂)  H (EqRep {as} s₁ s₂))
lem-HEqAt⇒EqH {as} stab s₁ s₂ t Heq t' lt = lem-HʳEqAt⇒Eq {as} stab s₁ s₂ t' (Heq t' lt , λ t'' lt'  Heq t'' (<ℜ₀-trans lt' lt))

lem-HʳEqAt⇒EqHʳ : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always ( (EqAt {as} s₁ s₂)   (EqRep {as} s₁ s₂))
lem-HʳEqAt⇒EqHʳ {as} stab s₁ s₂ t (eq , Heq) = lem-HʳEqAt⇒Eq {as} stab s₁ s₂ t (eq , Heq) , lem-HEqAt⇒EqH {as} stab s₁ s₂ t Heq

------------------------------------------------------------------------------

lem-AlwaysEqAt→AlwaysEqRep : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (EqAt {as} s₁ s₂)  Always (EqRep {as} s₁ s₂)
lem-AlwaysEqAt→AlwaysEqRep {as} stab s₁ s₂ eq t = lem-HʳEqAt⇒Eq {as} stab s₁ s₂ t (eq t , λ t' _  eq t')

lem-AlwaysEqAt→GʳEqRep : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (EqAt {as} s₁ s₂)  Always ( (EqRep {as} s₁ s₂))
lem-AlwaysEqAt→GʳEqRep {as} stab s₁ s₂ eq t = lem-AlwaysEqAt→AlwaysEqRep {as} stab s₁ s₂ eq t , λ t' _  lem-AlwaysEqAt→AlwaysEqRep {as} stab s₁ s₂ eq t'

------------------------------------------------------------------------------

lemC-UB-reduce : {A : Set}  {t₀ t₁ t₂ t₃ : Time}  (s : SigVec (C A))  t₁  [ t₀ , t₃ ]  t₂  [ t₀ , t₃ ]  UnchangingBetween {C A} s t₀ t₃  UnchangingBetween {C A} s t₁ t₂
lemC-UB-reduce s (p₁ , p₂) (q₁ , q₂) un tx ty (r₁ , r₂) (u₁ , u₂) = un tx ty (≤ℜ₀-trans p₁ r₁ , ≤ℜ₀-trans r₂ q₂) (≤ℜ₀-trans p₁ u₁ , ≤ℜ₀-trans u₂ q₂)

lem-UB-reduce : {as : SVDesc}  {t₀ t₁ t₂ t₃ : Time}  Stability  (s : SigVec as)  t₁  [ t₀ , t₃ ]  t₂  [ t₀ , t₃ ]  UnchangingBetween {as} s t₀ t₃  UnchangingBetween {as} s t₁ t₂
lem-UB-reduce {C _} stab s p q = lemC-UB-reduce s p q 
lem-UB-reduce {E _} stab (ma , cp) (p₁ , p₂) (q₁ , q₂) = λ un lt  lemCP-stable2 cp (stab cp) (p₁ , p₂) (q₁ , q₂) (lem-eq-strict cp un (≤ℜ₀-trans q₁ q₂))
lem-UB-reduce {S _} stab (a , cp) (p₁ , p₂) (q₁ , q₂) = λ un lt  lemCP-stable2 cp (stab cp) (p₁ , p₂) (q₁ , q₂) (lem-eq-strict cp un (≤ℜ₀-trans q₁ q₂))
lem-UB-reduce {as , bs} stab (sa , sb) p q = lem-UB-reduce {as} stab sa p q  lem-UB-reduce {bs} stab sb p q

lem-UB-reduceR : {as : SVDesc}  {t₀ t₁ t₂ : Time}  Stability  (s : SigVec as)  t₀  t₁  t₁  t₂  UnchangingBetween {as} s t₀ t₂  UnchangingBetween {as} s t₁ t₂
lem-UB-reduceR {as} stab s lt₁ lt₂ = lem-UB-reduce {as} stab s (lt₁ , lt₂) (≤ℜ₀-trans lt₁ lt₂ , inr refl)

------------------------------------------------------------------------------

lemC-UB→U-R : {A : Set}  (t₀ t₂ : Time)  (s : SigVec (C A))  t₀ < t₂  UnchangingBetween {C A} s t₀ t₂  Unchanging {C A} s t₂
lemC-UB→U-R t₀ t₃ s lt unch = t₀ , lt , lemC-UB→U-R-aux
  where
     lemC-UB→U-R-aux : (t₁ t₂ : Time)  t₁  [ t₀ , t₃ ]  t₂  [ t₀ , t₃ ]  s t₁  s t₂
     lemC-UB→U-R-aux t₁ t₂ (p , q) (r , u) = unch t₁ t₂ (p , q) (r , u)

lemE-EqRep→U : {A : Set}  {t₀ : Time}  Stability  (t₂ : Time)  (s : SigVec (E A))  t₀ < t₂  rep {E A} s t₀  rep {E A} s t₂  Unchanging {E A} s t₂
lemE-EqRep→U stab O s () eq
lemE-EqRep→U stab (t₂ >0) (ma , cp) lt eq with ×-inj eq
... | refl , eqcp rewrite lemCP-eq-lookup lt cp (stab cp) eqcp = id

lemS-EqRep→U : {A : Set}  {t₀ : Time}  Stability  (t₂ : Time)  (s : SigVec (S A))  t₀ < t₂  rep {S A} s t₀  rep {S A} s t₂  Unchanging {S A} s t₂
lemS-EqRep→U stab O s () eq
lemS-EqRep→U stab (t₂ >0) (a , cp) lt eq with ×-inj eq
... | refl , eqcp rewrite lemCP-eq-lookup lt cp (stab cp) eqcp = id

lemE-UB→U-R : {A : Set}  {t₀ : Time}  Stability  (t₂ : Time)  (s : SigVec (E A))  t₀ < t₂  UnchangingBetween {E A} s t₀ t₂  Unchanging {E A} s t₂
lemE-UB→U-R stab t₂ s lt un = lemE-EqRep→U stab t₂ s lt (lem-UB-rep {E _} (inl lt) s un)

lemS-UB→U-R : {A : Set}  {t₀ : Time}  Stability  (t₂ : Time)  (s : SigVec (S A))  t₀ < t₂  UnchangingBetween {S A} s t₀ t₂  Unchanging {S A} s t₂
lemS-UB→U-R stab t₂ s lt un = lemS-EqRep→U stab t₂ s lt (lem-UB-rep {S _} (inl lt) s un)

lem-UB→U-R : {as : SVDesc}  {t₀ t₁ : Time}  Stability  (s : SigVec as)  t₀ < t₁  UnchangingBetween {as} s t₀ t₁  Unchanging {as} s t₁
lem-UB→U-R {C _} stab s lt = lemC-UB→U-R _ _ s lt
lem-UB→U-R {E _} stab s lt = lemE-UB→U-R stab _ s lt
lem-UB→U-R {S _} stab s lt = lemS-UB→U-R stab _ s lt
lem-UB→U-R {as , bs} stab (sa , sb) lt = lem-UB→U-R {as} stab sa lt  lem-UB→U-R {bs} stab sb lt

lem-UB→U : {as : SVDesc}  {t₀ t₁ t₂ : Time}  Stability  (s : SigVec as)  t₁   t₀ , t₂ ]  UnchangingBetween {as} s t₀ t₂  Unchanging {as} s t₁
lem-UB→U {as} stab s (lt₁ , lt₂) unch = lem-UB→U-R {as} stab s lt₁ (lem-UB-reduce {as} stab s (inr refl , ≤ℜ₀-trans (inl lt₁) lt₂) (inl lt₁ , lt₂) unch)

------------------------------------------------------------------------------

lemC-UB : {A : Set}  {t₁ t₂ : Time}  (s : SigVec (C A))  t₁  t₂  UnchangingBetween {C A} s t₂ t₁
lemC-UB s lt t₁' t₂' (p₁ , p₂) (q₁ , q₂) = cong s (≤ℜ₀-antisym (≤ℜ₀-trans p₂ (≤ℜ₀-trans lt q₁)) (≤ℜ₀-trans q₂ (≤ℜ₀-trans lt p₁)))

lem-UB : {as : SVDesc}  {t₁ t₂ : Time}  (s : SigVec as)  t₁  t₂  UnchangingBetween {as} s t₂ t₁
lem-UB {C _} s lt = lemC-UB s lt
lem-UB {E _} (ma , cp) p =  q  absurd (<≤ℜ₀-asym q p))
lem-UB {S _} (a , cp) p =  q  absurd (<≤ℜ₀-asym q p))
lem-UB {as , bs} (sa , sb) lt = lem-UB {as} sa lt , lem-UB {bs} sb lt

------------------------------------------------------------------------------

lemE-U→nothing : {A : Set}  (s : SigVec (E A))  (t : Time)  Unchanging {E A} s t  at (E A) s t  nothing
lemE-U→nothing (ma , cp) O un = lem-isNothing un
lemE-U→nothing (ma , cp) (t >0) un = lem-isNothing un

lemE-U-Eq : {A : Set}  (s₁ s₂ : SigVec (E A))  Always (Unchanging {E A} s₁  Unchanging {E A} s₂  EqAt {E A} s₁ s₂)
lemE-U-Eq s₁ s₂ t un₁ un₂ = trans (lemE-U→nothing s₁ t un₁) (sym (lemE-U→nothing s₂ t un₂))

lemE-HEq⇒U⇒HʳEq : {A : Set}  (s₁ s₂ : SigVec (E A))  Always (H (EqAt {E A} s₁ s₂)  Unchanging {E A} s₁  Unchanging {E A} s₂   (EqAt {E A} s₁ s₂))
lemE-HEq⇒U⇒HʳEq s₁ s₂ t Heq un₁ un₂ = lemE-U-Eq s₁ s₂ t un₁ un₂ , Heq

lemE-HEq⇒U⇒EqRep : {A : Set}  Stability  (s₁ s₂ : SigVec (E A))  Always (H (EqAt {E A} s₁ s₂)  Unchanging {E A} s₁  Unchanging {E A} s₂  EqRep {E A} s₁ s₂)
lemE-HEq⇒U⇒EqRep stab s₁ s₂ t Heq un₁ un₂ = lemE-HʳEqAt⇒Eq stab s₁ s₂ t (lemE-HEq⇒U⇒HʳEq s₁ s₂ t Heq un₁ un₂)

lemE-EqH⇒U⇒EqR : {A : Set}  Stability  (s₁ s₂ : SigVec (E A))  Always (H (EqRep {E A} s₁ s₂)  Unchanging {E A} s₁  Unchanging {E A} s₂  EqRep {E A} s₁ s₂)
lemE-EqH⇒U⇒EqR stab s₁ s₂ t Heq un₁ un₂ = lemE-HEq⇒U⇒EqRep stab s₁ s₂ t (lem-rep-Hat {E _} s₁ s₂ t Heq) un₁ un₂

------------------------------------------------------------------------------

lemS-U→nothing : {A : Set}  (s : SigVec (S A))  (t : Time)  Unchanging {S A} s t  at (S A) s t  nothing
lemS-U→nothing (a , cp) O ()
lemS-U→nothing (a , cp) (t >0) un = lem-isNothing un

lemS-U-Eq : {A : Set}  (s₁ s₂ : SigVec (S A))  Always (Unchanging {S A} s₁  Unchanging {S A} s₂  EqAt {S A} s₁ s₂)
lemS-U-Eq s₁ s₂ t un₁ un₂ = trans (lemS-U→nothing s₁ t un₁) (sym (lemS-U→nothing s₂ t un₂))

lemS-HEq⇒U⇒HʳEq : {A : Set}  (s₁ s₂ : SigVec (S A))  Always (H (EqAt {S A} s₁ s₂)  Unchanging {S A} s₁  Unchanging {S A} s₂   (EqAt {S A} s₁ s₂))
lemS-HEq⇒U⇒HʳEq s₁ s₂ t Heq un₁ un₂ = lemS-U-Eq s₁ s₂ t un₁ un₂ , Heq

lemS-HEq⇒U⇒EqRep : {A : Set}  Stability  (s₁ s₂ : SigVec (S A))  Always (H (EqAt {S A} s₁ s₂)  Unchanging {S A} s₁  Unchanging {S A} s₂  EqRep {S A} s₁ s₂)
lemS-HEq⇒U⇒EqRep stab s₁ s₂ t Heq un₁ un₂ = lemS-HʳEqAt⇒Eq stab s₁ s₂ t (lemS-HEq⇒U⇒HʳEq s₁ s₂ t Heq un₁ un₂)

lemS-EqH⇒U⇒EqR : {A : Set}  Stability  (s₁ s₂ : SigVec (S A))  Always (H (EqRep {S A} s₁ s₂)  Unchanging {S A} s₁  Unchanging {S A} s₂  EqRep {S A} s₁ s₂)
lemS-EqH⇒U⇒EqR stab s₁ s₂ t Heq un₁ un₂ = lemS-HEq⇒U⇒EqRep stab s₁ s₂ t (lem-rep-Hat {S _} s₁ s₂ t Heq) un₁ un₂

------------------------------------------------------------------------------

lemC-EqH⇒U⇒EqR : {A : Set}  (s₁ s₂ : SigVec (C A))  Always (H (EqRep {C A} s₁ s₂)  Unchanging {C A} s₁  Unchanging {C A} s₂  s₁  s₂)
lemC-EqH⇒U⇒EqR s₁ s₂ t Heq (t₁ , lt₁ , p₁) (t₂ , lt₂ , p₂) with compareLeq t₁ t₂
... | leq  p  = trans2 (p₁ t t₂ (inl lt₁ , inr refl) (p , inl lt₂)) (Heq t₂ lt₂) (p₂ t₂ t (inr refl , inl lt₂) (inl lt₂ , inr refl))
... | more p  = trans2 (p₁ t t₁ (inl lt₁ , inr refl) (inr refl , inl lt₁)) (Heq t₁ lt₁) (p₂ t₁ t (inl p , inl lt₁) (inl lt₂ , inr refl))

------------------------------------------------------------------------------

lem-EqH⇒U⇒EqR : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqRep {as} s₁ s₂)  Unchanging {as} s₁  Unchanging {as} s₂  EqRep {as} s₁ s₂)
lem-EqH⇒U⇒EqR {C _} stab s₁ s₂ t Heq un₁ un₂ = lemC-EqH⇒U⇒EqR s₁ s₂ t Heq un₁ un₂
lem-EqH⇒U⇒EqR {E _} stab s₁ s₂ t Heq un₁ un₂ = lemE-EqH⇒U⇒EqR stab s₁ s₂ t Heq un₁ un₂
lem-EqH⇒U⇒EqR {S _} stab s₁ s₂ t Heq un₁ un₂ = lemS-EqH⇒U⇒EqR stab s₁ s₂ t Heq un₁ un₂
lem-EqH⇒U⇒EqR {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t Heq (una₁ , unb₁) (una₂ , unb₂) with ×-inj3' Heq
... | Heqa , Heqb = ×-cong (lem-EqH⇒U⇒EqR {as} stab sa₁ sa₂ t Heqa una₁ una₂) (lem-EqH⇒U⇒EqR {bs} stab sb₁ sb₂ t Heqb unb₁ unb₂)

lem-EqH⇒U⇒EqHʳ : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqRep {as} s₁ s₂)  Unchanging {as} s₁  Unchanging {as} s₂   (EqRep {as} s₁ s₂))
lem-EqH⇒U⇒EqHʳ {as} stab s₁ s₂ t Heq un₁ un₂ = lem-EqH⇒U⇒EqR {as} stab s₁ s₂ t Heq un₁ un₂ , Heq

lem-C→EqRep : {as : SVDesc}  {t₁ t₂ : Time}  (s : SigVec as)  t₁  t₂  ChangelessSV {as} s t₁  rep {as} s t₁  rep {as} s t₂
lem-C→EqRep {as} {t₁} {t₂} s (inl p) ch = lem-UB-rep {as} (inl p) s (ch t₂ p)
lem-C→EqRep s (inr refl) ch = refl

lem-EqHʳ⇒C⇒Eq : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always ( (EqRep {as} s₁ s₂)  ChangelessSV {as} s₁  ChangelessSV {as} s₂   _  Always (EqRep {as} s₁ s₂)))
lem-EqHʳ⇒C⇒Eq s₁ s₂ t (eq , Heq) ch₁ ch₂ t' with compare t' t
lem-EqHʳ⇒C⇒Eq s₁ s₂ t (eq , Heq) ch₁ ch₂ .t | refl   = eq
lem-EqHʳ⇒C⇒Eq s₁ s₂ t (eq , Heq) ch₁ ch₂ t' | less p = Heq t' p
lem-EqHʳ⇒C⇒Eq {as} s₁ s₂ t (eq , Heq) ch₁ ch₂ t' | more p = trans2 (sym (lem-C→EqRep {as} s₁ (inl p) ch₁)) eq (lem-C→EqRep {as} s₂ (inl p) ch₂)

lem-EqH⇒Cʳ⇒Eq : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqRep {as} s₁ s₂)  ChangelessSVʳ {as} s₁  ChangelessSVʳ {as} s₂   _  Always (EqRep {as} s₁ s₂)))
lem-EqH⇒Cʳ⇒Eq {as} stab s₁ s₂ t Heq ch₁ ch₂ = lem-EqHʳ⇒C⇒Eq {as} s₁ s₂ t (lem-EqH⇒U⇒EqHʳ {as} stab s₁ s₂ t Heq (ChangelessSVʳ⇒Unchanging {as} s₁ t ch₁) (ChangelessSVʳ⇒Unchanging {as} s₂ t ch₂)) (ChangelessSVʳ⇒ChangelessSV {as} s₁ t ch₁) (ChangelessSVʳ⇒ChangelessSV {as} s₂ t ch₂)

lem-HEq⇒Cʳ⇒GʳEq : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqAt {as} s₁ s₂)  ChangelessSVʳ {as} s₁  ChangelessSVʳ {as} s₂   (EqAt {as} s₁ s₂))
lem-HEq⇒Cʳ⇒GʳEq {as} stab s₁ s₂ t Heq ch₁ ch₂ with lem-EqH⇒Cʳ⇒Eq {as} stab s₁ s₂ t (lem-HEqAt⇒EqH {as} stab s₁ s₂ t Heq) ch₁ ch₂
... | eqA = lem-rep-at {as} s₁ s₂ t (eqA t) , λ t' _  lem-rep-at {as} s₁ s₂ t' (eqA t')

lem-HʳEq⇒C⇒GEq : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always ( (EqAt {as} s₁ s₂)  ChangelessSV {as} s₁  ChangelessSV {as} s₂  G (EqAt {as} s₁ s₂))
lem-HʳEq⇒C⇒GEq {as} stab s₁ s₂ t Heq ch₁ ch₂ t' _ with lem-EqHʳ⇒C⇒Eq {as} s₁ s₂ t (lem-HʳEqAt⇒EqHʳ {as} stab s₁ s₂ t Heq) ch₁ ch₂
... | eqA = lem-rep-at {as} s₁ s₂ t' (eqA t')

------------------------------------------------------------------------------

------------------------------------------------------------------

lemS-HEqSample⇒U⇒EqSample : {A : Set}  Stability  (s₁ s₂ : SigVec (S A))  Always (H (EqSample {S A} s₁ s₂)  Unchanging {S A} s₁  Unchanging {S A} s₂  EqSample {S A} s₁ s₂)
lemS-HEqSample⇒U⇒EqSample stab (a₁ , cp₁) (a₂ , cp₂) O Heq () ()
lemS-HEqSample⇒U⇒EqSample stab (a₁ , cp₁) (a₂ , cp₂) (t >0) Heq un₁ un₂ = lemCP-Hval⇒val cp₁ cp₂ (stab cp₁) (stab cp₂) t un₁ un₂ Heq

lemE-U⇒EqR : {A : Set}  (s₁ s₂ : SigVec (E A))  Always (Unchanging {E A} s₁  Unchanging {E A} s₂  EqSample {E A} s₁ s₂)
lemE-U⇒EqR (nothing , _) (nothing , _) O      un₁ un₂ = refl
lemE-U⇒EqR _             (just y' , _) O      un₁ un₂ = magic un₂
lemE-U⇒EqR (just _ , _)  _             O      un₁ un₂ = magic un₁
lemE-U⇒EqR (_ , fdas₁)   (_ , fdas₂)   (t >0) un₁ un₂ = lem-isNothingEq un₁ un₂

lemC-HEqSample⇒U⇒EqSample : {A : Set}  (s₁ s₂ : SigVec (C A))  Always (H (EqSample {C A} s₁ s₂)  Unchanging {C A} s₁  Unchanging {C A} s₂  EqSample {C A} s₁ s₂)
lemC-HEqSample⇒U⇒EqSample s₁ s₂ t Heq (t₁ , lt₁ , p₁) (t₂ , lt₂ , p₂) with compareℜ₀ t₁ t₂ | Heq t₁ lt₁ | Heq t₂ lt₂
lemC-HEqSample⇒U⇒EqSample s₁ s₂ t Heq (t₁ , lt₁ , p₁) (._ , lt₂ , p₂) | refl   | eq₁₂ | _     = trans2 (sym (p₁ t₁ t (inr refl , inl lt₂) (inl lt₂ , inr refl))) eq₁₂ (p₂ t₁ t (inr refl , inl lt₂) (inl lt₂ , inr refl))
lemC-HEqSample⇒U⇒EqSample s₁ s₂ t Heq (t₁ , lt₁ , p₁) (t₂ , lt₂ , p₂) | less q | _    | eq₂₁  = trans2 (sym (p₁ t₂ t (inl q , inl lt₂) (inl lt₁ , inr refl))) eq₂₁ (p₂ t₂ t (inr refl , inl lt₂) (inl lt₂ , inr refl))
lemC-HEqSample⇒U⇒EqSample s₁ s₂ t Heq (t₁ , lt₁ , p₁) (t₂ , lt₂ , p₂) | more q | eq₁₂ | _     = trans2 (sym (p₁ t₁ t (inr refl , inl lt₁) (inl lt₁ , inr refl))) eq₁₂ (p₂ t₁ t (inl q , inl lt₁) (inl lt₂ , inr refl))

lem-HEqSample⇒U⇒EqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqSample {as} s₁ s₂)  Unchanging {as} s₁  Unchanging {as} s₂  EqSample {as} s₁ s₂)
lem-HEqSample⇒U⇒EqSample {C _} stab s₁ s₂ t Heq un₁ un₂ = lemC-HEqSample⇒U⇒EqSample s₁ s₂ t Heq un₁ un₂
lem-HEqSample⇒U⇒EqSample {S _} stab s₁ s₂ t Heq un₁ un₂ = lemS-HEqSample⇒U⇒EqSample stab s₁ s₂ t Heq un₁ un₂
lem-HEqSample⇒U⇒EqSample {E _} stab s₁ s₂ t Heq un₁ un₂ = lemE-U⇒EqR s₁ s₂ t un₁ un₂
lem-HEqSample⇒U⇒EqSample {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t Heq (una₁ , unb₁) (una₂ , unb₂) with ×-split2' (result2' ×-inj Heq)
... | Heqa , Heqb = ×-cong (lem-HEqSample⇒U⇒EqSample {as} stab sa₁ sa₂ t Heqa una₁ una₂) (lem-HEqSample⇒U⇒EqSample {bs} stab sb₁ sb₂ t Heqb unb₁ unb₂)

lem-HEqSample⇒Cʳ⇒EqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqSample {as} s₁ s₂)  ChangelessSVʳ {as} s₁  ChangelessSVʳ {as} s₂  EqSample {as} s₁ s₂)
lem-HEqSample⇒Cʳ⇒EqSample {as} stab s₁ s₂ t Heq (un₁ , Gun₁) (un₂ , Gun₂) = lem-HEqSample⇒U⇒EqSample {as} stab s₁ s₂ t Heq un₁ un₂

------------------------------------------------------------------------------

lemC-HʳEqSample⇒ChangelessSV⇒GEqSample : {A : Set}  (s₁ s₂ : SigVec (C A))  Always (EqSample {C A} s₁ s₂  ChangelessSV {C A} s₁  ChangelessSV {C A} s₂  G (EqSample {C A} s₁ s₂))
lemC-HʳEqSample⇒ChangelessSV⇒GEqSample s₁ s₂ t₁ eq ch₁ ch₂ t₂ lt = trans2 (ch₁ t₂ lt t₂ t₁ (inl lt , inr refl) (inr refl , inl lt)) eq (ch₂ t₂ lt t₁ t₂ (inr refl , inl lt) (inl lt , inr refl))

lemE-HʳEqSample⇒ChangelessSV⇒GEqSample : {A : Set}  Stability  (s₁ s₂ : SigVec (E A))  Always (EqSample {E A} s₁ s₂  ChangelessSV {E A} s₁  ChangelessSV {E A} s₂  G (EqSample {E A} s₁ s₂))
lemE-HʳEqSample⇒ChangelessSV⇒GEqSample stab (ma₁ , cp₁) (ma₂ , cp₂) t₁ eq ch₁ ch₂ O ()
lemE-HʳEqSample⇒ChangelessSV⇒GEqSample stab (ma₁ , cp₁) (ma₂ , cp₂) O eq ch₁ ch₂ (t₂ >0) lt with lemCP-O-empty cp₁ (stab cp₁) | lemCP-O-empty cp₂ (stab cp₂)
... | eq₁ | eq₂ with trans (sym (ch₁ (t₂ >0) lt lt)) eq₁ | trans (sym (ch₂ (t₂ >0) lt lt)) eq₂
...     | eqe₁ | eqe₂ rewrite eqe₁ | eqe₂ = refl
lemE-HʳEqSample⇒ChangelessSV⇒GEqSample stab (ma₁ , cp₁) (ma₂ , cp₂) (t₁ >0) eq ch₁ ch₂ (t₂ >0) lt with ch₁ (t₂ >0) lt lt | ch₂ (t₂ >0) lt lt
... | eq₁ | eq₂ rewrite sym eq₁ | sym eq₂ = lemCP-lookupBeyondEq cp₁ cp₂ (stab cp₁) (stab cp₂) lt

lemS-HʳEqSample⇒ChangelessSV⇒GEqSample : {A : Set}  (s₁ s₂ : SigVec (S A))  Always (EqSample {S A} s₁ s₂  ChangelessSV {S A} s₁  ChangelessSV {S A} s₂  G (EqSample {S A} s₁ s₂))
lemS-HʳEqSample⇒ChangelessSV⇒GEqSample (a₁ , cp₁) (a₂ , cp₂) t₁ eq ch₁ ch₂ t₂ lt with ch₁ t₂ lt lt | ch₂ t₂ lt lt
... | eq₁ | eq₂ rewrite sym eq₁ | sym eq₂ with reverse (cp₁ t₁) | reverse (cp₂ t₁)
... | [] | [] = eq
... | (_ , a')  _ | [] = eq
... | [] | (_ , a')  _ = eq
... | (_ , a₁')  _ | (_ , a₂')  _ = eq

lem-EqSample⇒ChangelessSV⇒GEqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (EqSample {as} s₁ s₂  ChangelessSV {as} s₁  ChangelessSV {as} s₂  G (EqSample {as} s₁ s₂))
lem-EqSample⇒ChangelessSV⇒GEqSample {C _} stab s₁ s₂ t₁ eq ch₁ ch₂ = lemC-HʳEqSample⇒ChangelessSV⇒GEqSample s₁ s₂ t₁ eq ch₁ ch₂
lem-EqSample⇒ChangelessSV⇒GEqSample {E _} stab s₁ s₂ t₁ eq ch₁ ch₂ = lemE-HʳEqSample⇒ChangelessSV⇒GEqSample stab s₁ s₂ t₁ eq ch₁ ch₂
lem-EqSample⇒ChangelessSV⇒GEqSample {S _} stab s₁ s₂ t₁ eq ch₁ ch₂ = lemS-HʳEqSample⇒ChangelessSV⇒GEqSample s₁ s₂ t₁ eq ch₁ ch₂
lem-EqSample⇒ChangelessSV⇒GEqSample {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t₁ eq ch₁ ch₂ with ×-inj eq | ×-split2' ch₁ | ×-split2' ch₂
... | eqa , eqb | cha₁ , chb₁ | cha₂ , chb₂ = ×-cong3 (lem-EqSample⇒ChangelessSV⇒GEqSample {as} stab sa₁ sa₂ t₁ eqa cha₁ cha₂) (lem-EqSample⇒ChangelessSV⇒GEqSample {bs} stab sb₁ sb₂ t₁ eqb chb₁ chb₂)

------------------------------------------------------------------------------

lem-HEqSample⇒ChangelessSVʳ⇒GʳEqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (H (EqSample {as} s₁ s₂)  ChangelessSVʳ {as} s₁  ChangelessSVʳ {as} s₂   (EqSample {as} s₁ s₂))
lem-HEqSample⇒ChangelessSVʳ⇒GʳEqSample {as} stab s₁ s₂ t Heq ch₁ ch₂ with lem-HEqSample⇒Cʳ⇒EqSample {as} stab s₁ s₂ t Heq ch₁ ch₂
... | eq = eq , lem-EqSample⇒ChangelessSV⇒GEqSample {as} stab s₁ s₂ t eq (snd ch₁) (snd ch₂)

------------------------------------------------------------------------------

lem-AlwaysEqAt : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always (H (EqAt {as} s₁ s₂)  (EqAt {as} s₁ s₂)  G (EqAt {as} s₁ s₂)   _  Always (EqAt {as} s₁ s₂)))
lem-AlwaysEqAt {as} s₁ s₂ = lem-AlwaysEq (at as s₁) (at as s₂)

------------------------------------------------------------------------------

lemC-AlwaysEqRep⇒C⇒C : {A : Set}  (s₁ s₂ : SigVec (C A))  Always (EqRep {C A} s₁ s₂)  Always (ChangelessSV {C A} s₁  ChangelessSV {C A} s₂)
lemC-AlwaysEqRep⇒C⇒C s₁ s₂ eqA t₀ ch t₃ lt t₁ t₂ (p₁ , p₂) (q₁ , q₂) = trans2 (sym (eqA t₁)) (ch t₃ lt t₁ t₂ (p₁ , p₂) (q₁ , q₂)) (eqA t₂)

lemE-AlwaysEqRep⇒C⇒C : {A : Set} (s₁ s₂ : SigVec (E A))  Always (EqRep {E A} s₁ s₂)  Always (ChangelessSV {E A} s₁  ChangelessSV {E A} s₂)
lemE-AlwaysEqRep⇒C⇒C (ma₁ , cp₁) (ma₂ , cp₂) eq t₀ ch t₂ lt₁ with ×-inj2' eq
... | _ , eqcp = λ _  trans2 (sym (eqcp t₀)) (ch t₂ lt₁ lt₁) (eqcp t₂)

lemS-AlwaysEqRep⇒C⇒C : {A : Set} (s₁ s₂ : SigVec (S A))  Always (EqRep {S A} s₁ s₂)  Always (ChangelessSV {S A} s₁  ChangelessSV {S A} s₂)
lemS-AlwaysEqRep⇒C⇒C (a₁ , cp₁) (a₂ , cp₂) eq t₀ ch t₂ lt₁ with ×-inj2' eq
... | _ , eqcp = λ _  trans2 (sym (eqcp t₀)) (ch t₂ lt₁ lt₁) (eqcp t₂)

lem-AlwaysEqRep⇒C⇒C : {as : SVDesc}  (s₁ s₂ : SigVec as)  Always (EqRep {as} s₁ s₂)  Always (ChangelessSV {as} s₁  ChangelessSV {as} s₂)
lem-AlwaysEqRep⇒C⇒C {C _} s₁ s₂ eq t un = lemC-AlwaysEqRep⇒C⇒C s₁ s₂ eq t un
lem-AlwaysEqRep⇒C⇒C {E _} s₁ s₂ eq t un = lemE-AlwaysEqRep⇒C⇒C s₁ s₂ eq t un
lem-AlwaysEqRep⇒C⇒C {S _} s₁ s₂ eq t un = lemS-AlwaysEqRep⇒C⇒C s₁ s₂ eq t un
lem-AlwaysEqRep⇒C⇒C {as , bs} (sa₁ , sb₁) (sa₂ , sb₂) eq t un with ×-split2' un | ×-inj2' eq
... | una , unb | eqa , eqb = lem-AlwaysEqRep⇒C⇒C {as} sa₁ sa₂ eqa t una &₂ lem-AlwaysEqRep⇒C⇒C {bs} sb₁ sb₂ eqb t unb

lem-AlwaysEqAt⇒C⇒C : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  Always (EqAt {as} s₁ s₂)  Always (ChangelessSV {as} s₁  ChangelessSV {as} s₂)
lem-AlwaysEqAt⇒C⇒C {as} stab s₁ s₂ eqAt = lem-AlwaysEqRep⇒C⇒C {as} s₁ s₂ (lem-AlwaysEqAt→AlwaysEqRep {as} stab s₁ s₂ eqAt)

------------------------------------------------------------------------------

lem-Eq0-ChangelessSVʳ : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  EqAt {as} s₁ s₂ O  ChangelessSVʳ {as} s₁ O  ChangelessSVʳ {as} s₂ O  Always (EqAt {as} s₁ s₂)
lem-Eq0-ChangelessSVʳ {as} stab s₁ s₂ eq ch₁ ch₂ t with lem-HEq⇒Cʳ⇒GʳEq {as} stab s₁ s₂ O  _ ()) ch₁ ch₂
lem-Eq0-ChangelessSVʳ stab s₁ s₂ eq ch₁ ch₂ O | eqAt , Geq = eq
lem-Eq0-ChangelessSVʳ stab s₁ s₂ eq ch₁ ch₂ (t >0) | eqAt , Geq = Geq (t >0) _

lemC-ChangelessSVʳ-Eq0 : {A : Set}  (s₁ s₂ : SigVec (C A))  (Unchanging {C A} s₁  Unchanging {C A} s₂  EqAt {C A} s₁ s₂) O
lemC-ChangelessSVʳ-Eq0 s₁ s₂ (t₀ , () , _) (t₁ , () , _)

lemE-ChangelessSVʳ-Eq0 : {A : Set}  (s₁ s₂ : SigVec (E A))  (Unchanging {E A} s₁  Unchanging {E A} s₂  EqAt {E A} s₁ s₂) O
lemE-ChangelessSVʳ-Eq0 (ma₁ , cp₁) (ma₂ , cp₂) un₁ un₂ = lem-isNothingEq un₁ un₂

lemS-ChangelessSVʳ-Eq0 : {A : Set}  (s₁ s₂ : SigVec (S A))  (Unchanging {S A} s₁  Unchanging {S A} s₂  EqAt {S A} s₁ s₂) O
lemS-ChangelessSVʳ-Eq0 (a₁ , cp₁) (a₂ , cp₂) () ()

lem-Unchanging0-Eq0 : {as : SVDesc}  (s₁ s₂ : SigVec as)  (Unchanging {as} s₁  Unchanging {as} s₂  EqAt {as} s₁ s₂) O
lem-Unchanging0-Eq0 {C _} s₁ s₂ un₁ un₂ = lemC-ChangelessSVʳ-Eq0 s₁ s₂ un₁ un₂
lem-Unchanging0-Eq0 {E _} s₁ s₂ un₁ un₂ = lemE-ChangelessSVʳ-Eq0 s₁ s₂ un₁ un₂
lem-Unchanging0-Eq0 {S _} s₁ s₂ un₁ un₂ = lemS-ChangelessSVʳ-Eq0 s₁ s₂ un₁ un₂
lem-Unchanging0-Eq0 {as , bs} (sa₁ , sb₁) (sa₂ , sb₂) (una₁ , unb₁) (una₂ , unb₂) = ×-cong (lem-Unchanging0-Eq0 {as} sa₁ sa₂ una₁ una₂)
                                                                                           (lem-Unchanging0-Eq0 {bs} sb₁ sb₂ unb₁ unb₂)

lem-ChangelessSVʳ-Eq0 : {as : SVDesc}  (s₁ s₂ : SigVec as)  (ChangelessSVʳ {as} s₁  ChangelessSVʳ {as} s₂  EqAt {as} s₁ s₂) O
lem-ChangelessSVʳ-Eq0 {as} s₁ s₂ (ch₁ , _) (ch₂ , _) = lem-Unchanging0-Eq0 {as} s₁ s₂ ch₁ ch₂

lem-ChangelessSVʳ-EqAlways : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  ChangelessSVʳ {as} s₁ O  ChangelessSVʳ {as} s₂ O  Always (EqAt {as} s₁ s₂)
lem-ChangelessSVʳ-EqAlways {as} stab s₁ s₂ ch₁ ch₂ = lem-Eq0-ChangelessSVʳ {as} stab s₁ s₂ (lem-ChangelessSVʳ-Eq0 {as} s₁ s₂ ch₁ ch₂) ch₁ ch₂

------------------------------------------------------------------------------

lem-ChangelessSVʳ-AlwaysEqRep : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  ChangelessSVʳ {as} s₁ O  ChangelessSVʳ {as} s₂ O  Always (EqRep {as} s₁ s₂)
lem-ChangelessSVʳ-AlwaysEqRep {as} stab s₁ s₂ ch₁ ch₂ = lem-EqH⇒Cʳ⇒Eq {as} stab s₁ s₂ O  _ ()) ch₁ ch₂


lemE-ChangelessSVʳ-rep-nothing : {A : Set}  Stability  (s : SigVec (E A))  (t : Time)  ChangelessSVʳ {E A} s O  rep {E A} s t  (nothing , [])
lemE-ChangelessSVʳ-rep-nothing stab (ma , cp) O      (isn , cp0) = ×-cong (lem-isNothing isn) (lemCP-O-empty cp (stab cp))
lemE-ChangelessSVʳ-rep-nothing stab (ma , cp) (t >0) (isn , cp0) = ×-cong (lem-isNothing isn) (trans (sym (cp0 (t >0) _ _)) (lemCP-O-empty cp (stab cp)))

lem-ChangelessSVʳ-EqRep : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  (t₁ t₂ : Time)  ChangelessSVʳ {as} s₁ O  ChangelessSVʳ {as} s₂ O  rep {as} s₁ t₁  rep {as} s₂ t₂
lem-ChangelessSVʳ-EqRep {C _} stab s₁ s₂ t₁ t₂ ((_ , () , _ ) , _) _
lem-ChangelessSVʳ-EqRep {E _} stab s₁ s₂ t₁ t₂ ch₁ ch₂ = trans (lemE-ChangelessSVʳ-rep-nothing stab s₁ t₁ ch₁) (sym (lemE-ChangelessSVʳ-rep-nothing stab s₂ t₂ ch₂))
lem-ChangelessSVʳ-EqRep {S _} stab s₁ s₂ t₁ t₂ (() , _) _
lem-ChangelessSVʳ-EqRep {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t₁ t₂ ((una₁ , unb₁) , unch₁) ((una₂ , unb₂) , unch₂) with ×-split2' unch₁ | ×-split2' unch₂
... | uncha₁ , unchb₁ | uncha₂ , unchb₂ = ×-cong (lem-ChangelessSVʳ-EqRep {as} stab sa₁ sa₂ t₁ t₂ (una₁ , uncha₁) (una₂ , uncha₂))
                                                 (lem-ChangelessSVʳ-EqRep {bs} stab sb₁ sb₂ t₁ t₂ (unb₁ , unchb₁) (unb₂ , unchb₂))

lemE-ChangelessSVʳ-sample-nothing : {A : Set}  Stability  (s : SigVec (E A))  (t : Time)  ChangelessSVʳ {E A} s O  sample {E A} s t  nothing
lemE-ChangelessSVʳ-sample-nothing stab (ma , cp) O (isn , cp0) = lem-isNothing isn
lemE-ChangelessSVʳ-sample-nothing stab (ma , cp) (t >0) (isn , cp0) with lemCP-O-empty cp (stab cp) | cp0 (t >0) _ _
... | eq1 | eq2 rewrite (trans (sym eq2) eq1) = refl

lem-ChangelessSVʳ-EqSample : {as : SVDesc}  Stability  (s₁ s₂ : SigVec as)  (t₁ t₂ : Time)  ChangelessSVʳ {as} s₁ O  ChangelessSVʳ {as} s₂ O  sample {as} s₁ t₁  sample {as} s₂ t₂
lem-ChangelessSVʳ-EqSample {C _} stab s₁ s₂ t₁ t₂ ((_ , () , _ ) , _) _
lem-ChangelessSVʳ-EqSample {E _} stab s₁ s₂ t₁ t₂ ch₁ ch₂ = trans (lemE-ChangelessSVʳ-sample-nothing stab s₁ t₁ ch₁) (sym (lemE-ChangelessSVʳ-sample-nothing stab s₂ t₂ ch₂))
lem-ChangelessSVʳ-EqSample {S _} stab s₁ s₂ t₁ t₂ (() , _) _
lem-ChangelessSVʳ-EqSample {as , bs} stab (sa₁ , sb₁) (sa₂ , sb₂) t₁ t₂ ((una₁ , unb₁) , unch₁) ((una₂ , unb₂) , unch₂) with ×-split2' unch₁ | ×-split2' unch₂
... | uncha₁ , unchb₁ | uncha₂ , unchb₂ = ×-cong (lem-ChangelessSVʳ-EqSample {as} stab sa₁ sa₂ t₁ t₂ (una₁ , uncha₁) (una₂ , uncha₂))
                                                 (lem-ChangelessSVʳ-EqSample {bs} stab sb₁ sb₂ t₁ t₂ (unb₁ , unchb₁) (unb₂ , unchb₂))

------------------------------------------------------------------------------

lemC-Heq-splice : {A : Set}  (s₁ s₂ s : SigVec (C A))  (t t' : Time)  H (EqRep {C A} s₁ s₂) t  spliceC s₁ s t t'  spliceC s₂ s t t'
lemC-Heq-splice s₁ s₂ s t t' Heq with compareGeq t' t
... | less p = Heq t' p
... | geq  p = refl

-- postulate lemCP-occ-takeExcl'  : {A : Set} → {ma₁ ma₂ : Maybe A} → (cp₁ cp₂ : ChangePrefix A) → (t : Time⁺) → H (occ (ma₁ , cp₁) ≐ occ (ma₂ , cp₂)) (t >0) → ma₁ ≡ ma₂ × takeExcl⁺ t (cp₁ (t >0)) ≡ takeExcl⁺ t (cp₂ (t >0))

-- lemCP-Heq-splice : {A : Set} → Extensionality → (cp₁ cp₂ cp : ChangePrefix A) → (t : Time⁺) → takeExcl⁺ t δas ++ (ℜ⁺₀⁺-minus t (sumℜ⁺ (map fst (takeExcl⁺ t (cp₁ (t >0)))))
--        (lemTDL-sumTakeExcl⁺ t (cp₁ (t >0)))
--        , ma)
--       ∷ cp (ℜ₀⁺₀-minus t' t ≤-trustme)

postulate lemE-Heq-splice : {A : Set}  Extensionality  (s₁ s₂ s : SigVec (E A))  (t : Time)  H (EqRep {E A} s₁ s₂) t  spliceE s₁ s t  spliceE s₂ s t
-- lemE-Heq-splice ext (ma₁ , cp₁) (ma₂ , cp₂) (ma , cp) t Heq = ×-cong (fst (×-inj (Heq O _))) (ext (λ t' → {!!}))

-- -- lemE-Heq-splice⁺ ext (ma₁ , cp₁) (ma₂ , cp₂) (ma , cp) t Heq with lemCP-occ-takeExcl' cp₁ cp₂ t Heq
-- -- lemE-Heq-splice⁺ ext (.ma₂ , cp₁) (ma₂ , cp₂) (ma , cp) t Heq | refl , eqcp = ×-congL (ext (λ s → cong2 _++_ eqcp (cong2R (delayTDLinit ma) (trans (ℜ⁺₀⁺-minus-proof-irrelevence {!!} {!!} {!!} {!!}) {!cong2 (ℜ⁺₀⁺-minus t) ? ?!}))))

-- --- with takeExcl⁺ t (cp₁ (t >0)) | takeExcl⁺ t (cp₂ (t >0))
-- --- lemE-Heq-splice⁺ (.ma₂ , cp₁) (ma₂ , cp₂) (ma , cp) t Heq | refl , eqcp | δas₁ | δas₂ = {!!}


postulate lemS-Heq-splice : {A : Set}  Extensionality  (s₁ s₂ s : SigVec (S A))  (t : Time)  H (EqRep {S A} s₁ s₂) t  spliceS s₁ s t  spliceS s₂ s t
-- lemS-Heq-splice ext (a₁ , cp₁) (a₂ , cp₂) (a , cp) O Heq = refl
-- lemS-Heq-splice ext (a₁ , cp₁) (a₂ , cp₂) (a , cp) (t >0) Heq with ×-inj3' Heq
-- ... | Heqa , Heqcp = ×-cong (Heqa O _) (ext (λ t' → {!!}))

lem-Heq-splice : {as : SVDesc}  Extensionality  (s₁ s₂ s : SigVec as)  (t : Time)  H (EqRep {as} s₁ s₂) t  splice {as} s₁ s t  splice {as} s₂ s t
lem-Heq-splice {C _} ext s₁ s₂ s t Heq = ext  t'  lemC-Heq-splice s₁ s₂ s t t' Heq)
lem-Heq-splice {E _} ext s₁ s₂ s t Heq = lemE-Heq-splice ext s₁ s₂ s t Heq
lem-Heq-splice {S _} ext s₁ s₂ s t Heq = lemS-Heq-splice ext s₁ s₂ s t Heq
lem-Heq-splice {as , bs} ext (sa₁ , sb₁) (sa₂ , sb₂) (sa , sb) t Heq with ×-inj3' Heq
... | Heqa , Heqb = ×-cong (lem-Heq-splice {as} ext sa₁ sa₂ sa t Heqa) (lem-Heq-splice {bs} ext sb₁ sb₂ sb t Heqb)

-- lem-HEqRep-splice : {as : SVDesc} → Extensionality → (s₁ s₂ s : SigVec as) →  Always (H (EqRep {as} s₁ s₂) ⇒ splice {as} s₁ s ≐ splice {as} s₂ s)
-- lem-HEqRep-splice {as} ext s₁ s₂ s O      Heq = refl
-- lem-HEqRep-splice {as} ext s₁ s₂ s (t >0) Heq = lem-Heq-splice⁺ {as} ext s₁ s₂ s t Heq

------------------------------------------------------------------------------

postulate lemE-sample-advance-plus : {A : Set}  (d t : Time)  (s : SigVec (E A))  sample {E A} (advance {E A} d s) t  sample {E A} s (t ₀+₀ d)
-- lemE-sample-advance-plus d      O      (ma , cp) = refl
-- lemE-sample-advance-plus O      (t >0) (ma , cp) = {!!}
-- lemE-sample-advance-plus (d >0) (t >0) (ma , cp) = {!!}

postulate lemS-sample-advance-plus : {A : Set}  Stability  (d t : Time)  (s : SigVec (S A))  sample {S A} (advance {S A} d s) t  sample {S A} s (t ₀+₀ d)
-- lemS-sample-advance-plus stab O      O      (a , cp) rewrite lemCP-O-empty cp (stab cp) = refl
-- lemS-sample-advance-plus stab (d >0) O      (a , cp) = {!!}
-- lemS-sample-advance-plus stab O      (t >0) (a , cp) rewrite lemCP-O-empty cp (stab cp) = {!!}
-- lemS-sample-advance-plus stab (d >0) (t >0) (a , cp) = {!!}

lem-sample-advance-plus : {as : SVDesc}  Stability  (d t : Time)  (s : SigVec as)  sample {as} (advance {as} d s) t  sample {as} s (t ₀+₀ d)
lem-sample-advance-plus {C _} stab d t s = refl