{-# OPTIONS --type-in-type #-}
open import NeilPrelude
open import List
open import ListProps
open import RealTime
open import Maybe
open import StrictTotalOrder
open import Logic
open import TimeDeltaList
module TimeDeltaListProps where
lemTDL-delay-inj⁺ : {A : Set} → {t : Time⁺} → Injective {TDList A} (delayTDL⁺ t)
lemTDL-delay-inj⁺ {A} {t} {[]} {[]} refl = refl
lemTDL-delay-inj⁺ {A} {t} {[]} {(_ , _) ∷ _} ()
lemTDL-delay-inj⁺ {A} {t} {(_ , _) ∷ _} {[]} ()
lemTDL-delay-inj⁺ {A} {t} {(δ₁ , a₁) ∷ δas₁} {(δ₂ , a₂) ∷ δas₂} eq with ∷-inj eq
lemTDL-delay-inj⁺ {A} {t} {(δ₁ , a₁) ∷ .δas₂} {(δ₂ , a₂) ∷ δas₂} eq | eq' , refl with ×-inj eq'
lemTDL-delay-inj⁺ {A} {t} {(δ₁ , .a₂) ∷ .δas₂} {(δ₂ , a₂) ∷ δas₂} eq | eq' , refl | eql , refl with ⁺+⁺-cancL eql
lemTDL-delay-inj⁺ {A} {t} {(.δ₂ , .a₂) ∷ .δas₂} {(δ₂ , a₂) ∷ δas₂} eq | _ , refl | _ , refl | refl = refl
lemTDL-delayEmpty : {A : Set} → {t : Time⁺} → (δas : TDList A) → delayTDL⁺ t δas ≡ [] → δas ≡ []
lemTDL-delayEmpty [] p = p
lemTDL-delayEmpty ((_ , _) ∷ _) ()
lemTDL-delayEmptyResp : {A : Set} → {t : Time⁺} → (δas : TDList A) → δas ≡ [] → delayTDL⁺ t δas ≡ []
lemTDL-delayEmptyResp .[] refl = refl
lemTDL-dropEmpty→takeAll : {A : Set} → (t : Time⁺) → (δas : TDList A) → dropIncl⁺ t δas ≡ [] → takeIncl⁺ t δas ≡ δas
lemTDL-dropEmpty→takeAll t [] p = refl
lemTDL-dropEmpty→takeAll t ((δ , a) ∷ δas) p with compareℜ⁺ δ t
lemTDL-dropEmpty→takeAll t ((.t , a) ∷ δas) p | refl = ∷-congL (sym (lemTDL-delayEmpty δas p))
lemTDL-dropEmpty→takeAll t ((δ , a) ∷ δas) p | less lt = ∷-congL (lemTDL-dropEmpty→takeAll ((t ⁺-⁺ δ) lt) δas (lemTDL-delayEmpty _ p))
lemTDL-dropEmpty→takeAll t ((δ , a) ∷ δas) () | more _
lemTDL-takeDropEmpty⁺ : {A : Set} → (t : Time⁺) → (δas : TDList A) → dropIncl⁺ t δas ≡ [] → takeIncl⁺ t δas ≡ [] → δas ≡ []
lemTDL-takeDropEmpty⁺ t δas p = trans (sym (lemTDL-dropEmpty→takeAll t δas p))
lemTDL-takeDropEmpty : {A : Set} → (t : Time) → (δas : TDList A) → dropIncl t δas ≡ [] → takeIncl t δas ≡ [] → δas ≡ []
lemTDL-takeDropEmpty O δas = const
lemTDL-takeDropEmpty (t >0) δas = lemTDL-takeDropEmpty⁺ t δas
lemTDL-takeDropEmptyAbsurd⁺ : {A : Set} → (t : Time⁺) → (δa : Δt × A) → (δas : TDList A) → dropIncl⁺ t (δa ∷ δas) ≡ [] → takeIncl⁺ t (δa ∷ δas) ≡ [] → False
lemTDL-takeDropEmptyAbsurd⁺ t δa δas deq teq with lemTDL-takeDropEmpty⁺ t (δa ∷ δas) deq teq
... | ()
lemTDL-safelastEqTakeAll : {A : Set} → (t : Time⁺) → (δa δa₀ : Δt × A) → (δas : TDList A) → dropIncl⁺ t (δa ∷ δas) ≡ [] → safelast δa δas ≡ safelast δa₀ (takeIncl⁺ t (δa ∷ δas))
lemTDL-safelastEqTakeAll t δa δa₀ δas p with lemTDL-dropEmpty→takeAll t (δa ∷ δas) p
... | q = cong (safelast δa₀) (sym q)
lemTDL-sndsafelastEqTakeAll : {A : Set} → (t : Time⁺) → (δa δa₀ : Δt × A) → (δas : TDList A) → dropIncl⁺ t (δa ∷ δas) ≡ [] → snd (safelast δa δas) ≡ snd (safelast δa₀ (takeIncl⁺ t (δa ∷ δas)))
lemTDL-sndsafelastEqTakeAll t δa δa₀ δas p = cong snd (lemTDL-safelastEqTakeAll t δa δa₀ δas p)
lemTDL-takeDropSafeLast⁺ : {A : Set} → (t : Time⁺) → (δa₁ δa₂ : Δt × A) → (δas₁ δas₂ : TDList A) →
dropIncl⁺ t (δa₂ ∷ δas₂) ≡ [] → δa₁ ∷ δas₁ ≡ takeIncl⁺ t (δa₂ ∷ δas₂) → snd (safelast δa₂ δas₂) ≡ snd (safelast δa₁ δas₁)
lemTDL-takeDropSafeLast⁺ t (d₁ , a₁) (d₂ , a₂) δas₁ δas₂ p q with compareℜ⁺ d₂ t
lemTDL-takeDropSafeLast⁺ t (.t , .a₂) (.t , a₂) .[] δas₂ p refl | refl with lemTDL-delayEmpty δas₂ p
lemTDL-takeDropSafeLast⁺ t (.t , .a₂) (.t , a₂) .[] .[] p refl | refl | refl = refl
lemTDL-takeDropSafeLast⁺ t (d₁ , a₁) (d₂ , a₂) δas₁ δas₂ () () | more _
lemTDL-takeDropSafeLast⁺ t (.d₂ , .a₂) (d₂ , a₂) .[] [] p refl | less _ = refl
lemTDL-takeDropSafeLast⁺ t (.d₂ , .a₂) (d₂ , a₂) ._ (δa₂ ∷ δas₂) p refl | less lt = lemTDL-sndsafelastEqTakeAll ((t ⁺-⁺ d₂) lt) δa₂ (d₂ , a₂) δas₂ (lemTDL-delayEmpty _ p)
lemTDL-takeDropSafeLast : {A : Set} → (t : Time) → (δa₁ δa₂ : Δt × A) → (δas₁ δas₂ : TDList A) →
dropIncl t (δa₂ ∷ δas₂) ≡ [] → δa₁ ∷ δas₁ ≡ takeIncl t (δa₂ ∷ δas₂) → snd (safelast δa₂ δas₂) ≡ snd (safelast δa₁ δas₁)
lemTDL-takeDropSafeLast O δa₁ δa₂ δas₁ δas₂ () ()
lemTDL-takeDropSafeLast (t >0) δa₁ δa₂ δas₁ δas₂ p q = lemTDL-takeDropSafeLast⁺ t δa₁ δa₂ δas₁ δas₂ p q
lemTDL-takeDropEqual⁺ : {A : Set} → (t : Time⁺) → (δas₁ δas₂ : TDList A) → takeIncl⁺ t δas₁ ≡ takeIncl⁺ t δas₂ → dropIncl⁺ t δas₁ ≡ dropIncl⁺ t δas₂ → δas₁ ≡ δas₂
lemTDL-takeDropEqual⁺ t [] [] teq deq = refl
lemTDL-takeDropEqual⁺ t [] (δa ∷ δas) teq deq = absurd (lemTDL-takeDropEmptyAbsurd⁺ t δa δas (sym deq) (sym teq))
lemTDL-takeDropEqual⁺ t (δa ∷ δas) [] teq deq = absurd (lemTDL-takeDropEmptyAbsurd⁺ t δa δas deq teq)
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((δ₂ , b) ∷ δbs) teq deq with compareℜ⁺ δ₁ t | compareℜ⁺ δ₂ t
lemTDL-takeDropEqual⁺ t ((.t , .b) ∷ δas) ((.t , b) ∷ δbs) refl deq | refl | refl = cong2L _∷_ (lemTDL-delay-inj⁺ deq)
lemTDL-takeDropEqual⁺ t ((.t , a) ∷ δas) ((δ₂ , b) ∷ δbs) () deq | refl | more q
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((δ₂ , b) ∷ δbs) () deq | less p | more q
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((.t , b) ∷ δbs) () deq | more p | refl
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((δ₂ , b) ∷ δbs) () deq | more p | less q
lemTDL-takeDropEqual⁺ t ((.δ₂ , .b) ∷ .δbs) ((δ₂ , b) ∷ δbs) refl refl | more p | more q = refl
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((.t , b) ∷ δbs) teq deq | less p | refl with ∷-inj teq
lemTDL-takeDropEqual⁺ t ((.t , a) ∷ δas) ((.t , .a) ∷ δbs) teq deq | less p | refl | refl , teq' = absurd (<ℜ⁺-irreflexive p)
lemTDL-takeDropEqual⁺ t ((.t , a) ∷ δas) ((δ₂ , b) ∷ δbs) teq deq | refl | less q with ∷-inj teq
lemTDL-takeDropEqual⁺ t ((.t , a) ∷ δas) ((.t , .a) ∷ δbs) teq deq | refl | less q | refl , teq' = absurd (<ℜ⁺-irreflexive q)
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((δ₂ , b) ∷ δbs) teq deq | less p | less q with ∷-inj teq
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((.δ₁ , .a) ∷ δbs) teq deq | less p | less q | refl , teq' with lemTDL-delay-inj⁺ deq
lemTDL-takeDropEqual⁺ t ((δ₁ , a) ∷ δas) ((.δ₁ , .a) ∷ δbs) teq deq | less p | less q | refl , teq' | deq' with ℜ⁺-minus t δ₁ p | ℜ⁺-minus t δ₁ q | lem-ℜ⁺-minus-proofirrelevence p q
... | t' | .t' | refl = cong2L _∷_ (lemTDL-takeDropEqual⁺ t' δas δbs teq' deq')
lemTDL-takeDropEqual : {A : Set} → (t : Time) → (δas₁ δas₂ : TDList A) → takeIncl t δas₁ ≡ takeIncl t δas₂ → dropIncl t δas₁ ≡ dropIncl t δas₂ → δas₁ ≡ δas₂
lemTDL-takeDropEqual O = λ _ _ _ → id
lemTDL-takeDropEqual (t >0) = lemTDL-takeDropEqual⁺ t
lemTDL-dropInclSum→Empty⁺ : {A : Set} → (t : Time⁺) → (δas : TDList A) → sumTDL δas ≤ℜ₀ (t >0) → dropIncl⁺ t δas ≡ []
lemTDL-dropInclSum→Empty⁺ t [] p = refl
lemTDL-dropInclSum→Empty⁺ t ((δ , a) ∷ δas) p with lem-ℜ⁺-leq p | compareℜ⁺ δ t
lemTDL-dropInclSum→Empty⁺ t ((.t , a) ∷ []) p | p' | refl = refl
lemTDL-dropInclSum→Empty⁺ t ((.t , a) ∷ δa ∷ δas) p | p' | refl = absurd (<≤ℜ⁺-asym lem-ℜ⁺-+-<-increasingR p')
lemTDL-dropInclSum→Empty⁺ t ((δ , a) ∷ δas) p | p' | more q = absurd (<≤ℜ⁺-asym (≤<ℜ⁺-trans p' q) (lem-ℜ⁺₀-⁺+-increasingR (sumℜ⁺ (map fst δas))))
lemTDL-dropInclSum→Empty⁺ t ((δ , a) ∷ δas) p | p' | less q = lemTDL-delayEmptyResp _ (lemTDL-dropInclSum→Empty⁺ ((t ⁺-⁺ δ) q) δas (lem-ℜ₀-x⁺+₀y≤z→y≤z-x q p') )
lemTDL-dropInclSum→Empty : {A : Set} → (t : Time) → (δas : TDList A) → sumTDL δas ≤ℜ₀ t → dropIncl t δas ≡ []
lemTDL-dropInclSum→Empty (t >0) δas p = lemTDL-dropInclSum→Empty⁺ t δas p
lemTDL-dropInclSum→Empty O δas (inl ())
lemTDL-dropInclSum→Empty O [] (inr q) = refl
lemTDL-dropInclSum→Empty O (δa ∷ δas) (inr ())
lemTDL-lookupFirstDelta : {A : Set} → {a : A} → {δas : TDList A} → (δ : Δt) → lookupTDL⁺ ((δ , a) ∷ δas) δ ≡ just a
lemTDL-lookupFirstDelta δ with compareℜ⁺ δ δ
lemTDL-lookupFirstDelta δ | refl = refl
lemTDL-lookupFirstDelta δ | less p = absurd (<ℜ⁺-irreflexive p)
lemTDL-lookupFirstDelta δ | more p = absurd (<ℜ⁺-irreflexive p)
lemTDL-lookupFirstDelta2 : {A : Set} → {a : A} → {δas : TDList A} → (δ : Δt) → IsJust (lookupTDL⁺ ((δ , a) ∷ δas) δ)
lemTDL-lookupFirstDelta2 δ with compareℜ⁺ δ δ
lemTDL-lookupFirstDelta2 δ | refl = _
lemTDL-lookupFirstDelta2 δ | less p = absurd (<ℜ⁺-irreflexive p)
lemTDL-lookupFirstDelta2 δ | more p = absurd (<ℜ⁺-irreflexive p)
lemTDL-lookupDelay : {A : Set} → (δas : TDList A) → (d t : Time⁺) → (q : d <ℜ⁺ t)→ lookupTDL⁺ (delayTDL⁺ d δas) t ≡ lookupTDL⁺ δas ((t ⁺-⁺ d) q)
lemTDL-lookupDelay [] d t q = refl
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q with compareℜ⁺ (d ⁺+⁺ δ) t
lemTDL-lookupDelay ((δ , a) ∷ δas) d ._ q | refl = trans (sym (lemTDL-lookupFirstDelta δ))
(cong (lookupTDL⁺ ((δ , a) ∷ δas)) (sym (lem-ℜ⁺-[x+y]-x=y q)))
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | less r with compareℜ⁺ δ ((t ⁺-⁺ d) q)
lemTDL-lookupDelay ((._ , a) ∷ δas) d t q | less r | refl = absurd (<ℜ⁺-irreflexive (<ℜ⁺-substL (lem-ℜ⁺-x+[y-x]=y q) r))
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | less r | less s = cong (lookupTDL⁺ δas) (lem-ℜ⁺-x-[y+z]=[x-y]-z r q s)
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | less r | more s = absurd (<ℜ⁺-asym r (lem-ℜ⁺-x-y<z→x<y+z q s))
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | more r with compareℜ⁺ δ ((t ⁺-⁺ d) q)
lemTDL-lookupDelay ((._ , a) ∷ δas) d t q | more r | refl = absurd (<ℜ⁺-irreflexive (<ℜ⁺-substR (lem-ℜ⁺-x+[y-x]=y q) r))
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | more r | less s = absurd (<ℜ⁺-asym r (lem-ℜ⁺-y<z-x→x+y<z q s))
lemTDL-lookupDelay ((δ , a) ∷ δas) d t q | more _ | more _ = refl
lemTDL-lookupLessThanDelay : {A : Set} → (δas : TDList A) → (t₁ t₂ : Time⁺) → t₁ <ℜ⁺ t₂ → IsNothing (lookupTDL⁺ (delayTDL⁺ t₂ δas) t₁)
lemTDL-lookupLessThanDelay [] t₁ t₂ lt p = p
lemTDL-lookupLessThanDelay ((δ , a) ∷ δas) t₁ t₂ lt p with compareℜ⁺ (t₂ ⁺+⁺ δ) t₁
lemTDL-lookupLessThanDelay ((δ , a) ∷ δas) .(t₂ ⁺+⁺ δ) t₂ lt p | refl = <ℜ⁺-asym lt lem-ℜ⁺-+-<-increasingR
lemTDL-lookupLessThanDelay ((δ , a) ∷ δas) t₁ t₂ lt p | less q = <ℜ⁺-asym q (<ℜ⁺-trans lt lem-ℜ⁺-+-<-increasingR)
lemTDL-lookupLessThanDelay ((δ , a) ∷ δas) t₁ t₂ lt p | more q = p
lemTDL-lookupLessThenDelta2⁺ : {A : Set} → {a : A} → {δas : TDList A} → (t δ : Time⁺) → t <ℜ⁺ δ → IsNothing (lookupTDL⁺ ((δ , a) ∷ δas) t)
lemTDL-lookupLessThenDelta2⁺ t δ lt p with compareℜ⁺ δ t
lemTDL-lookupLessThenDelta2⁺ t .t lt p | refl = <ℜ⁺-irreflexive lt
lemTDL-lookupLessThenDelta2⁺ t δ lt p | less gt = <ℜ⁺-asym lt gt
lemTDL-lookupLessThenDelta2⁺ t δ lt p | more gt = p
lemTDL-lookupLessThenDelta⁺ : {A : Set} → {a : A} → {δas : TDList A} → (t δ : Time⁺) → t <ℜ⁺ δ → lookupTDL⁺ ((δ , a) ∷ δas) t ≡ nothing
lemTDL-lookupLessThenDelta⁺ {A} {a} {δas} t δ lt with lemTDL-lookupLessThenDelta2⁺ {A} {a} {δas} t δ lt
... | p with lookupTDL⁺ ((δ , a) ∷ δas) t
... | nothing = refl
... | just _ = magic p
lemTDL-lookupDelayed→Nothing : {A : Set} → (t : Time⁺) → (δas : TDList A) → IsNothing (lookupTDL⁺ (delayTDL⁺ t δas) t)
lemTDL-lookupDelayed→Nothing t [] p = p
lemTDL-lookupDelayed→Nothing t ((δ , a) ∷ δas) p = lemTDL-lookupLessThenDelta2⁺ t _ lem-ℜ⁺-+-<-increasingR p
lemTDL-lookupDropped→Nothing1 : {A : Set} → (t : Time⁺) → (δas : TDList A) → IsNothing (lookupTDL⁺ (dropIncl⁺ t δas) t)
lemTDL-lookupDropped→Nothing1 t [] ()
lemTDL-lookupDropped→Nothing1 t ((δ , a) ∷ δas) p with compareℜ⁺ δ t
lemTDL-lookupDropped→Nothing1 t ((.t , a) ∷ δas) p | refl = lemTDL-lookupDelayed→Nothing t δas p
lemTDL-lookupDropped→Nothing1 t ((δ , a) ∷ δas) p | more q = lemTDL-lookupLessThenDelta2⁺ t δ q p
lemTDL-lookupDropped→Nothing1 t ((δ , a) ∷ δas) p | less q = lemTDL-lookupDropped→Nothing1 ((t ⁺-⁺ δ) q) δas (subst (cong IsJust (lemTDL-lookupDelay (dropIncl⁺ ((t ⁺-⁺ δ) q) δas) δ t q)) p)
lemTDL-lookupDropped→Nothing2 : {A : Set} → (t₁ t₂ : Time⁺) → t₁ <ℜ⁺ t₂ → (δas : TDList A) → IsNothing (lookupTDL⁺ (dropIncl⁺ t₂ δas) t₁)
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt [] p = p
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((δ , a) ∷ δas) p with compareℜ⁺ δ t₂
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((.t₂ , a) ∷ δas) p | refl = lemTDL-lookupLessThanDelay δas t₁ t₂ lt p
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((δ , a) ∷ δas) p | more q = lemTDL-lookupLessThenDelta2⁺ t₁ δ (<ℜ⁺-trans lt q) p
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((δ , a) ∷ δas) p | less q with compareℜ⁺ δ t₁
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((.t₁ , a) ∷ δas) p | less q | refl = lemTDL-lookupDelayed→Nothing t₁ (dropIncl⁺ ((t₂ ⁺-⁺ t₁) q) δas) p
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((δ , a) ∷ δas) p | less q | less r = lemTDL-lookupDropped→Nothing2 ((t₁ ⁺-⁺ δ) r) ((t₂ ⁺-⁺ δ) q) (lem-ℜ⁺-minus-<-cancellative r q lt) δas (subst (cong IsJust (lemTDL-lookupDelay (dropIncl⁺ ((t₂ ⁺-⁺ δ) q) δas) δ t₁ r)) p)
lemTDL-lookupDropped→Nothing2 t₁ t₂ lt ((δ , a) ∷ δas) p | less q | more r = lemTDL-lookupLessThanDelay (dropIncl⁺ ((t₂ ⁺-⁺ δ) q) δas) t₁ δ r p
lemTDL-lookupDropped→Nothing : {A : Set} → (t₁ t₂ : Time⁺) → t₁ ≤ℜ⁺ t₂ → (δas : TDList A) → IsNothing (lookupTDL⁺ (dropIncl⁺ t₂ δas) t₁)
lemTDL-lookupDropped→Nothing t₁ t₂ (inl lt) = lemTDL-lookupDropped→Nothing2 t₁ t₂ lt
lemTDL-lookupDropped→Nothing t₁ .t₁ (inr refl) = lemTDL-lookupDropped→Nothing1 t₁
lemTDL-lookupTaken⁺ : {A : Set} → (t₁ t₂ : Time⁺) → t₁ ≤ℜ⁺ t₂ → (δas : TDList A) → lookupTDL⁺ (takeIncl⁺ t₂ δas) t₁ ≡ lookupTDL⁺ δas t₁
lemTDL-lookupTaken⁺ t₁ t₂ lt [] = refl
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) with compareℜ⁺ δ t₁ | compareℜ⁺ δ t₂
lemTDL-lookupTaken⁺ .t₂ t₂ lt ((.t₂ , a) ∷ δas) | refl | refl = lemTDL-lookupFirstDelta t₂
lemTDL-lookupTaken⁺ t₁ t₂ lt ((.t₁ , a) ∷ δas) | refl | less q = lemTDL-lookupFirstDelta t₁
lemTDL-lookupTaken⁺ t₁ t₂ lt ((.t₁ , a) ∷ δas) | refl | more q = absurd (<≤ℜ⁺-asym q lt)
lemTDL-lookupTaken⁺ t₁ t₂ lt ((.t₂ , a) ∷ δas) | more p | refl = lemTDL-lookupLessThenDelta⁺ t₁ t₂ p
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | more p | less q = lemTDL-lookupLessThenDelta⁺ t₁ δ p
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | more p | more q = refl
lemTDL-lookupTaken⁺ t₁ t₂ lt ((.t₂ , a) ∷ δas) | less p | refl = absurd (<≤ℜ⁺-asym p lt)
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | less p | more q = absurd (<ℜ⁺-asym p (≤<ℜ⁺-trans lt q))
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | less p | less q with compareℜ⁺ δ t₁
lemTDL-lookupTaken⁺ .δ t₂ lt ((δ , a) ∷ δas) | less p | less q | refl = absurd (<ℜ⁺-irreflexive p)
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | less p | less q | more r = absurd (<ℜ⁺-asym p r)
lemTDL-lookupTaken⁺ t₁ t₂ lt ((δ , a) ∷ δas) | less p | less q | less r = trans (cong (lookupTDL⁺ (takeIncl⁺ ((t₂ ⁺-⁺ δ) q) δas)) (lem-ℜ⁺-minus-proofirrelevence r p)) (lemTDL-lookupTaken⁺ ((t₁ ⁺-⁺ δ) p) ((t₂ ⁺-⁺ δ) q) (lem-ℜ⁺-minus-≤-cancellative p q lt) δas)
lemTDL-lookupTaken : {A : Set} → (t₁ t₂ : Time) → t₁ ≤ℜ₀ t₂ → (δas : TDList A) → lookupTDL (takeIncl t₂ δas) t₁ ≡ lookupTDL δas t₁
lemTDL-lookupTaken O t₂ lt δas = refl
lemTDL-lookupTaken (_ >0) O (inl ()) δas
lemTDL-lookupTaken (_ >0) O (inr ()) δas
lemTDL-lookupTaken (t₁ >0) (t₂ >0) lt δas = lemTDL-lookupTaken⁺ t₁ t₂ (lem-ℜ⁺-leq lt) δas
lemTDL-lookupBeyond⁺ : {A : Set} → (t : Time⁺) → (δas : TDList A) → sumTDL δas <ℜ₀ (t >0) → IsNothing (lookupTDL⁺ δas t)
lemTDL-lookupBeyond⁺ t [] _ ()
lemTDL-lookupBeyond⁺ t ((δ , a) ∷ δas) lt p with compareℜ⁺ δ t
lemTDL-lookupBeyond⁺ t ((.t , a) ∷ δas) lt p | refl = <≤ℜ⁺-asym lt (lem-ℜ⁺₀-⁺+-increasingR (sumTDL δas))
lemTDL-lookupBeyond⁺ t ((δ , a) ∷ δas) lt p | less q = lemTDL-lookupBeyond⁺ (ℜ⁺-minus t δ q) δas (lem-ℜ₀-x⁺+₀y<z→y<z-x q lt) p
lemTDL-lookupBeyond⁺ t ((δ , a) ∷ δas) lt () | more _
lemTDL-lookupBeyond : {A : Set} → (t : Time) → (δas : TDList A) → sumTDL δas <ℜ₀ t → IsNothing (lookupTDL δas t)
lemTDL-lookupBeyond O δas ()
lemTDL-lookupBeyond (t >0) δas lt = lemTDL-lookupBeyond⁺ t δas lt
lemTDL-sumExclLess : {A : Set} → (t : Time⁺) → (δas : TDList A) → sumTDL (takeExcl⁺ t δas) <ℜ₀ (t >0)
lemTDL-sumExclLess t [] = _
lemTDL-sumExclLess t ((δ , a) ∷ δas) with compareGeqℜ⁺ δ t
lemTDL-sumExclLess t ((δ , a) ∷ δas) | less p = lem-ℜ₀-y<z⁺-⁺x→x⁺+₀y<z p (lemTDL-sumExclLess ((t ⁺-⁺ δ) p) δas)
lemTDL-sumExclLess t ((δ , a) ∷ δas) | geq p = _