module Graded.Modality.Instances.Linear-or-affine where
import Tools.Algebra
open import Tools.Empty
open import Tools.Function
open import Tools.Level
open import Tools.Nat using (1+; Sequence)
open import Tools.Product
open import Tools.PropositionalEquality as PE
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Relation
open import Tools.Sum using (_β_; injβ; injβ)
import Graded.Modality
open import Graded.FullReduction.Assumptions
import Graded.Modality.Properties.Addition as Addition
import Graded.Modality.Properties.Greatest-lower-bound as GLB
import Graded.Modality.Properties.Meet as Meet
import Graded.Modality.Properties.Multiplication as Multiplication
import Graded.Modality.Properties.Natrec as Natrec
import Graded.Modality.Properties.PartialOrder as PartialOrder
import Graded.Modality.Properties.Star as Star
import Graded.Modality.Properties.Subtraction as Subtraction
open import Graded.Modality.Variant lzero
open import Definition.Typed.Restrictions
open import Graded.Usage.Restrictions
open import Definition.Untyped using (BMΞ£; π€; π¨)
private variable
variant : Modality-variant
trs : Type-restrictions _
urs : Usage-restrictions _
data Linear-or-affine : Set where
π π β€π β€Ο : Linear-or-affine
open Graded.Modality Linear-or-affine
open Tools.Algebra Linear-or-affine
private variable
n nβ nβ p q r s sβ sβ z zβ zβ : Linear-or-affine
infixr 43 _β§_
_β§_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π β§ π = π
π β§ π = π
β€Ο β§ _ = β€Ο
_ β§ β€Ο = β€Ο
_ β§ _ = β€π
infixr 40 _+_
_+_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π + q = q
p + π = p
_ + _ = β€Ο
infixr 45 _Β·_
_Β·_ : Linear-or-affine β Linear-or-affine β Linear-or-affine
π Β· _ = π
_ Β· π = π
π Β· q = q
p Β· π = p
β€π Β· β€π = β€π
_ Β· _ = β€Ο
infix 10 _β_
_β_ : Decidable (_β‘_ {A = Linear-or-affine})
π β π = yes refl
π β π = no (Ξ» ())
π β β€π = no (Ξ» ())
π β β€Ο = no (Ξ» ())
π β π = no (Ξ» ())
π β π = yes refl
π β β€π = no (Ξ» ())
π β β€Ο = no (Ξ» ())
β€π β π = no (Ξ» ())
β€π β π = no (Ξ» ())
β€π β β€π = yes refl
β€π β β€Ο = no (Ξ» ())
β€Ο β π = no (Ξ» ())
β€Ο β π = no (Ξ» ())
β€Ο β β€π = no (Ξ» ())
β€Ο β β€Ο = yes refl
infix 10 _β€_
_β€_ : Linear-or-affine β Linear-or-affine β Set
p β€ q = p β‘ p β§ q
β€Οβ€ : β p β β€Ο β€ p
β€Οβ€ _ = refl
π-maximal : π β€ p β p β‘ π
π-maximal {p = π} refl = refl
π-maximal {p = π} ()
π-maximal {p = β€π} ()
π-maximal {p = β€Ο} ()
π-maximal : π β€ p β p β‘ π
π-maximal {p = π} refl = refl
π-maximal {p = π} ()
π-maximal {p = β€π} ()
π-maximal {p = β€Ο} ()
opaque
β’πββ€π : p β’ π β p β€ π
β’πββ€π {(π)} πβ’π = β₯-elim (πβ’π refl)
β’πββ€π {(π)} _ = refl
β’πββ€π {(β€π)} _ = refl
β’πββ€π {(β€Ο)} _ = refl
+-zeroΛ‘ : LeftZero β€Ο _+_
+-zeroΛ‘ π = refl
+-zeroΛ‘ π = refl
+-zeroΛ‘ β€π = refl
+-zeroΛ‘ β€Ο = refl
+-zeroΚ³ : RightZero β€Ο _+_
+-zeroΚ³ π = refl
+-zeroΚ³ π = refl
+-zeroΚ³ β€π = refl
+-zeroΚ³ β€Ο = refl
+-zero : Zero β€Ο _+_
+-zero = +-zeroΛ‘ , +-zeroΚ³
β’π+β’π : p β’ π β q β’ π β p + q β‘ β€Ο
β’π+β’π {p = π} πβ’π _ = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = π} {q = π} _ _ = refl
β’π+β’π {p = π} {q = β€π} _ _ = refl
β’π+β’π {p = π} {q = β€Ο} _ _ = refl
β’π+β’π {p = β€π} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = β€π} {q = π} _ _ = refl
β’π+β’π {p = β€π} {q = β€π} _ _ = refl
β’π+β’π {p = β€π} {q = β€Ο} _ _ = refl
β’π+β’π {p = β€Ο} {q = π} _ πβ’π = β₯-elim (πβ’π refl)
β’π+β’π {p = β€Ο} {q = π} _ _ = refl
β’π+β’π {p = β€Ο} {q = β€π} _ _ = refl
β’π+β’π {p = β€Ο} {q = β€Ο} _ _ = refl
opaque
β€Ο+ : β p β β€Ο + p β‘ β€Ο
β€Ο+ π = refl
β€Ο+ π = refl
β€Ο+ β€π = refl
β€Ο+ β€Ο = refl
+β‘π : p + q β‘ π β p β‘ π Γ q β‘ π β p β‘ π Γ q β‘ π
+β‘π {p = π} {q = π} refl = injβ (refl , refl)
+β‘π {p = π} {q = π} refl = injβ (refl , refl)
+β‘π {p = π} {q = β€π} ()
+β‘π {p = π} {q = β€Ο} ()
+β‘π {p = π} {q = π} ()
+β‘π {p = π} {q = π} ()
+β‘π {p = π} {q = β€π} ()
+β‘π {p = π} {q = β€Ο} ()
+β‘π {p = β€π} {q = π} ()
+β‘π {p = β€π} {q = π} ()
+β‘π {p = β€π} {q = β€π} ()
+β‘π {p = β€π} {q = β€Ο} ()
+β‘π {p = β€Ο} {q = π} ()
+β‘π {p = β€Ο} {q = π} ()
+β‘π {p = β€Ο} {q = β€π} ()
+β‘π {p = β€Ο} {q = β€Ο} ()
β§β‘π : p β§ q β‘ π β p β‘ π Γ q β‘ π
β§β‘π {p = π} {q = π} _ = refl , refl
β§β‘π {p = π} {q = π} ()
β§β‘π {p = π} {q = β€π} ()
β§β‘π {p = π} {q = β€Ο} ()
β§β‘π {p = π} {q = π} ()
β§β‘π {p = π} {q = π} ()
β§β‘π {p = π} {q = β€π} ()
β§β‘π {p = π} {q = β€Ο} ()
β§β‘π {p = β€π} {q = π} ()
β§β‘π {p = β€π} {q = π} ()
β§β‘π {p = β€π} {q = β€π} ()
β§β‘π {p = β€π} {q = β€Ο} ()
β§β‘π {p = β€Ο} ()
opaque
πβ§pβ’π : β p β π β§ p β’ π
πβ§pβ’π π ()
πβ§pβ’π π ()
πβ§pβ’π β€π ()
πβ§pβ’π β€Ο ()
Β·-idempotent : Idempotent _Β·_
Β·-idempotent π = refl
Β·-idempotent π = refl
Β·-idempotent β€π = refl
Β·-idempotent β€Ο = refl
Β·-comm : Commutative _Β·_
Β·-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
β€ΟΒ·β’π : p β’ π β β€Ο Β· p β‘ β€Ο
β€ΟΒ·β’π {p = π} πβ’π = β₯-elim (πβ’π refl)
β€ΟΒ·β’π {p = π} _ = refl
β€ΟΒ·β’π {p = β€π} _ = refl
β€ΟΒ·β’π {p = β€Ο} _ = refl
opaque
β’πΒ·β€Ο : p β’ π β p Β· β€Ο β‘ β€Ο
β’πΒ·β€Ο {p} pβ’π = trans (Β·-comm p β€Ο) (β€ΟΒ·β’π pβ’π)
β€ΟΒ·β’π : β p β β€Ο Β· p β’ π
β€ΟΒ·β’π π ()
β€ΟΒ·β’π π ()
β€ΟΒ·β’π β€π ()
β€ΟΒ·β’π β€Ο ()
πΒ·β’π : p β’ π β π Β· p β’ π
πΒ·β’π {p = π} πβ’π = πβ’π
πΒ·β’π {p = π} _ = Ξ» ()
πΒ·β’π {p = β€π} _ = Ξ» ()
πΒ·β’π {p = β€Ο} _ = Ξ» ()
β€πΒ·β’π : p β’ π β β€π Β· p β’ π
β€πΒ·β’π {p = π} πβ’π = πβ’π
β€πΒ·β’π {p = π} _ = Ξ» ()
β€πΒ·β’π {p = β€π} _ = Ξ» ()
β€πΒ·β’π {p = β€Ο} _ = Ξ» ()
opaque
β€ΟΒ·+β€β€ΟΒ·Κ³ : β p β β€Ο Β· (p + q) β€ β€Ο Β· q
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€Ο} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€π} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€Ο} π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} β€π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} β€π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€π} β€π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€Ο} β€π = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} β€Ο = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = π} β€Ο = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€π} β€Ο = refl
β€ΟΒ·+β€β€ΟΒ·Κ³ {q = β€Ο} β€Ο = refl
opaque
β’πΒ·β’π : p β’ π β q β’ π β p Β· q β’ π
β’πΒ·β’π {p = π} pβ’π _ _ = pβ’π refl
β’πΒ·β’π {p = π} {q = π} _ qβ’π _ = qβ’π refl
β’πΒ·β’π {p = β€π} {q = π} _ qβ’π _ = qβ’π refl
β’πΒ·β’π {p = β€Ο} {q = π} _ qβ’π _ = qβ’π refl
β’πΒ·β’π {p = π} {q = π} _ _ ()
β’πΒ·β’π {p = π} {q = β€π} _ _ ()
β’πΒ·β’π {p = π} {q = β€Ο} _ _ ()
β’πΒ·β’π {p = β€π} {q = π} _ _ ()
β’πΒ·β’π {p = β€π} {q = β€π} _ _ ()
β’πΒ·β’π {p = β€π} {q = β€Ο} _ _ ()
β’πΒ·β’π {p = β€Ο} {q = π} _ _ ()
β’πΒ·β’π {p = β€Ο} {q = β€π} _ _ ()
β’πΒ·β’π {p = β€Ο} {q = β€Ο} _ _ ()
linear-or-affine-semiring-with-meet : Semiring-with-meet
linear-or-affine-semiring-with-meet = record
{ _+_ = _+_
; _Β·_ = _Β·_
; _β§_ = _β§_
; π = π
; π = π
; Ο = β€Ο
; Οβ€π = refl
; ΟΒ·+β€ΟΒ·Κ³ = Ξ» {p = p} β β€ΟΒ·+β€β€ΟΒ·Κ³ p
; is-π? = _β π
; +-Β·-Semiring = record
{ isSemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _+_
}
; assoc = +-assoc
}
; identity =
(Ξ» _ β refl)
, commβ§idΛ‘βidΚ³ +-comm (Ξ» _ β refl)
}
; comm = +-comm
}
; *-cong = congβ _Β·_
; *-assoc = Β·-assoc
; *-identity =
Β·-identityΛ‘
, commβ§idΛ‘βidΚ³ Β·-comm Β·-identityΛ‘
; distrib =
Β·-distribΛ‘-+
, commβ§distrΛ‘βdistrΚ³ Β·-comm Β·-distribΛ‘-+
}
; zero =
(Ξ» _ β refl)
, commβ§zeΛ‘βzeΚ³ Β·-comm (Ξ» _ β refl)
}
; β§-Semilattice = record
{ isBand = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; β-cong = congβ _β§_
}
; assoc = β§-assoc
}
; idem = Ξ» where
π β refl
π β refl
β€π β refl
β€Ο β refl
}
; comm = β§-comm
}
; Β·-distrib-β§ =
Β·-distribΛ‘-β§
, commβ§distrΛ‘βdistrΚ³ Β·-comm Β·-distribΛ‘-β§
; +-distrib-β§ =
+-distribΛ‘-β§
, commβ§distrΛ‘βdistrΚ³ +-comm +-distribΛ‘-β§
}
where
+-assoc : Associative _+_
+-assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-comm : Commutative _+_
+-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
Β·-assoc : Associative _Β·_
Β·-assoc = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
Β·-identityΛ‘ : LeftIdentity π _Β·_
Β·-identityΛ‘ = Ξ» where
π β refl
π β refl
β€π β refl
β€Ο β refl
Β·-distribΛ‘-+ : _Β·_ DistributesOverΛ‘ _+_
Β·-distribΛ‘-+ = Ξ» where
π _ _ β refl
π π _ β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π _ β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π _ β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β§-assoc : Associative _β§_
β§-assoc = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β§-comm : Commutative _β§_
β§-comm = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
Β·-distribΛ‘-β§ : _Β·_ DistributesOverΛ‘ _β§_
Β·-distribΛ‘-β§ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-distribΛ‘-β§ : _+_ DistributesOverΛ‘ _β§_
+-distribΛ‘-β§ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
instance
linear-or-affine-has-well-behaved-zero :
Has-well-behaved-zero linear-or-affine-semiring-with-meet
linear-or-affine-has-well-behaved-zero = record
{ non-trivial = Ξ» ()
; zero-product = Ξ» where
{p = π} _ β injβ refl
{q = π} _ β injβ refl
{p = π} {q = π} ()
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
{p = β€π} {q = π} ()
{p = β€π} {q = β€π} ()
{p = β€π} {q = β€Ο} ()
{p = β€Ο} {q = π} ()
{p = β€Ο} {q = β€π} ()
{p = β€Ο} {q = β€Ο} ()
; +-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
{p = π} {q = π} ()
{p = π} {q = π} ()
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
{p = β€π} {q = π} ()
{p = β€π} {q = π} ()
{p = β€π} {q = β€π} ()
{p = β€π} {q = β€Ο} ()
{p = β€Ο} {q = π} ()
{p = β€Ο} {q = π} ()
{p = β€Ο} {q = β€π} ()
{p = β€Ο} {q = β€Ο} ()
; β§-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
{p = π} {q = π} ()
{p = π} {q = π} ()
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
{p = β€π} {q = π} ()
{p = β€π} {q = π} ()
{p = β€π} {q = β€π} ()
{p = β€π} {q = β€Ο} ()
{p = β€Ο} ()
}
Star-requirements :
(Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine) β
Set
Star-requirements _β_β·_ =
(β {q r} β (β€Ο β q β· r) β‘ β€Ο) Γ
(β {p r} β (p β β€Ο β· r) β‘ β€Ο) Γ
(β {p q} β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· β€Ο) β‘ β€Ο) Γ
(β {r} β (π β π β· r) β‘ π) Γ
(β {p} β (p β π β· π) β‘ β€Ο) Γ
(β {p} β (p β π β· β€π) β‘ β€Ο) Γ
(β {p} β (p β β€π β· π) β‘ β€Ο) Γ
(β {p} β (p β β€π β· β€π) β‘ β€Ο) Γ
((π β π β· π) β€ β€π) Γ
((π β β€π β· π) β€ β€π) Γ
((π β π β· π) β€ β€π) Γ
((β€π β π β· π) β€ β€π) Γ
((π β π β· π) β€ π) Γ
((π β π β· β€π) β€ β€π) Γ
((β€π β π β· π) β€ β€π) Γ
((β€π β π β· β€π) β€ β€π) Γ
((π β π β· π) β€ π) Γ
((π β β€π β· π) β€ β€π) Γ
((β€π β π β· π) β€ β€π) Γ
((β€π β β€π β· π) β€ β€π)
Star-requirements-requiredβ² :
(M : Semiring-with-meet) β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet.π M β‘ π β
Semiring-with-meet._+_ M β‘ _+_ β
Semiring-with-meet._Β·_ M β‘ _Β·_ β
Semiring-with-meet._β§_ M β‘ _β§_ β
(_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine) β
(β p q r β (p β q β· r) β€ q + r Β· (p β q β· r)) β
(β p q r β (p β q β· r) β€ p) β
(β r β _Β·_ SubDistributesOverΚ³ (_β_β· r) by _β€_) β
Star-requirements _β_β·_
Star-requirements-requiredβ²
M@record{} refl refl refl refl refl star β-ineqβ β-ineqβ
Β·-sub-distribΚ³-β =
(Ξ» {_ _} β Οββ·)
, (Ξ» {_ _} β βΟβ·)
, (Ξ» {_ _} β ββ·Ο _ _)
, (Ξ» {r = r} β β€-antisym
(begin
π β π β· r β€β¨ β-ineqβ _ _ _ β©
π β)
(begin
π β‘Λβ¨ Β·-zeroΚ³ (π β π β· r) β©
π β π β· r Β· π β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
π β π β· r β))
, (Ξ» {p = p} β β€-antisym
(begin
p β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· p β π β· π ββ¨ β’π+β’π {p = π} (Ξ» ()) (πΒ·β’π βπβ·) β©
β€Ο β)
(β€Οβ€ (p β π β· π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β π β· β€π β€β¨ β-ineqβ _ _ _ β©
π + β€π Β· p β π β· β€π ββ¨ β’π+β’π {p = π} (Ξ» ()) (β€πΒ·β’π βπβ·) β©
β€Ο β)
(β€Οβ€ (p β π β· β€π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· p β β€π β· π ββ¨ β’π+β’π {p = β€π} (Ξ» ()) (πΒ·β’π ββ€πβ·) β©
β€Ο β)
(β€Οβ€ (p β β€π β· π)))
, (Ξ» {p = p} β β€-antisym
(begin
p β β€π β· β€π β€β¨ β-ineqβ _ _ _ β©
β€π + β€π Β· p β β€π β· β€π ββ¨ β’π+β’π {p = β€π} (Ξ» ()) (β€πΒ·β’π ββ€πβ·) β©
β€Ο β)
(β€Οβ€ (p β β€π β· β€π)))
, β§-greatest-lower-bound
(β-ineqβ _ _ _)
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
, (begin
π β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· π β β€π β· π β‘β¨β©
β€π β)
, β§-greatest-lower-bound
(begin
π β π β· π β€β¨ β-ineqβ _ _ _ β©
π + π Β· π β π β· π β‘β¨β©
π β)
(β-ineqβ _ _ _)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, (begin
π β π β· β€π β€β¨ β-ineqβ _ _ _ β©
β€π Β· π β π β· β€π β€β¨ Β·-monotoneΚ³ {r = β€π} (β-ineqβ _ _ _) β©
β€π Β· π β‘β¨β©
β€π β)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, β-ineqβ _ _ _
, (begin
π β β€π β· π β€β¨ β-ineqβ _ _ _ β©
β€π + π Β· π β β€π β· π β‘β¨β©
β€π β)
, β-ineqβ _ _ _
, β-ineqβ _ _ _
where
open Semiring-with-meet M using (Β·-zeroΚ³)
open PartialOrder M
open Meet M
open Multiplication M
open Tools.Reasoning.PartialOrder β€-poset
infix 50 _β_β·_
_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine
_β_β·_ = star
Οββ· : β€Ο β q β· r β‘ β€Ο
Οββ· {q = q} {r = r} = β€-antisym
(begin
β€Ο β q β· r β€β¨ β-ineqβ _ _ _ β©
β€Ο β)
(β€Οβ€ (β€Ο β q β· r))
βΟβ· : p β β€Ο β· r β‘ β€Ο
βΟβ· {p = p} {r = r} = β€-antisym
(begin
p β β€Ο β· r β€β¨ β-ineqβ _ _ _ β©
β€Ο + r Β· p β β€Ο β· r β‘β¨ +-zeroΛ‘ (r Β· _) β©
β€Ο β)
(β€Οβ€ (p β β€Ο β· r))
πββ· : π β q β· r β’ π
πββ· {q = q} {r = r} πββ·β‘π =
case begin
π β‘β¨β©
π Β· β€Ο β‘Λβ¨ cong (_Β· _) πββ·β‘π β©
π β q β· r Β· β€Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
β€Ο β q Β· β€Ο β· r β‘β¨ Οββ· β©
β€Ο β
of Ξ» ()
β€πββ· : β€π β q β· r β’ π
β€πββ· {q = q} {r = r} β€πββ·β‘π =
case begin
π β‘β¨β©
π Β· β€Ο β‘Λβ¨ cong (_Β· _) β€πββ·β‘π β©
β€π β q β· r Β· β€Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
β€Ο β q Β· β€Ο β· r β‘β¨ Οββ· β©
β€Ο β
of Ξ» ()
βπβ· : p β π β· r β’ π
βπβ· {p = p} {r = r} βπβ·β‘π =
case begin
π β‘β¨β©
π Β· β€Ο β‘Λβ¨ cong (_Β· _) βπβ·β‘π β©
p β π β· r Β· β€Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
(p Β· β€Ο) β β€Ο β· r β‘β¨ βΟβ· β©
β€Ο β
of Ξ» ()
ββ€πβ· : p β β€π β· r β’ π
ββ€πβ· {p = p} {r = r} ββ€πβ·β‘π =
case begin
π β‘β¨β©
π Β· β€Ο β‘Λβ¨ cong (_Β· _) ββ€πβ·β‘π β©
p β β€π β· r Β· β€Ο β€β¨ Β·-sub-distribΚ³-β _ _ _ _ β©
(p Β· β€Ο) β β€Ο β· r β‘β¨ βΟβ· β©
β€Ο β
of Ξ» ()
ββ·Ο : β p q β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· β€Ο) β‘ β€Ο
ββ·Ο _ β€Ο _ = βΟβ·
ββ·Ο β€Ο _ _ = Οββ·
ββ·Ο π π Β¬β‘πΓβ‘π = β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
ββ·Ο p π _ = β€-antisym
(begin
p β π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
π + β€Ο Β· p β π β· β€Ο β‘β¨ cong (π +_) (β€ΟΒ·β’π βπβ·) β©
π + β€Ο β‘β¨β©
β€Ο β)
(β€Οβ€ (p β π β· β€Ο))
ββ·Ο p β€π _ = β€-antisym
(begin
p β β€π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€π + β€Ο Β· p β β€π β· β€Ο β‘β¨ cong (β€π +_) (β€ΟΒ·β’π ββ€πβ·) β©
β€π + β€Ο β‘β¨β©
β€Ο β)
(β€Οβ€ (p β π β· β€Ο))
ββ·Ο π π _ = β€-antisym
(begin
π β π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€Ο Β· π β π β· β€Ο ββ¨ β€ΟΒ·β’π πββ· β©
β€Ο β)
(β€Οβ€ (π β π β· β€Ο))
ββ·Ο β€π π _ = β€-antisym
(begin
β€π β π β· β€Ο β€β¨ β-ineqβ _ _ _ β©
β€Ο Β· β€π β π β· β€Ο ββ¨ β€ΟΒ·β’π β€πββ· β©
β€Ο β)
(β€Οβ€ (β€π β π β· β€Ο))
Star-requirements-required :
(has-star : Has-star linear-or-affine-semiring-with-meet) β
Star-requirements (Has-star._β_β·_ has-star)
Star-requirements-required has-star =
Star-requirements-requiredβ²
linear-or-affine-semiring-with-meet refl refl refl refl refl
_β_β·_ β-ineqβ β-ineqβ Β·-sub-distribΚ³-β
where
open Has-star has-star
infix 50 _β_β·_
_β_β·_ :
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine
p β q β· π = p β§ q
p β q β· π = p + β€Ο Β· q
p β q β· β€π = p β§ β€Ο Β· q
p β q β· β€Ο = β€Ο Β· (p β§ q)
β€Οββ· : β r β β€Ο β q β· r β‘ β€Ο
β€Οββ· π = refl
β€Οββ· {q = π} π = refl
β€Οββ· {q = π} π = refl
β€Οββ· {q = β€π} π = refl
β€Οββ· {q = β€Ο} π = refl
β€Οββ· {q = π} β€π = refl
β€Οββ· {q = π} β€π = refl
β€Οββ· {q = β€π} β€π = refl
β€Οββ· {q = β€Ο} β€π = refl
β€Οββ· β€Ο = refl
ββ€Οβ· : β r β p β β€Ο β· r β‘ β€Ο
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = β€π} π = refl
ββ€Οβ· {p = β€Ο} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = π} π = refl
ββ€Οβ· {p = β€π} π = refl
ββ€Οβ· {p = β€Ο} π = refl
ββ€Οβ· {p = π} β€π = refl
ββ€Οβ· {p = π} β€π = refl
ββ€Οβ· {p = β€π} β€π = refl
ββ€Οβ· {p = β€Ο} β€π = refl
ββ€Οβ· {p = π} β€Ο = refl
ββ€Οβ· {p = π} β€Ο = refl
ββ€Οβ· {p = β€π} β€Ο = refl
ββ€Οβ· {p = β€Ο} β€Ο = refl
πβπβ· : β r β π β π β· r β‘ π
πβπβ· π = refl
πβπβ· π = refl
πβπβ· β€π = refl
πβπβ· β€Ο = refl
ββ·β€Ο : β p q β Β¬ (p β‘ π Γ q β‘ π) β (p β q β· β€Ο) β‘ β€Ο
ββ·β€Ο = Ξ» where
π π Β¬β‘πΓβ‘π β β₯-elim (Β¬β‘πΓβ‘π (refl , refl))
π π _ β refl
β€π π _ β refl
β€Ο π _ β refl
π π _ β refl
π π _ β refl
β€π π _ β refl
β€Ο π _ β refl
π β€π _ β refl
π β€π _ β refl
β€π β€π _ β refl
β€Ο β€π _ β refl
p β€Ο _ β ββ€Οβ· {p = p} β€Ο
βπβ·π : β p β p β π β· π β‘ β€Ο
βπβ·π π = refl
βπβ·π π = refl
βπβ·π β€π = refl
βπβ·π β€Ο = refl
βπβ·β€π : β p β p β π β· β€π β‘ β€Ο
βπβ·β€π π = refl
βπβ·β€π π = refl
βπβ·β€π β€π = refl
βπβ·β€π β€Ο = refl
ββ€πβ·π : β p β p β β€π β· π β‘ β€Ο
ββ€πβ·π π = refl
ββ€πβ·π π = refl
ββ€πβ·π β€π = refl
ββ€πβ·π β€Ο = refl
ββ€πβ·β€π : β p β p β β€π β· β€π β‘ β€Ο
ββ€πβ·β€π π = refl
ββ€πβ·β€π π = refl
ββ€πβ·β€π β€π = refl
ββ€πβ·β€π β€Ο = refl
β-greatest :
(has-star : Has-star linear-or-affine-semiring-with-meet) β
β p q r β Has-star._β_β·_ has-star p q r β€ p β q β· r
β-greatest has-star =
case Star-requirements-required has-star of
Ξ» (β€Οββ·β² , ββ€Οβ·β² , ββ·β²β€Ο , πβπβ·β² ,
βπβ·β²π , βπβ·β²β€π , ββ€πβ·β²π , ββ€πβ·β²β€π ,
πβπβ·β²π , πββ€πβ·β²π , πβπβ·β²π , β€πβπβ·β²π ,
πβπβ·β²π , πβπβ·β²β€π , β€πβπβ·β²π , β€πβπβ·β²β€π ,
πβπβ·β²π , πββ€πβ·β²π , β€πβπβ·β²π , β€πββ€πβ·β²π) β Ξ» where
β€Ο q r β begin
β€Ο β q β·β² r ββ¨ β€Οββ·β² β©
β€Ο βΛβ¨ β€Οββ· r β©
β€Ο β q β· r β
p β€Ο r β begin
p β β€Ο β·β² r ββ¨ ββ€Οβ·β² β©
β€Ο βΛβ¨ ββ€Οβ· r β©
p β β€Ο β· r β
π π r β begin
π β π β·β² r ββ¨ πβπβ·β² β©
π βΛβ¨ πβπβ· r β©
π β π β· r β
π π β€Ο β begin
π β π β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (_ , ()) }) β©
β€Ο βΛβ¨ ββ·β€Ο π π (Ξ» { (_ , ()) }) β©
π β π β· β€Ο β
π β€π β€Ο β begin
π β β€π β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (_ , ()) }) β©
β€Ο βΛβ¨ ββ·β€Ο π π (Ξ» { (_ , ()) }) β©
π β β€π β· β€Ο β
π q β€Ο β begin
π β q β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (() , _) }) β©
β€Ο βΛβ¨ ββ·β€Ο π q (Ξ» { (() , _) }) β©
π β q β· β€Ο β
β€π q β€Ο β begin
β€π β q β·β² β€Ο ββ¨ ββ·β²β€Ο (Ξ» { (() , _) }) β©
β€Ο βΛβ¨ ββ·β€Ο β€π q (Ξ» { (() , _) }) β©
β€π β q β· β€Ο β
p π π β begin
p β π β·β² π ββ¨ βπβ·β²π β©
β€Ο βΛβ¨ βπβ·π p β©
p β π β· π β
p β€π π β begin
p β β€π β·β² π ββ¨ ββ€πβ·β²π β©
β€Ο βΛβ¨ ββ€πβ·π p β©
p β β€π β· π β
p π β€π β begin
p β π β·β² β€π ββ¨ βπβ·β²β€π β©
β€Ο βΛβ¨ βπβ·β€π p β©
p β π β· β€π β
p β€π β€π β begin
p β β€π β·β² β€π ββ¨ ββ€πβ·β²β€π β©
β€Ο βΛβ¨ ββ€πβ·β€π p β©
p β β€π β· β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
β€π β
π β€π π β begin
π β β€π β·β² π β€β¨ πββ€πβ·β²π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
π π β€π β begin
π β π β·β² β€π β€β¨ πβπβ·β²β€π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
β€π π β€π β begin
β€π β π β·β² β€π β€β¨ β€πβπβ·β²β€π β©
β€π β
π π π β begin
π β π β·β² π β€β¨ πβπβ·β²π β©
π β
π β€π π β begin
π β β€π β·β² π β€β¨ πββ€πβ·β²π β©
β€π β
β€π π π β begin
β€π β π β·β² π β€β¨ β€πβπβ·β²π β©
β€π β
β€π β€π π β begin
β€π β β€π β·β² π β€β¨ β€πββ€πβ·β²π β©
β€π β
where
open Has-star has-star renaming (_β_β·_ to _β_β·β²_)
open PartialOrder linear-or-affine-semiring-with-meet
open Tools.Reasoning.PartialOrder β€-poset
linear-or-affine-has-star :
Has-star linear-or-affine-semiring-with-meet
linear-or-affine-has-star = record
{ _β_β·_ = _β_β·_
; β-ineq = β-ineqβ , β-ineqβ
; +-sub-interchangeable-β = +-sub-interchangeable-β
; Β·-sub-distribΚ³-β = Ξ» r _ _ _ β
β€-reflexive (Β·-distribΚ³-β r _ _ _)
; β-sub-distrib-β§ = Ξ» r β
(Ξ» _ _ _ β β€-reflexive (β-distribΛ‘-β§ r _ _ _))
, (Ξ» _ _ _ β β€-reflexive (β-distribΚ³-β§ r _ _ _))
}
where
semiring-with-meet = linear-or-affine-semiring-with-meet
open Semiring-with-meet semiring-with-meet
hiding (π; π; _+_; _Β·_; _β§_; _β€_)
open PartialOrder semiring-with-meet
open Addition semiring-with-meet
open Multiplication semiring-with-meet
β-ineqβ : β p q r β p β q β· r β€ q + r Β· p β q β· r
β-ineqβ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
β-ineqβ : β p q r β (p β q β· r) β€ p
β-ineqβ = Ξ» where
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π π π β refl
π π π β refl
π π β€π β refl
π π β€Ο β refl
π β€π π β refl
π β€π π β refl
π β€π β€π β refl
π β€π β€Ο β refl
π β€Ο π β refl
π β€Ο π β refl
π β€Ο β€π β refl
π β€Ο β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π π π β refl
β€π π π β refl
β€π π β€π β refl
β€π π β€Ο β refl
β€π β€π π β refl
β€π β€π π β refl
β€π β€π β€π β refl
β€π β€π β€Ο β refl
β€π β€Ο π β refl
β€π β€Ο π β refl
β€π β€Ο β€π β refl
β€π β€Ο β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο π π β refl
β€Ο π π β refl
β€Ο π β€π β refl
β€Ο π β€Ο β refl
β€Ο β€π π β refl
β€Ο β€π π β refl
β€Ο β€π β€π β refl
β€Ο β€π β€Ο β refl
β€Ο β€Ο π β refl
β€Ο β€Ο π β refl
β€Ο β€Ο β€π β refl
β€Ο β€Ο β€Ο β refl
+-sub-interchangeable-β : β r β _+_ SubInterchangeable (_β_β· r) by _β€_
+-sub-interchangeable-β = Ξ» where
π p q pβ² qβ² β begin
(p β§ q) + (pβ² β§ qβ²) β€β¨ +-sub-interchangeable-β§ p _ _ _ β©
(p + pβ²) β§ (q + qβ²) β
π p q pβ² qβ² β begin
(p + β€Ο Β· q) + (pβ² + β€Ο Β· qβ²) ββ¨ +-assoc p _ _ β©
p + (β€Ο Β· q + (pβ² + β€Ο Β· qβ²)) βΛβ¨ cong (p +_) (+-assoc (β€Ο Β· q) _ _) β©
p + ((β€Ο Β· q + pβ²) + β€Ο Β· qβ²) ββ¨ cong (Ξ» q β p + (q + _)) (+-comm _ pβ²) β©
p + ((pβ² + β€Ο Β· q) + β€Ο Β· qβ²) ββ¨ cong (p +_) (+-assoc pβ² _ _) β©
p + (pβ² + (β€Ο Β· q + β€Ο Β· qβ²)) βΛβ¨ +-assoc p _ _ β©
(p + pβ²) + (β€Ο Β· q + β€Ο Β· qβ²) βΛβ¨ cong ((p + _) +_) (Β·-distribΛ‘-+ β€Ο q _) β©
(p + pβ²) + β€Ο Β· (q + qβ²) β
β€π p q pβ² qβ² β begin
(p β§ β€Ο Β· q) + (pβ² β§ β€Ο Β· qβ²) β€β¨ +-sub-interchangeable-β§ p _ _ _ β©
(p + pβ²) β§ (β€Ο Β· q + β€Ο Β· qβ²) βΛβ¨ β§-congΛ‘ (Β·-distribΛ‘-+ β€Ο q _) β©
(p + pβ²) β§ β€Ο Β· (q + qβ²) β
β€Ο p q pβ² qβ² β begin
β€Ο Β· (p β§ q) + β€Ο Β· (pβ² β§ qβ²) βΛβ¨ Β·-distribΛ‘-+ β€Ο (p β§ _) _ β©
β€Ο Β· ((p β§ q) + (pβ² β§ qβ²)) β€β¨ Β·-monotoneΚ³ {r = β€Ο} (+-sub-interchangeable-β§ p _ _ _) β©
β€Ο Β· ((p + pβ²) β§ (q + qβ²)) β
where
open Tools.Reasoning.PartialOrder β€-poset
Β·-distribΚ³-β : β r β _Β·_ DistributesOverΚ³ (_β_β· r)
Β·-distribΚ³-β = Ξ» where
π q p pβ² β
(p β§ pβ²) Β· q β‘β¨ Β·-distribΚ³-β§ _ p _ β©
p Β· q β§ pβ² Β· q β
π q p pβ² β
(p + β€Ο Β· pβ²) Β· q β‘β¨ Β·-distribΚ³-+ _ p _ β©
p Β· q + (β€Ο Β· pβ²) Β· q β‘β¨ cong (p Β· _ +_) (Β·-assoc β€Ο pβ² _) β©
p Β· q + β€Ο Β· pβ² Β· q β
β€π q p pβ² β
(p β§ β€Ο Β· pβ²) Β· q β‘β¨ Β·-distribΚ³-β§ _ p _ β©
p Β· q β§ (β€Ο Β· pβ²) Β· q β‘β¨ β§-congΛ‘ (Β·-assoc β€Ο pβ² _) β©
p Β· q β§ β€Ο Β· pβ² Β· q β
β€Ο q p pβ² β
(β€Ο Β· (p β§ pβ²)) Β· q β‘β¨ Β·-assoc β€Ο (p β§ _) _ β©
β€Ο Β· (p β§ pβ²) Β· q β‘β¨ cong (β€Ο Β·_) (Β·-distribΚ³-β§ _ p _) β©
β€Ο Β· (p Β· q β§ pβ² Β· q) β
where
open Tools.Reasoning.PropositionalEquality
β-distribΛ‘-β§ : β r β (_β_β· r) DistributesOverΛ‘ _β§_
β-distribΛ‘-β§ = Ξ» where
π p _ _ β lemma p _ _
π p q qβ² β
p + β€Ο Β· (q β§ qβ²) β‘β¨ cong (p +_) (Β·-distribΛ‘-β§ β€Ο q _) β©
p + (β€Ο Β· q β§ β€Ο Β· qβ²) β‘β¨ +-distribΛ‘-β§ p _ _ β©
(p + β€Ο Β· q) β§ (p + β€Ο Β· qβ²) β
β€π p q qβ² β
p β§ β€Ο Β· (q β§ qβ²) β‘β¨ β§-congΛ‘ (Β·-distribΛ‘-β§ β€Ο q _) β©
p β§ (β€Ο Β· q β§ β€Ο Β· qβ²) β‘β¨ lemma p _ _ β©
(p β§ β€Ο Β· q) β§ (p β§ β€Ο Β· qβ²) β
β€Ο p q qβ² β
β€Ο Β· (p β§ q β§ qβ²) β‘β¨ cong (β€Ο Β·_) (lemma p _ _) β©
β€Ο Β· ((p β§ q) β§ (p β§ qβ²)) β‘β¨ Β·-distribΛ‘-β§ β€Ο (p β§ _) _ β©
β€Ο Β· (p β§ q) β§ β€Ο Β· (p β§ qβ²) β
where
open Tools.Reasoning.PropositionalEquality
lemma = Ξ» p q qβ² β
p β§ (q β§ qβ²) β‘Λβ¨ cong (_β§ _) (β§-idem p) β©
(p β§ p) β§ (q β§ qβ²) β‘β¨ β§-assoc p _ _ β©
p β§ (p β§ (q β§ qβ²)) β‘Λβ¨ cong (p β§_) (β§-assoc p _ _) β©
p β§ ((p β§ q) β§ qβ²) β‘β¨ cong (Ξ» q β p β§ (q β§ _)) (β§-comm p _) β©
p β§ ((q β§ p) β§ qβ²) β‘β¨ cong (p β§_) (β§-assoc q _ _) β©
p β§ (q β§ (p β§ qβ²)) β‘Λβ¨ β§-assoc p _ _ β©
(p β§ q) β§ (p β§ qβ²) β
β-distribΚ³-β§ : β r β (_β_β· r) DistributesOverΚ³ _β§_
β-distribΚ³-β§ = Ξ» where
π _ p _ β lemma _ p _
π q p pβ² β
(p β§ pβ²) + β€Ο Β· q β‘β¨ +-distribΚ³-β§ _ p _ β©
(p + β€Ο Β· q) β§ (pβ² + β€Ο Β· q) β
β€π q p pβ² β
(p β§ pβ²) β§ β€Ο Β· q β‘β¨ lemma _ _ _ β©
(p β§ β€Ο Β· q) β§ (pβ² β§ β€Ο Β· q) β
β€Ο q p pβ² β
β€Ο Β· ((p β§ pβ²) β§ q) β‘β¨ cong (β€Ο Β·_) (lemma _ p _) β©
β€Ο Β· ((p β§ q) β§ (pβ² β§ q)) β‘β¨ Β·-distribΛ‘-β§ β€Ο (p β§ _) _ β©
β€Ο Β· (p β§ q) β§ β€Ο Β· (pβ² β§ q) β
where
open Tools.Reasoning.PropositionalEquality
lemma = Ξ» q p pβ² β
(p β§ pβ²) β§ q β‘β¨ β§-comm _ q β©
q β§ (p β§ pβ²) β‘β¨ β-distribΛ‘-β§ π q _ _ β©
(q β§ p) β§ (q β§ pβ²) β‘β¨ congβ _β§_ (β§-comm q _) (β§-comm q _) β©
(p β§ q) β§ (pβ² β§ q) β
linear-or-affine : Modality-variant β Modality
linear-or-affine variant = record
{ variant = variant
; semiring-with-meet = linear-or-affine-semiring-with-meet
; π-well-behaved = Ξ» _ β linear-or-affine-has-well-behaved-zero
}
opaque
bad-linear-or-affine-has-nr : Has-nr linear-or-affine-semiring-with-meet
bad-linear-or-affine-has-nr =
Star.has-nr _ β¦ linear-or-affine-has-star β¦
nr :
Linear-or-affine β Linear-or-affine β
Linear-or-affine β Linear-or-affine β Linear-or-affine β
Linear-or-affine
nr p π z s n = ((π β§ p) Β· n + s) β§ (n + z)
nr p π z s n = (π + p) Β· n + β€Ο Β· s + z
nr p β€π z s n = (β€π + p) Β· n + β€Ο Β· s + β€π Β· z
nr _ β€Ο z s n = β€Ο Β· (n + s + z)
nr-π : β r β nr p r z s n β‘ π β (z β‘ π Γ s β‘ π Γ n β‘ π)
nr-π r =
lemmaβ _ r _ _ _
, Ξ» { (refl , refl , refl) β lemmaβ _ r }
where
lemmaβ : β p r z s n β nr p r z s n β‘ π β z β‘ π Γ s β‘ π Γ n β‘ π
lemmaβ = Ξ» where
π π π π π refl β refl , refl , refl
π π π π π refl β refl , refl , refl
β€π π π π π refl β refl , refl , refl
β€Ο π π π π refl β refl , refl , refl
π π π π π refl β refl , refl , refl
π π π π π refl β refl , refl , refl
β€π π π π π refl β refl , refl , refl
β€Ο π π π π refl β refl , refl , refl
π β€π π π π refl β refl , refl , refl
π β€π π π π refl β refl , refl , refl
β€π β€π π π π refl β refl , refl , refl
β€Ο β€π π π π refl β refl , refl , refl
_ β€Ο π π π refl β refl , refl , refl
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π β€π π ()
π π β€π β€π π ()
π π β€π β€π β€π ()
π π β€π β€π β€Ο ()
π π β€π β€Ο π ()
π π β€π β€Ο π ()
π π β€π β€Ο β€π ()
π π β€π β€Ο β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο β€π π ()
π π β€Ο β€π π ()
π π β€Ο β€π β€π ()
π π β€Ο β€π β€Ο ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο β€π ()
π π β€Ο β€Ο β€Ο ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π β€π π ()
π π β€π β€π π ()
π π β€π β€π β€π ()
π π β€π β€π β€Ο ()
π π β€π β€Ο π ()
π π β€π β€Ο π ()
π π β€π β€Ο β€π ()
π π β€π β€Ο β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο β€π π ()
π π β€Ο β€π π ()
π π β€Ο β€π β€π ()
π π β€Ο β€π β€Ο ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο β€π ()
π π β€Ο β€Ο β€Ο ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π β€π π ()
β€π π π β€π π ()
β€π π π β€π β€π ()
β€π π π β€π β€Ο ()
β€π π π β€Ο π ()
β€π π π β€Ο π ()
β€π π π β€Ο β€π ()
β€π π π β€Ο β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π β€π π ()
β€π π π β€π π ()
β€π π π β€π β€π ()
β€π π π β€π β€Ο ()
β€π π π β€Ο π ()
β€π π π β€Ο π ()
β€π π π β€Ο β€π ()
β€π π π β€Ο β€Ο ()
β€π π β€π π π ()
β€π π β€π π π ()
β€π π β€π π β€π ()
β€π π β€π π β€Ο ()
β€π π β€π π π ()
β€π π β€π π π ()
β€π π β€π π β€π ()
β€π π β€π π β€Ο ()
β€π π β€π β€π π ()
β€π π β€π β€π π ()
β€π π β€π β€π β€π ()
β€π π β€π β€π β€Ο ()
β€π π β€π β€Ο π ()
β€π π β€π β€Ο π ()
β€π π β€π β€Ο β€π ()
β€π π β€π β€Ο β€Ο ()
β€π π β€Ο π π ()
β€π π β€Ο π π ()
β€π π β€Ο π β€π ()
β€π π β€Ο π β€Ο ()
β€π π β€Ο π π ()
β€π π β€Ο π π ()
β€π π β€Ο π β€π ()
β€π π β€Ο π β€Ο ()
β€π π β€Ο β€π π ()
β€π π β€Ο β€π π ()
β€π π β€Ο β€π β€π ()
β€π π β€Ο β€π β€Ο ()
β€π π β€Ο β€Ο π ()
β€π π β€Ο β€Ο π ()
β€π π β€Ο β€Ο β€π ()
β€π π β€Ο β€Ο β€Ο ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π β€π π ()
β€Ο π π β€π π ()
β€Ο π π β€π β€π ()
β€Ο π π β€π β€Ο ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο β€π ()
β€Ο π π β€Ο β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π β€π π ()
β€Ο π π β€π π ()
β€Ο π π β€π β€π ()
β€Ο π π β€π β€Ο ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο β€π ()
β€Ο π π β€Ο β€Ο ()
β€Ο π β€π π π ()
β€Ο π β€π π π ()
β€Ο π β€π π β€π ()
β€Ο π β€π π β€Ο ()
β€Ο π β€π π π ()
β€Ο π β€π π π ()
β€Ο π β€π π β€π ()
β€Ο π β€π π β€Ο ()
β€Ο π β€π β€π π ()
β€Ο π β€π β€π π ()
β€Ο π β€π β€π β€π ()
β€Ο π β€π β€π β€Ο ()
β€Ο π β€π β€Ο π ()
β€Ο π β€π β€Ο π ()
β€Ο π β€π β€Ο β€π ()
β€Ο π β€π β€Ο β€Ο ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π β€π ()
β€Ο π β€Ο π β€Ο ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π β€π ()
β€Ο π β€Ο π β€Ο ()
β€Ο π β€Ο β€π π ()
β€Ο π β€Ο β€π π ()
β€Ο π β€Ο β€π β€π ()
β€Ο π β€Ο β€π β€Ο ()
β€Ο π β€Ο β€Ο π ()
β€Ο π β€Ο β€Ο π ()
β€Ο π β€Ο β€Ο β€π ()
β€Ο π β€Ο β€Ο β€Ο ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π β€π π ()
π π β€π β€π π ()
π π β€π β€π β€π ()
π π β€π β€π β€Ο ()
π π β€π β€Ο π ()
π π β€π β€Ο π ()
π π β€π β€Ο β€π ()
π π β€π β€Ο β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο β€π π ()
π π β€Ο β€π π ()
π π β€Ο β€π β€π ()
π π β€Ο β€π β€Ο ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο β€π ()
π π β€Ο β€Ο β€Ο ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π π π ()
π π π π π ()
π π π π β€π ()
π π π π β€Ο ()
π π π β€π π ()
π π π β€π π ()
π π π β€π β€π ()
π π π β€π β€Ο ()
π π π β€Ο π ()
π π π β€Ο π ()
π π π β€Ο β€π ()
π π π β€Ο β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π π π ()
π π β€π π π ()
π π β€π π β€π ()
π π β€π π β€Ο ()
π π β€π β€π π ()
π π β€π β€π π ()
π π β€π β€π β€π ()
π π β€π β€π β€Ο ()
π π β€π β€Ο π ()
π π β€π β€Ο π ()
π π β€π β€Ο β€π ()
π π β€π β€Ο β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο π π ()
π π β€Ο π π ()
π π β€Ο π β€π ()
π π β€Ο π β€Ο ()
π π β€Ο β€π π ()
π π β€Ο β€π π ()
π π β€Ο β€π β€π ()
π π β€Ο β€π β€Ο ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο π ()
π π β€Ο β€Ο β€π ()
π π β€Ο β€Ο β€Ο ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π β€π π ()
β€π π π β€π π ()
β€π π π β€π β€π ()
β€π π π β€π β€Ο ()
β€π π π β€Ο π ()
β€π π π β€Ο π ()
β€π π π β€Ο β€π ()
β€π π π β€Ο β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π π π ()
β€π π π π π ()
β€π π π π β€π ()
β€π π π π β€Ο ()
β€π π π β€π π ()
β€π π π β€π π ()
β€π π π β€π β€π ()
β€π π π β€π β€Ο ()
β€π π π β€Ο π ()
β€π π π β€Ο π ()
β€π π π β€Ο β€π ()
β€π π π β€Ο β€Ο ()
β€π π β€π π π ()
β€π π β€π π π ()
β€π π β€π π β€π ()
β€π π β€π π β€Ο ()
β€π π β€π π π ()
β€π π β€π π π ()
β€π π β€π π β€π ()
β€π π β€π π β€Ο ()
β€π π β€π β€π π ()
β€π π β€π β€π π ()
β€π π β€π β€π β€π ()
β€π π β€π β€π β€Ο ()
β€π π β€π β€Ο π ()
β€π π β€π β€Ο π ()
β€π π β€π β€Ο β€π ()
β€π π β€π β€Ο β€Ο ()
β€π π β€Ο π π ()
β€π π β€Ο π π ()
β€π π β€Ο π β€π ()
β€π π β€Ο π β€Ο ()
β€π π β€Ο π π ()
β€π π β€Ο π π ()
β€π π β€Ο π β€π ()
β€π π β€Ο π β€Ο ()
β€π π β€Ο β€π π ()
β€π π β€Ο β€π π ()
β€π π β€Ο β€π β€π ()
β€π π β€Ο β€π β€Ο ()
β€π π β€Ο β€Ο π ()
β€π π β€Ο β€Ο π ()
β€π π β€Ο β€Ο β€π ()
β€π π β€Ο β€Ο β€Ο ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π β€π π ()
β€Ο π π β€π π ()
β€Ο π π β€π β€π ()
β€Ο π π β€π β€Ο ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο β€π ()
β€Ο π π β€Ο β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π π π ()
β€Ο π π π π ()
β€Ο π π π β€π ()
β€Ο π π π β€Ο ()
β€Ο π π β€π π ()
β€Ο π π β€π π ()
β€Ο π π β€π β€π ()
β€Ο π π β€π β€Ο ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο π ()
β€Ο π π β€Ο β€π ()
β€Ο π π β€Ο β€Ο ()
β€Ο π β€π π π ()
β€Ο π β€π π π ()
β€Ο π β€π π β€π ()
β€Ο π β€π π β€Ο ()
β€Ο π β€π π π ()
β€Ο π β€π π π ()
β€Ο π β€π π β€π ()
β€Ο π β€π π β€Ο ()
β€Ο π β€π β€π π ()
β€Ο π β€π β€π π ()
β€Ο π β€π β€π β€π ()
β€Ο π β€π β€π β€Ο ()
β€Ο π β€π β€Ο π ()
β€Ο π β€π β€Ο π ()
β€Ο π β€π β€Ο β€π ()
β€Ο π β€π β€Ο β€Ο ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π β€π ()
β€Ο π β€Ο π β€Ο ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π π ()
β€Ο π β€Ο π β€π ()
β€Ο π β€Ο π β€Ο ()
β€Ο π β€Ο β€π π ()
β€Ο π β€Ο β€π π ()
β€Ο π β€Ο β€π β€π ()
β€Ο π β€Ο β€π β€Ο ()
β€Ο π β€Ο β€Ο π ()
β€Ο π β€Ο β€Ο π ()
β€Ο π β€Ο β€Ο β€π ()
β€Ο π β€Ο β€Ο β€Ο ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π β€π π ()
π β€π π β€π π ()
π β€π π β€π β€π ()
π β€π π β€π β€Ο ()
π β€π π β€Ο π ()
π β€π π β€Ο π ()
π β€π π β€Ο β€π ()
π β€π π β€Ο β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π β€π π ()
π β€π π β€π π ()
π β€π π β€π β€π ()
π β€π π β€π β€Ο ()
π β€π π β€Ο π ()
π β€π π β€Ο π ()
π β€π π β€Ο β€π ()
π β€π π β€Ο β€Ο ()
π β€π β€π π π ()
π β€π β€π π π ()
π β€π β€π π β€π ()
π β€π β€π π β€Ο ()
π β€π β€π π π ()
π β€π β€π π π ()
π β€π β€π π β€π ()
π β€π β€π π β€Ο ()
π β€π β€π β€π π ()
π β€π β€π β€π π ()
π β€π β€π β€π β€π ()
π β€π β€π β€π β€Ο ()
π β€π β€π β€Ο π ()
π β€π β€π β€Ο π ()
π β€π β€π β€Ο β€π ()
π β€π β€π β€Ο β€Ο ()
π β€π β€Ο π π ()
π β€π β€Ο π π ()
π β€π β€Ο π β€π ()
π β€π β€Ο π β€Ο ()
π β€π β€Ο π π ()
π β€π β€Ο π π ()
π β€π β€Ο π β€π ()
π β€π β€Ο π β€Ο ()
π β€π β€Ο β€π π ()
π β€π β€Ο β€π π ()
π β€π β€Ο β€π β€π ()
π β€π β€Ο β€π β€Ο ()
π β€π β€Ο β€Ο π ()
π β€π β€Ο β€Ο π ()
π β€π β€Ο β€Ο β€π ()
π β€π β€Ο β€Ο β€Ο ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π β€π π ()
π β€π π β€π π ()
π β€π π β€π β€π ()
π β€π π β€π β€Ο ()
π β€π π β€Ο π ()
π β€π π β€Ο π ()
π β€π π β€Ο β€π ()
π β€π π β€Ο β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π π π ()
π β€π π π π ()
π β€π π π β€π ()
π β€π π π β€Ο ()
π β€π π β€π π ()
π β€π π β€π π ()
π β€π π β€π β€π ()
π β€π π β€π β€Ο ()
π β€π π β€Ο π ()
π β€π π β€Ο π ()
π β€π π β€Ο β€π ()
π β€π π β€Ο β€Ο ()
π β€π β€π π π ()
π β€π β€π π π ()
π β€π β€π π β€π ()
π β€π β€π π β€Ο ()
π β€π β€π π π ()
π β€π β€π π π ()
π β€π β€π π β€π ()
π β€π β€π π β€Ο ()
π β€π β€π β€π π ()
π β€π β€π β€π π ()
π β€π β€π β€π β€π ()
π β€π β€π β€π β€Ο ()
π β€π β€π β€Ο π ()
π β€π β€π β€Ο π ()
π β€π β€π β€Ο β€π ()
π β€π β€π β€Ο β€Ο ()
π β€π β€Ο π π ()
π β€π β€Ο π π ()
π β€π β€Ο π β€π ()
π β€π β€Ο π β€Ο ()
π β€π β€Ο π π ()
π β€π β€Ο π π ()
π β€π β€Ο π β€π ()
π β€π β€Ο π β€Ο ()
π β€π β€Ο β€π π ()
π β€π β€Ο β€π π ()
π β€π β€Ο β€π β€π ()
π β€π β€Ο β€π β€Ο ()
π β€π β€Ο β€Ο π ()
π β€π β€Ο β€Ο π ()
π β€π β€Ο β€Ο β€π ()
π β€π β€Ο β€Ο β€Ο ()
β€π β€π π π π ()
β€π β€π π π β€π ()
β€π β€π π π β€Ο ()
β€π β€π π π π ()
β€π β€π π π π ()
β€π β€π π π β€π ()
β€π β€π π π β€Ο ()
β€π β€π π β€π π ()
β€π β€π π β€π π ()
β€π β€π π β€π β€π ()
β€π β€π π β€π β€Ο ()
β€π β€π π β€Ο π ()
β€π β€π π β€Ο π ()
β€π β€π π β€Ο β€π ()
β€π β€π π β€Ο β€Ο ()
β€π β€π π π π ()
β€π β€π π π π ()
β€π β€π π π β€π ()
β€π β€π π π β€Ο ()
β€π β€π π π π ()
β€π β€π π π π ()
β€π β€π π π β€π ()
β€π β€π π π β€Ο ()
β€π β€π π β€π π ()
β€π β€π π β€π π ()
β€π β€π π β€π β€π ()
β€π β€π π β€π β€Ο ()
β€π β€π π β€Ο π ()
β€π β€π π β€Ο π ()
β€π β€π π β€Ο β€π ()
β€π β€π π β€Ο β€Ο ()
β€π β€π β€π π π ()
β€π β€π β€π π π ()
β€π β€π β€π π β€π ()
β€π β€π β€π π β€Ο ()
β€π β€π β€π π π ()
β€π β€π β€π π π ()
β€π β€π β€π π β€π ()
β€π β€π β€π π β€Ο ()
β€π β€π β€π β€π π ()
β€π β€π β€π β€π π ()
β€π β€π β€π β€π β€π ()
β€π β€π β€π β€π β€Ο ()
β€π β€π β€π β€Ο π ()
β€π β€π β€π β€Ο π ()
β€π β€π β€π β€Ο β€π ()
β€π β€π β€π β€Ο β€Ο ()
β€π β€π β€Ο π π ()
β€π β€π β€Ο π π ()
β€π β€π β€Ο π β€π ()
β€π β€π β€Ο π β€Ο ()
β€π β€π β€Ο π π ()
β€π β€π β€Ο π π ()
β€π β€π β€Ο π β€π ()
β€π β€π β€Ο π β€Ο ()
β€π β€π β€Ο β€π π ()
β€π β€π β€Ο β€π π ()
β€π β€π β€Ο β€π β€π ()
β€π β€π β€Ο β€π β€Ο ()
β€π β€π β€Ο β€Ο π ()
β€π β€π β€Ο β€Ο π ()
β€π β€π β€Ο β€Ο β€π ()
β€π β€π β€Ο β€Ο β€Ο ()
β€Ο β€π π π π ()
β€Ο β€π π π β€π ()
β€Ο β€π π π β€Ο ()
β€Ο β€π π π π ()
β€Ο β€π π π π ()
β€Ο β€π π π β€π ()
β€Ο β€π π π β€Ο ()
β€Ο β€π π β€π π ()
β€Ο β€π π β€π π ()
β€Ο β€π π β€π β€π ()
β€Ο β€π π β€π β€Ο ()
β€Ο β€π π β€Ο π ()
β€Ο β€π π β€Ο π ()
β€Ο β€π π β€Ο β€π ()
β€Ο β€π π β€Ο β€Ο ()
β€Ο β€π π π π ()
β€Ο β€π π π π ()
β€Ο β€π π π β€π ()
β€Ο β€π π π β€Ο ()
β€Ο β€π π π π ()
β€Ο β€π π π π ()
β€Ο β€π π π β€π ()
β€Ο β€π π π β€Ο ()
β€Ο β€π π β€π π ()
β€Ο β€π π β€π π ()
β€Ο β€π π β€π β€π ()
β€Ο β€π π β€π β€Ο ()
β€Ο β€π π β€Ο π ()
β€Ο β€π π β€Ο π ()
β€Ο β€π π β€Ο β€π ()
β€Ο β€π π β€Ο β€Ο ()
β€Ο β€π β€π π π ()
β€Ο β€π β€π π π ()
β€Ο β€π β€π π β€π ()
β€Ο β€π β€π π β€Ο ()
β€Ο β€π β€π π π ()
β€Ο β€π β€π π π ()
β€Ο β€π β€π π β€π ()
β€Ο β€π β€π π β€Ο ()
β€Ο β€π β€π β€π π ()
β€Ο β€π β€π β€π π ()
β€Ο β€π β€π β€π β€π ()
β€Ο β€π β€π β€π β€Ο ()
β€Ο β€π β€π β€Ο π ()
β€Ο β€π β€π β€Ο π ()
β€Ο β€π β€π β€Ο β€π ()
β€Ο β€π β€π β€Ο β€Ο ()
β€Ο β€π β€Ο π π ()
β€Ο β€π β€Ο π π ()
β€Ο β€π β€Ο π β€π ()
β€Ο β€π β€Ο π β€Ο ()
β€Ο β€π β€Ο π π ()
β€Ο β€π β€Ο π π ()
β€Ο β€π β€Ο π β€π ()
β€Ο β€π β€Ο π β€Ο ()
β€Ο β€π β€Ο β€π π ()
β€Ο β€π β€Ο β€π π ()
β€Ο β€π β€Ο β€π β€π ()
β€Ο β€π β€Ο β€π β€Ο ()
β€Ο β€π β€Ο β€Ο π ()
β€Ο β€π β€Ο β€Ο π ()
β€Ο β€π β€Ο β€Ο β€π ()
β€Ο β€π β€Ο β€Ο β€Ο ()
_ β€Ο π π π ()
_ β€Ο π π β€π ()
_ β€Ο π π β€Ο ()
_ β€Ο π π π ()
_ β€Ο π π π ()
_ β€Ο π π β€π ()
_ β€Ο π π β€Ο ()
_ β€Ο π β€π π ()
_ β€Ο π β€π π ()
_ β€Ο π β€π β€π ()
_ β€Ο π β€π β€Ο ()
_ β€Ο π β€Ο π ()
_ β€Ο π β€Ο π ()
_ β€Ο π β€Ο β€π ()
_ β€Ο π β€Ο β€Ο ()
_ β€Ο π π π ()
_ β€Ο π π π ()
_ β€Ο π π β€π ()
_ β€Ο π π β€Ο ()
_ β€Ο π π π ()
_ β€Ο π π π ()
_ β€Ο π π β€π ()
_ β€Ο π π β€Ο ()
_ β€Ο π β€π π ()
_ β€Ο π β€π π ()
_ β€Ο π β€π β€π ()
_ β€Ο π β€π β€Ο ()
_ β€Ο π β€Ο π ()
_ β€Ο π β€Ο π ()
_ β€Ο π β€Ο β€π ()
_ β€Ο π β€Ο β€Ο ()
_ β€Ο β€π π π ()
_ β€Ο β€π π π ()
_ β€Ο β€π π β€π ()
_ β€Ο β€π π β€Ο ()
_ β€Ο β€π π π ()
_ β€Ο β€π π π ()
_ β€Ο β€π π β€π ()
_ β€Ο β€π π β€Ο ()
_ β€Ο β€π β€π π ()
_ β€Ο β€π β€π π ()
_ β€Ο β€π β€π β€π ()
_ β€Ο β€π β€π β€Ο ()
_ β€Ο β€π β€Ο π ()
_ β€Ο β€π β€Ο π ()
_ β€Ο β€π β€Ο β€π ()
_ β€Ο β€π β€Ο β€Ο ()
_ β€Ο β€Ο π π ()
_ β€Ο β€Ο π π ()
_ β€Ο β€Ο π β€π ()
_ β€Ο β€Ο π β€Ο ()
_ β€Ο β€Ο π π ()
_ β€Ο β€Ο π π ()
_ β€Ο β€Ο π β€π ()
_ β€Ο β€Ο π β€Ο ()
_ β€Ο β€Ο β€π π ()
_ β€Ο β€Ο β€π π ()
_ β€Ο β€Ο β€π β€π ()
_ β€Ο β€Ο β€π β€Ο ()
_ β€Ο β€Ο β€Ο π ()
_ β€Ο β€Ο β€Ο π ()
_ β€Ο β€Ο β€Ο β€π ()
_ β€Ο β€Ο β€Ο β€Ο ()
lemmaβ : β p r β nr p r π π π β‘ π
lemmaβ = Ξ» where
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
π π β refl
π π β refl
π β€π β refl
π β€Ο β refl
β€π π β refl
β€π π β refl
β€π β€π β refl
β€π β€Ο β refl
β€Ο π β refl
β€Ο π β refl
β€Ο β€π β refl
β€Ο β€Ο β refl
linear-or-affine-has-nr : Has-nr linear-or-affine-semiring-with-meet
linear-or-affine-has-nr = record
{ nr = nr
; nr-monotone = Ξ» {p = p} {r = r} β nr-monotone p r
; nr-Β· = Ξ» {p = _} {r = r} β nr-Β· r
; nr-+ = Ξ» {p = _} {r = r} β nr-+ r
; nr-positive = Ξ» {p = _} {r = r} β nr-π r .projβ
; nr-zero = Ξ» {n = _} {p = _} {r = r} β nr-zero r _ _ _ _
; nr-suc = Ξ» {p = _} {r = r} β nr-suc r _ _ _ _
}
where
open Semiring-with-meet linear-or-affine-semiring-with-meet
hiding (π; π; _+_; _Β·_; _β§_; _β€_)
open Addition linear-or-affine-semiring-with-meet
open Meet linear-or-affine-semiring-with-meet
open Multiplication linear-or-affine-semiring-with-meet
open PartialOrder linear-or-affine-semiring-with-meet
nr-monotone :
β p r β
zβ β€ zβ β sβ β€ sβ β nβ β€ nβ β
nr p r zβ sβ nβ β€ nr p r zβ sβ nβ
nr-monotone = Ξ» where
p π zββ€zβ sββ€sβ nββ€nβ β
β§-monotone (+-monotone (Β·-monotoneΚ³ {r = π β§ p} nββ€nβ) sββ€sβ)
(+-monotone nββ€nβ zββ€zβ)
p π zββ€zβ sββ€sβ nββ€nβ β
+-monotone (Β·-monotoneΚ³ {r = π + p} nββ€nβ)
(+-monotone (Β·-monotoneΚ³ {r = β€Ο} sββ€sβ) zββ€zβ)
p β€π zββ€zβ sββ€sβ nββ€nβ β
+-monotone (Β·-monotoneΚ³ {r = β€π + p} nββ€nβ)
(+-monotone (Β·-monotoneΚ³ {r = β€Ο} sββ€sβ)
(Β·-monotoneΚ³ {r = β€π} zββ€zβ))
_ β€Ο zββ€zβ sββ€sβ nββ€nβ β
Β·-monotoneΚ³ {r = β€Ο} (+-monotone nββ€nβ (+-monotone sββ€sβ zββ€zβ))
nr-Β· : β r β nr p r z s n Β· q β€ nr p r (z Β· q) (s Β· q) (n Β· q)
nr-Β· {p = p} {z = z} {s = s} {n = n} {q = q} = Ξ» where
π β begin
(((π β§ p) Β· n + s) β§ (n + z)) Β· q β‘β¨ Β·-distribΚ³-β§ _ ((π β§ p) Β· _ + _) _ β©
((π β§ p) Β· n + s) Β· q β§ (n + z) Β· q β‘β¨ β§-cong (Β·-distribΚ³-+ _ ((π β§ p) Β· _) _)
(Β·-distribΚ³-+ _ n _) β©
(((π β§ p) Β· n) Β· q + s Β· q) β§ (n Β· q + z Β· q) β‘β¨ β§-congΚ³ (+-congΚ³ (Β·-assoc (π β§ p) _ _)) β©
((π β§ p) Β· (n Β· q) + s Β· q) β§ (n Β· q + z Β· q) β
π β begin
((π + p) Β· n + β€Ο Β· s + z) Β· q β‘β¨ Β·-distribΚ³-+ _ ((π + p) Β· _) _ β©
((π + p) Β· n) Β· q + (β€Ο Β· s + z) Β· q β‘β¨ +-congΛ‘ {x = ((π + p) Β· _) Β· _}
(Β·-distribΚ³-+ _ (β€Ο Β· s) _) β©
((π + p) Β· n) Β· q + (β€Ο Β· s) Β· q + z Β· q β‘β¨ +-cong (Β·-assoc (π + p) _ _)
(+-congΚ³ (Β·-assoc β€Ο s _)) β©
(π + p) Β· (n Β· q) + β€Ο Β· (s Β· q) + z Β· q β
β€π β begin
((β€π + p) Β· n + β€Ο Β· s + β€π Β· z) Β· q β‘β¨ Β·-distribΚ³-+ _ ((β€π + p) Β· _) _ β©
((β€π + p) Β· n) Β· q + (β€Ο Β· s + β€π Β· z) Β· q β‘β¨ +-congΛ‘ {x = ((β€π + p) Β· _) Β· _}
(Β·-distribΚ³-+ _ (β€Ο Β· s) _) β©
((β€π + p) Β· n) Β· q + (β€Ο Β· s) Β· q + (β€π Β· z) Β· q β‘β¨ +-cong (Β·-assoc (β€π + p) _ _)
(+-cong (Β·-assoc β€Ο s _) (Β·-assoc β€π z _)) β©
(β€π + p) Β· (n Β· q) + β€Ο Β· (s Β· q) + β€π Β· (z Β· q) β
β€Ο β begin
(β€Ο Β· (n + s + z)) Β· q β‘β¨ Β·-assoc β€Ο (n + _) _ β©
β€Ο Β· ((n + s + z) Β· q) β‘β¨ Β·-congΛ‘ {x = β€Ο} (Β·-distribΚ³-+ _ n _) β©
β€Ο Β· (n Β· q + (s + z) Β· q) β‘β¨ Β·-congΛ‘ {x = β€Ο} (+-congΛ‘ {x = n Β· _} (Β·-distribΚ³-+ _ s _)) β©
β€Ο Β· (n Β· q + s Β· q + z Β· q) β
where
open Tools.Reasoning.PartialOrder β€-poset
nr-+ :
β r β
nr p r zβ sβ nβ + nr p r zβ sβ nβ β€
nr p r (zβ + zβ) (sβ + sβ) (nβ + nβ)
nr-+
{p = p}
{zβ = zβ} {sβ = sβ} {nβ = nβ}
{zβ = zβ} {sβ = sβ} {nβ = nβ} = Ξ» where
π β begin
(((π β§ p) Β· nβ + sβ) β§ (nβ + zβ)) +
(((π β§ p) Β· nβ + sβ) β§ (nβ + zβ)) β€β¨ +-sub-interchangeable-β§ ((π β§ p) Β· _ + _) _ _ _ β©
(((π β§ p) Β· nβ + sβ) + ((π β§ p) Β· nβ + sβ)) β§
((nβ + zβ) + (nβ + zβ)) β‘β¨ β§-cong (+-sub-interchangeable-+ ((π β§ p) Β· _) _ _ _)
(+-sub-interchangeable-+ nβ _ _ _) β©
(((π β§ p) Β· nβ + (π β§ p) Β· nβ) + (sβ + sβ)) β§
((nβ + nβ) + (zβ + zβ)) β‘Λβ¨ β§-congΚ³ (+-congΚ³ (Β·-distribΛ‘-+ (π β§ p) _ _)) β©
((π β§ p) Β· (nβ + nβ) + (sβ + sβ)) β§ ((nβ + nβ) + (zβ + zβ)) β
π β begin
((π + p) Β· nβ + β€Ο Β· sβ + zβ) + ((π + p) Β· nβ + β€Ο Β· sβ + zβ) β‘β¨ +-sub-interchangeable-+ ((π + p) Β· _) _ _ _ β©
((π + p) Β· nβ + (π + p) Β· nβ) + (β€Ο Β· sβ + zβ) + (β€Ο Β· sβ + zβ) β‘β¨ +-cong (sym (Β·-distribΛ‘-+ (π + p) _ _))
(+-sub-interchangeable-+ (β€Ο Β· sβ) _ _ _) β©
(π + p) Β· (nβ + nβ) + (β€Ο Β· sβ + β€Ο Β· sβ) + (zβ + zβ) β‘Λβ¨ +-congΛ‘ {x = (π + p) Β· _}
(+-congΚ³ (Β·-distribΛ‘-+ β€Ο sβ _)) β©
(π + p) Β· (nβ + nβ) + β€Ο Β· (sβ + sβ) + (zβ + zβ) β
β€π β begin
((β€π + p) Β· nβ + β€Ο Β· sβ + β€π Β· zβ) +
((β€π + p) Β· nβ + β€Ο Β· sβ + β€π Β· zβ) β‘β¨ +-sub-interchangeable-+ ((β€π + p) Β· _) _ _ _ β©
((β€π + p) Β· nβ + (β€π + p) Β· nβ) +
(β€Ο Β· sβ + β€π Β· zβ) + (β€Ο Β· sβ + β€π Β· zβ) β‘β¨ +-cong (sym (Β·-distribΛ‘-+ (β€π + p) _ _))
(+-sub-interchangeable-+ (β€Ο Β· sβ) _ _ _) β©
(β€π + p) Β· (nβ + nβ) + (β€Ο Β· sβ + β€Ο Β· sβ) + (β€π Β· zβ + β€π Β· zβ) β‘Λβ¨ +-congΛ‘ {x = (β€π + p) Β· _}
(+-cong (Β·-distribΛ‘-+ β€Ο sβ _)
(Β·-distribΛ‘-+ β€π zβ _)) β©
(β€π + p) Β· (nβ + nβ) + β€Ο Β· (sβ + sβ) + β€π Β· (zβ + zβ) β
β€Ο β begin
β€Ο Β· (nβ + sβ + zβ) + β€Ο Β· (nβ + sβ + zβ) β‘Λβ¨ Β·-distribΛ‘-+ β€Ο (nβ + _) _ β©
β€Ο Β· ((nβ + sβ + zβ) + (nβ + sβ + zβ)) β‘β¨ Β·-congΛ‘ {x = β€Ο} lemma β©
β€Ο Β· ((nβ + nβ) + (sβ + sβ) + (zβ + zβ)) β
where
lemma =
(nβ + sβ + zβ) + (nβ + sβ + zβ) β‘β¨ +-sub-interchangeable-+ nβ _ _ _ β©
(nβ + nβ) + (sβ + zβ) + (sβ + zβ) β‘β¨ +-congΛ‘ {x = nβ + _}
(+-sub-interchangeable-+ sβ _ _ _) β©
(nβ + nβ) + (sβ + sβ) + (zβ + zβ) β
where
open Tools.Reasoning.PropositionalEquality
open Tools.Reasoning.PartialOrder β€-poset
nr-zero : β r p z s n β n β€ π β nr p r z s n β€ z
nr-zero = Ξ» where
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π β€π π refl β refl
π π β€π β€π β€π refl β refl
π π β€π β€π β€Ο refl β refl
π π β€π β€Ο π refl β refl
π π β€π β€Ο β€π refl β refl
π π β€π β€Ο β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο β€π π refl β refl
π π β€Ο β€π β€π refl β refl
π π β€Ο β€π β€Ο refl β refl
π π β€Ο β€Ο π refl β refl
π π β€Ο β€Ο β€π refl β refl
π π β€Ο β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π β€π π refl β refl
π π β€π β€π β€π refl β refl
π π β€π β€π β€Ο refl β refl
π π β€π β€Ο π refl β refl
π π β€π β€Ο β€π refl β refl
π π β€π β€Ο β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο β€π π refl β refl
π π β€Ο β€π β€π refl β refl
π π β€Ο β€π β€Ο refl β refl
π π β€Ο β€Ο π refl β refl
π π β€Ο β€Ο β€π refl β refl
π π β€Ο β€Ο β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π β€π π refl β refl
π β€π π β€π β€π refl β refl
π β€π π β€π β€Ο refl β refl
π β€π π β€Ο π refl β refl
π β€π π β€Ο β€π refl β refl
π β€π π β€Ο β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π β€π π refl β refl
π β€π π β€π β€π refl β refl
π β€π π β€π β€Ο refl β refl
π β€π π β€Ο π refl β refl
π β€π π β€Ο β€π refl β refl
π β€π π β€Ο β€Ο refl β refl
π β€π β€π π π refl β refl
π β€π β€π π β€π refl β refl
π β€π β€π π β€Ο refl β refl
π β€π β€π π π refl β refl
π β€π β€π π β€π refl β refl
π β€π β€π π β€Ο refl β refl
π β€π β€π β€π π refl β refl
π β€π β€π β€π β€π refl β refl
π β€π β€π β€π β€Ο refl β refl
π β€π β€π β€Ο π refl β refl
π β€π β€π β€Ο β€π refl β refl
π β€π β€π β€Ο β€Ο refl β refl
π β€π β€Ο π π refl β refl
π β€π β€Ο π β€π refl β refl
π β€π β€Ο π β€Ο refl β refl
π β€π β€Ο π π refl β refl
π β€π β€Ο π β€π refl β refl
π β€π β€Ο π β€Ο refl β refl
π β€π β€Ο β€π π refl β refl
π β€π β€Ο β€π β€π refl β refl
π β€π β€Ο β€π β€Ο refl β refl
π β€π β€Ο β€Ο π refl β refl
π β€π β€Ο β€Ο β€π refl β refl
π β€π β€Ο β€Ο β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π β€π π refl β refl
π β€Ο π β€π β€π refl β refl
π β€Ο π β€π β€Ο refl β refl
π β€Ο π β€Ο π refl β refl
π β€Ο π β€Ο β€π refl β refl
π β€Ο π β€Ο β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π β€π π refl β refl
π β€Ο π β€π β€π refl β refl
π β€Ο π β€π β€Ο refl β refl
π β€Ο π β€Ο π refl β refl
π β€Ο π β€Ο β€π refl β refl
π β€Ο π β€Ο β€Ο refl β refl
π β€Ο β€π π π refl β refl
π β€Ο β€π π β€π refl β refl
π β€Ο β€π π β€Ο refl β refl
π β€Ο β€π π π refl β refl
π β€Ο β€π π β€π refl β refl
π β€Ο β€π π β€Ο refl β refl
π β€Ο β€π β€π π refl β refl
π β€Ο β€π β€π β€π refl β refl
π β€Ο β€π β€π β€Ο refl β refl
π β€Ο β€π β€Ο π refl β refl
π β€Ο β€π β€Ο β€π refl β refl
π β€Ο β€π β€Ο β€Ο refl β refl
π β€Ο β€Ο π π refl β refl
π β€Ο β€Ο π β€π refl β refl
π β€Ο β€Ο π β€Ο refl β refl
π β€Ο β€Ο π π refl β refl
π β€Ο β€Ο π β€π refl β refl
π β€Ο β€Ο π β€Ο refl β refl
π β€Ο β€Ο β€π π refl β refl
π β€Ο β€Ο β€π β€π refl β refl
π β€Ο β€Ο β€π β€Ο refl β refl
π β€Ο β€Ο β€Ο π refl β refl
π β€Ο β€Ο β€Ο β€π refl β refl
π β€Ο β€Ο β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π β€π π refl β refl
π π β€π β€π β€π refl β refl
π π β€π β€π β€Ο refl β refl
π π β€π β€Ο π refl β refl
π π β€π β€Ο β€π refl β refl
π π β€π β€Ο β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο β€π π refl β refl
π π β€Ο β€π β€π refl β refl
π π β€Ο β€π β€Ο refl β refl
π π β€Ο β€Ο π refl β refl
π π β€Ο β€Ο β€π refl β refl
π π β€Ο β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π π π refl β refl
π π π π β€π refl β refl
π π π π β€Ο refl β refl
π π π β€π π refl β refl
π π π β€π β€π refl β refl
π π π β€π β€Ο refl β refl
π π π β€Ο π refl β refl
π π π β€Ο β€π refl β refl
π π π β€Ο β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π π π refl β refl
π π β€π π β€π refl β refl
π π β€π π β€Ο refl β refl
π π β€π β€π π refl β refl
π π β€π β€π β€π refl β refl
π π β€π β€π β€Ο refl β refl
π π β€π β€Ο π refl β refl
π π β€π β€Ο β€π refl β refl
π π β€π β€Ο β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο π π refl β refl
π π β€Ο π β€π refl β refl
π π β€Ο π β€Ο refl β refl
π π β€Ο β€π π refl β refl
π π β€Ο β€π β€π refl β refl
π π β€Ο β€π β€Ο refl β refl
π π β€Ο β€Ο π refl β refl
π π β€Ο β€Ο β€π refl β refl
π π β€Ο β€Ο β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π β€π π refl β refl
π β€π π β€π β€π refl β refl
π β€π π β€π β€Ο refl β refl
π β€π π β€Ο π refl β refl
π β€π π β€Ο β€π refl β refl
π β€π π β€Ο β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π π π refl β refl
π β€π π π β€π refl β refl
π β€π π π β€Ο refl β refl
π β€π π β€π π refl β refl
π β€π π β€π β€π refl β refl
π β€π π β€π β€Ο refl β refl
π β€π π β€Ο π refl β refl
π β€π π β€Ο β€π refl β refl
π β€π π β€Ο β€Ο refl β refl
π β€π β€π π π refl β refl
π β€π β€π π β€π refl β refl
π β€π β€π π β€Ο refl β refl
π β€π β€π π π refl β refl
π β€π β€π π β€π refl β refl
π β€π β€π π β€Ο refl β refl
π β€π β€π β€π π refl β refl
π β€π β€π β€π β€π refl β refl
π β€π β€π β€π β€Ο refl β refl
π β€π β€π β€Ο π refl β refl
π β€π β€π β€Ο β€π refl β refl
π β€π β€π β€Ο β€Ο refl β refl
π β€π β€Ο π π refl β refl
π β€π β€Ο π β€π refl β refl
π β€π β€Ο π β€Ο refl β refl
π β€π β€Ο π π refl β refl
π β€π β€Ο π β€π refl β refl
π β€π β€Ο π β€Ο refl β refl
π β€π β€Ο β€π π refl β refl
π β€π β€Ο β€π β€π refl β refl
π β€π β€Ο β€π β€Ο refl β refl
π β€π β€Ο β€Ο π refl β refl
π β€π β€Ο β€Ο β€π refl β refl
π β€π β€Ο β€Ο β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π β€π π refl β refl
π β€Ο π β€π β€π refl β refl
π β€Ο π β€π β€Ο refl β refl
π β€Ο π β€Ο π refl β refl
π β€Ο π β€Ο β€π refl β refl
π β€Ο π β€Ο β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π π π refl β refl
π β€Ο π π β€π refl β refl
π β€Ο π π β€Ο refl β refl
π β€Ο π β€π π refl β refl
π β€Ο π β€π β€π refl β refl
π β€Ο π β€π β€Ο refl β refl
π β€Ο π β€Ο π refl β refl
π β€Ο π β€Ο β€π refl β refl
π β€Ο π β€Ο β€Ο refl β refl
π β€Ο β€π π π refl β refl
π β€Ο β€π π β€π refl β refl
π β€Ο β€π π β€Ο refl β refl
π β€Ο β€π π π refl β refl
π β€Ο β€π π β€π refl β refl
π β€Ο β€π π β€Ο refl β refl
π β€Ο β€π β€π π refl β refl
π β€Ο β€π β€π β€π refl β refl
π β€Ο β€π β€π β€Ο refl β refl
π β€Ο β€π β€Ο π refl β refl
π β€Ο β€π β€Ο β€π refl β refl
π β€Ο β€π β€Ο β€Ο refl β refl
π β€Ο β€Ο π π refl β refl
π β€Ο β€Ο π β€π refl β refl
π β€Ο β€Ο π β€Ο refl β refl
π β€Ο β€Ο π π refl β refl
π β€Ο β€Ο π β€π refl β refl
π β€Ο β€Ο π β€Ο refl β refl
π β€Ο β€Ο β€π π refl β refl
π β€Ο β€Ο β€π β€π refl β refl
π β€Ο β€Ο β€π β€Ο refl β refl
π β€Ο β€Ο β€Ο π refl β refl
π β€Ο β€Ο β€Ο β€π refl β refl
π β€Ο β€Ο β€Ο β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π β€π π refl β refl
β€π π π β€π β€π refl β refl
β€π π π β€π β€Ο refl β refl
β€π π π β€Ο π refl β refl
β€π π π β€Ο β€π refl β refl
β€π π π β€Ο β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π β€π π refl β refl
β€π π π β€π β€π refl β refl
β€π π π β€π β€Ο refl β refl
β€π π π β€Ο π refl β refl
β€π π π β€Ο β€π refl β refl
β€π π π β€Ο β€Ο refl β refl
β€π π β€π π π refl β refl
β€π π β€π π β€π refl β refl
β€π π β€π π β€Ο refl β refl
β€π π β€π π π refl β refl
β€π π β€π π β€π refl β refl
β€π π β€π π β€Ο refl β refl
β€π π β€π β€π π refl β refl
β€π π β€π β€π β€π refl β refl
β€π π β€π β€π β€Ο refl β refl
β€π π β€π β€Ο π refl β refl
β€π π β€π β€Ο β€π refl β refl
β€π π β€π β€Ο β€Ο refl β refl
β€π π β€Ο π π refl β refl
β€π π β€Ο π β€π refl β refl
β€π π β€Ο π β€Ο refl β refl
β€π π β€Ο π π refl β refl
β€π π β€Ο π β€π refl β refl
β€π π β€Ο π β€Ο refl β refl
β€π π β€Ο β€π π refl β refl
β€π π β€Ο β€π β€π refl β refl
β€π π β€Ο β€π β€Ο refl β refl
β€π π β€Ο β€Ο π refl β refl
β€π π β€Ο β€Ο β€π refl β refl
β€π π β€Ο β€Ο β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π β€π π refl β refl
β€π π π β€π β€π refl β refl
β€π π π β€π β€Ο refl β refl
β€π π π β€Ο π refl β refl
β€π π π β€Ο β€π refl β refl
β€π π π β€Ο β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π π π refl β refl
β€π π π π β€π refl β refl
β€π π π π β€Ο refl β refl
β€π π π β€π π refl β refl
β€π π π β€π β€π refl β refl
β€π π π β€π β€Ο refl β refl
β€π π π β€Ο π refl β refl
β€π π π β€Ο β€π refl β refl
β€π π π β€Ο β€Ο refl β refl
β€π π β€π π π refl β refl
β€π π β€π π β€π refl β refl
β€π π β€π π β€Ο refl β refl
β€π π β€π π π refl β refl
β€π π β€π π β€π refl β refl
β€π π β€π π β€Ο refl β refl
β€π π β€π β€π π refl β refl
β€π π β€π β€π β€π refl β refl
β€π π β€π β€π β€Ο refl β refl
β€π π β€π β€Ο π refl β refl
β€π π β€π β€Ο β€π refl β refl
β€π π β€π β€Ο β€Ο refl β refl
β€π π β€Ο π π refl β refl
β€π π β€Ο π β€π refl β refl
β€π π β€Ο π β€Ο refl β refl
β€π π β€Ο π π refl β refl
β€π π β€Ο π β€π refl β refl
β€π π β€Ο π β€Ο refl β refl
β€π π β€Ο β€π π refl β refl
β€π π β€Ο β€π β€π refl β refl
β€π π β€Ο β€π β€Ο refl β refl
β€π π β€Ο β€Ο π refl β refl
β€π π β€Ο β€Ο β€π refl β refl
β€π π β€Ο β€Ο β€Ο refl β refl
β€π β€π π π π refl β refl
β€π β€π π π β€π refl β refl
β€π β€π π π β€Ο refl β refl
β€π β€π π π π refl β refl
β€π β€π π π β€π refl β refl
β€π β€π π π β€Ο refl β refl
β€π β€π π β€π π refl β refl
β€π β€π π β€π β€π refl β refl
β€π β€π π β€π β€Ο refl β refl
β€π β€π π β€Ο π refl β refl
β€π β€π π β€Ο β€π refl β refl
β€π β€π π β€Ο β€Ο refl β refl
β€π β€π π π π refl β refl
β€π β€π π π β€π refl β refl
β€π β€π π π β€Ο refl β refl
β€π β€π π π π refl β refl
β€π β€π π π β€π refl β refl
β€π β€π π π β€Ο refl β refl
β€π β€π π β€π π refl β refl
β€π β€π π β€π β€π refl β refl
β€π β€π π β€π β€Ο refl β refl
β€π β€π π β€Ο π refl β refl
β€π β€π π β€Ο β€π refl β refl
β€π β€π π β€Ο β€Ο refl β refl
β€π β€π β€π π π refl β refl
β€π β€π β€π π β€π refl β refl
β€π β€π β€π π β€Ο refl β refl
β€π β€π β€π π π refl β refl
β€π β€π β€π π β€π refl β refl
β€π β€π β€π π β€Ο refl β refl
β€π β€π β€π β€π π refl β refl
β€π β€π β€π β€π β€π refl β refl
β€π β€π β€π β€π β€Ο refl β refl
β€π β€π β€π β€Ο π refl β refl
β€π β€π β€π β€Ο β€π refl β refl
β€π β€π β€π β€Ο β€Ο refl β refl
β€π β€π β€Ο π π refl β refl
β€π β€π β€Ο π β€π refl β refl
β€π β€π β€Ο π β€Ο refl β refl
β€π β€π β€Ο π π refl β refl
β€π β€π β€Ο π β€π refl β refl
β€π β€π β€Ο π β€Ο refl β refl
β€π β€π β€Ο β€π π refl β refl
β€π β€π β€Ο β€π β€π refl β refl
β€π β€π β€Ο β€π β€Ο refl β refl
β€π β€π β€Ο β€Ο π refl β refl
β€π β€π β€Ο β€Ο β€π refl β refl
β€π β€π β€Ο β€Ο β€Ο refl β refl
β€π β€Ο π π π refl β refl
β€π β€Ο π π β€π refl β refl
β€π β€Ο π π β€Ο refl β refl
β€π β€Ο π π π refl β refl
β€π β€Ο π π β€π refl β refl
β€π β€Ο π π β€Ο refl β refl
β€π β€Ο π β€π π refl β refl
β€π β€Ο π β€π β€π refl β refl
β€π β€Ο π β€π β€Ο refl β refl
β€π β€Ο π β€Ο π refl β refl
β€π β€Ο π β€Ο β€π refl β refl
β€π β€Ο π β€Ο β€Ο refl β refl
β€π β€Ο π π π refl β refl
β€π β€Ο π π β€π refl β refl
β€π β€Ο π π β€Ο refl β refl
β€π β€Ο π π π refl β refl
β€π β€Ο π π β€π refl β refl
β€π β€Ο π π β€Ο refl β refl
β€π β€Ο π β€π π refl β refl
β€π β€Ο π β€π β€π refl β refl
β€π β€Ο π β€π β€Ο refl β refl
β€π β€Ο π β€Ο π refl β refl
β€π β€Ο π β€Ο β€π refl β refl
β€π β€Ο π β€Ο β€Ο refl β refl
β€π β€Ο β€π π π refl β refl
β€π β€Ο β€π π β€π refl β refl
β€π β€Ο β€π π β€Ο refl β refl
β€π β€Ο β€π π π refl β refl
β€π β€Ο β€π π β€π refl β refl
β€π β€Ο β€π π β€Ο refl β refl
β€π β€Ο β€π β€π π refl β refl
β€π β€Ο β€π β€π β€π refl β refl
β€π β€Ο β€π β€π β€Ο refl β refl
β€π β€Ο β€π β€Ο π refl β refl
β€π β€Ο β€π β€Ο β€π refl β refl
β€π β€Ο β€π β€Ο β€Ο refl β refl
β€π β€Ο β€Ο π π refl β refl
β€π β€Ο β€Ο π β€π refl β refl
β€π β€Ο β€Ο π β€Ο refl β refl
β€π β€Ο β€Ο π π refl β refl
β€π β€Ο β€Ο π β€π refl β refl
β€π β€Ο β€Ο π β€Ο refl β refl
β€π β€Ο β€Ο β€π π refl β refl
β€π β€Ο β€Ο β€π β€π refl β refl
β€π β€Ο β€Ο β€π β€Ο refl β refl
β€π β€Ο β€Ο β€Ο π refl β refl
β€π β€Ο β€Ο β€Ο β€π refl β refl
β€π β€Ο β€Ο β€Ο β€Ο refl β refl
β€Ο _ π π π refl β refl
β€Ο _ π π β€π refl β refl
β€Ο _ π π β€Ο refl β refl
β€Ο _ π π π refl β refl
β€Ο _ π π β€π refl β refl
β€Ο _ π π β€Ο refl β refl
β€Ο _ π β€π π refl β refl
β€Ο _ π β€π β€π refl β refl
β€Ο _ π β€π β€Ο refl β refl
β€Ο _ π β€Ο π refl β refl
β€Ο _ π β€Ο β€π refl β refl
β€Ο _ π β€Ο β€Ο refl β refl
β€Ο _ π π π refl β refl
β€Ο _ π π β€π refl β refl
β€Ο _ π π β€Ο refl β refl
β€Ο _ π π π refl β refl
β€Ο _ π π β€π refl β refl
β€Ο _ π π β€Ο refl β refl
β€Ο _ π β€π π refl β refl
β€Ο _ π β€π β€π refl β refl
β€Ο _ π β€π β€Ο refl β refl
β€Ο _ π β€Ο π refl β refl
β€Ο _ π β€Ο β€π refl β refl
β€Ο _ π β€Ο β€Ο refl β refl
β€Ο _ β€π π π refl β refl
β€Ο _ β€π π β€π refl β refl
β€Ο _ β€π π β€Ο refl β refl
β€Ο _ β€π π π refl β refl
β€Ο _ β€π π β€π refl β refl
β€Ο _ β€π π β€Ο refl β refl
β€Ο _ β€π β€π π refl β refl
β€Ο _ β€π β€π β€π refl β refl
β€Ο _ β€π β€π β€Ο refl β refl
β€Ο _ β€π β€Ο π refl β refl
β€Ο _ β€π β€Ο β€π refl β refl
β€Ο _ β€π β€Ο β€Ο refl β refl
β€Ο _ β€Ο π π refl β refl
β€Ο _ β€Ο π β€π refl β refl
β€Ο _ β€Ο π β€Ο refl β refl
β€Ο _ β€Ο π π refl β refl
β€Ο _ β€Ο π β€π refl β refl
β€Ο _ β€Ο π β€Ο refl β refl
β€Ο _ β€Ο β€π π refl β refl
β€Ο _ β€Ο β€π β€π refl β refl
β€Ο _ β€Ο β€π β€Ο refl β refl
β€Ο _ β€Ο β€Ο π refl β refl
β€Ο _ β€Ο β€Ο β€π refl β refl
β€Ο _ β€Ο β€Ο β€Ο refl β refl
_ _ _ _ π ()
nr-suc : β r p z s n β nr p r z s n β€ s + p Β· n + r Β· nr p r z s n
nr-suc = Ξ» where
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π β€π π β refl
π π β€π β€π π β refl
π π β€π β€π β€π β refl
π π β€π β€π β€Ο β refl
π π β€π β€Ο π β refl
π π β€π β€Ο π β refl
π π β€π β€Ο β€π β refl
π π β€π β€Ο β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο β€π π β refl
π π β€Ο β€π π β refl
π π β€Ο β€π β€π β refl
π π β€Ο β€π β€Ο β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο β€π β refl
π π β€Ο β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π β€π π β refl
π π β€π β€π π β refl
π π β€π β€π β€π β refl
π π β€π β€π β€Ο β refl
π π β€π β€Ο π β refl
π π β€π β€Ο π β refl
π π β€π β€Ο β€π β refl
π π β€π β€Ο β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο β€π π β refl
π π β€Ο β€π π β refl
π π β€Ο β€π β€π β refl
π π β€Ο β€π β€Ο β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο β€π β refl
π π β€Ο β€Ο β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π β€π π β refl
π β€π π β€π π β refl
π β€π π β€π β€π β refl
π β€π π β€π β€Ο β refl
π β€π π β€Ο π β refl
π β€π π β€Ο π β refl
π β€π π β€Ο β€π β refl
π β€π π β€Ο β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π β€π π β refl
π β€π π β€π π β refl
π β€π π β€π β€π β refl
π β€π π β€π β€Ο β refl
π β€π π β€Ο π β refl
π β€π π β€Ο π β refl
π β€π π β€Ο β€π β refl
π β€π π β€Ο β€Ο β refl
π β€π β€π π π β refl
π β€π β€π π π β refl
π β€π β€π π β€π β refl
π β€π β€π π β€Ο β refl
π β€π β€π π π β refl
π β€π β€π π π β refl
π β€π β€π π β€π β refl
π β€π β€π π β€Ο β refl
π β€π β€π β€π π β refl
π β€π β€π β€π π β refl
π β€π β€π β€π β€π β refl
π β€π β€π β€π β€Ο β refl
π β€π β€π β€Ο π β refl
π β€π β€π β€Ο π β refl
π β€π β€π β€Ο β€π β refl
π β€π β€π β€Ο β€Ο β refl
π β€π β€Ο π π β refl
π β€π β€Ο π π β refl
π β€π β€Ο π β€π β refl
π β€π β€Ο π β€Ο β refl
π β€π β€Ο π π β refl
π β€π β€Ο π π β refl
π β€π β€Ο π β€π β refl
π β€π β€Ο π β€Ο β refl
π β€π β€Ο β€π π β refl
π β€π β€Ο β€π π β refl
π β€π β€Ο β€π β€π β refl
π β€π β€Ο β€π β€Ο β refl
π β€π β€Ο β€Ο π β refl
π β€π β€Ο β€Ο π β refl
π β€π β€Ο β€Ο β€π β refl
π β€π β€Ο β€Ο β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π β€π π β refl
π β€Ο π β€π π β refl
π β€Ο π β€π β€π β refl
π β€Ο π β€π β€Ο β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο β€π β refl
π β€Ο π β€Ο β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π β€π π β refl
π β€Ο π β€π π β refl
π β€Ο π β€π β€π β refl
π β€Ο π β€π β€Ο β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο β€π β refl
π β€Ο π β€Ο β€Ο β refl
π β€Ο β€π π π β refl
π β€Ο β€π π π β refl
π β€Ο β€π π β€π β refl
π β€Ο β€π π β€Ο β refl
π β€Ο β€π π π β refl
π β€Ο β€π π π β refl
π β€Ο β€π π β€π β refl
π β€Ο β€π π β€Ο β refl
π β€Ο β€π β€π π β refl
π β€Ο β€π β€π π β refl
π β€Ο β€π β€π β€π β refl
π β€Ο β€π β€π β€Ο β refl
π β€Ο β€π β€Ο π β refl
π β€Ο β€π β€Ο π β refl
π β€Ο β€π β€Ο β€π β refl
π β€Ο β€π β€Ο β€Ο β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π β€π β refl
π β€Ο β€Ο π β€Ο β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π β€π β refl
π β€Ο β€Ο π β€Ο β refl
π β€Ο β€Ο β€π π β refl
π β€Ο β€Ο β€π π β refl
π β€Ο β€Ο β€π β€π β refl
π β€Ο β€Ο β€π β€Ο β refl
π β€Ο β€Ο β€Ο π β refl
π β€Ο β€Ο β€Ο π β refl
π β€Ο β€Ο β€Ο β€π β refl
π β€Ο β€Ο β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π β€π π β refl
π π β€π β€π π β refl
π π β€π β€π β€π β refl
π π β€π β€π β€Ο β refl
π π β€π β€Ο π β refl
π π β€π β€Ο π β refl
π π β€π β€Ο β€π β refl
π π β€π β€Ο β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο β€π π β refl
π π β€Ο β€π π β refl
π π β€Ο β€π β€π β refl
π π β€Ο β€π β€Ο β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο β€π β refl
π π β€Ο β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π π π β refl
π π π π π β refl
π π π π β€π β refl
π π π π β€Ο β refl
π π π β€π π β refl
π π π β€π π β refl
π π π β€π β€π β refl
π π π β€π β€Ο β refl
π π π β€Ο π β refl
π π π β€Ο π β refl
π π π β€Ο β€π β refl
π π π β€Ο β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π π π β refl
π π β€π π π β refl
π π β€π π β€π β refl
π π β€π π β€Ο β refl
π π β€π β€π π β refl
π π β€π β€π π β refl
π π β€π β€π β€π β refl
π π β€π β€π β€Ο β refl
π π β€π β€Ο π β refl
π π β€π β€Ο π β refl
π π β€π β€Ο β€π β refl
π π β€π β€Ο β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο π π β refl
π π β€Ο π π β refl
π π β€Ο π β€π β refl
π π β€Ο π β€Ο β refl
π π β€Ο β€π π β refl
π π β€Ο β€π π β refl
π π β€Ο β€π β€π β refl
π π β€Ο β€π β€Ο β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο π β refl
π π β€Ο β€Ο β€π β refl
π π β€Ο β€Ο β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π β€π π β refl
π β€π π β€π π β refl
π β€π π β€π β€π β refl
π β€π π β€π β€Ο β refl
π β€π π β€Ο π β refl
π β€π π β€Ο π β refl
π β€π π β€Ο β€π β refl
π β€π π β€Ο β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π π π β refl
π β€π π π π β refl
π β€π π π β€π β refl
π β€π π π β€Ο β refl
π β€π π β€π π β refl
π β€π π β€π π β refl
π β€π π β€π β€π β refl
π β€π π β€π β€Ο β refl
π β€π π β€Ο π β refl
π β€π π β€Ο π β refl
π β€π π β€Ο β€π β refl
π β€π π β€Ο β€Ο β refl
π β€π β€π π π β refl
π β€π β€π π π β refl
π β€π β€π π β€π β refl
π β€π β€π π β€Ο β refl
π β€π β€π π π β refl
π β€π β€π π π β refl
π β€π β€π π β€π β refl
π β€π β€π π β€Ο β refl
π β€π β€π β€π π β refl
π β€π β€π β€π π β refl
π β€π β€π β€π β€π β refl
π β€π β€π β€π β€Ο β refl
π β€π β€π β€Ο π β refl
π β€π β€π β€Ο π β refl
π β€π β€π β€Ο β€π β refl
π β€π β€π β€Ο β€Ο β refl
π β€π β€Ο π π β refl
π β€π β€Ο π π β refl
π β€π β€Ο π β€π β refl
π β€π β€Ο π β€Ο β refl
π β€π β€Ο π π β refl
π β€π β€Ο π π β refl
π β€π β€Ο π β€π β refl
π β€π β€Ο π β€Ο β refl
π β€π β€Ο β€π π β refl
π β€π β€Ο β€π π β refl
π β€π β€Ο β€π β€π β refl
π β€π β€Ο β€π β€Ο β refl
π β€π β€Ο β€Ο π β refl
π β€π β€Ο β€Ο π β refl
π β€π β€Ο β€Ο β€π β refl
π β€π β€Ο β€Ο β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π β€π π β refl
π β€Ο π β€π π β refl
π β€Ο π β€π β€π β refl
π β€Ο π β€π β€Ο β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο β€π β refl
π β€Ο π β€Ο β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π π π β refl
π β€Ο π π π β refl
π β€Ο π π β€π β refl
π β€Ο π π β€Ο β refl
π β€Ο π β€π π β refl
π β€Ο π β€π π β refl
π β€Ο π β€π β€π β refl
π β€Ο π β€π β€Ο β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο π β refl
π β€Ο π β€Ο β€π β refl
π β€Ο π β€Ο β€Ο β refl
π β€Ο β€π π π β refl
π β€Ο β€π π π β refl
π β€Ο β€π π β€π β refl
π β€Ο β€π π β€Ο β refl
π β€Ο β€π π π β refl
π β€Ο β€π π π β refl
π β€Ο β€π π β€π β refl
π β€Ο β€π π β€Ο β refl
π β€Ο β€π β€π π β refl
π β€Ο β€π β€π π β refl
π β€Ο β€π β€π β€π β refl
π β€Ο β€π β€π β€Ο β refl
π β€Ο β€π β€Ο π β refl
π β€Ο β€π β€Ο π β refl
π β€Ο β€π β€Ο β€π β refl
π β€Ο β€π β€Ο β€Ο β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π β€π β refl
π β€Ο β€Ο π β€Ο β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π π β refl
π β€Ο β€Ο π β€π β refl
π β€Ο β€Ο π β€Ο β refl
π β€Ο β€Ο β€π π β refl
π β€Ο β€Ο β€π π β refl
π β€Ο β€Ο β€π β€π β refl
π β€Ο β€Ο β€π β€Ο β refl
π β€Ο β€Ο β€Ο π β refl
π β€Ο β€Ο β€Ο π β refl
π β€Ο β€Ο β€Ο β€π β refl
π β€Ο β€Ο β€Ο β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π β€π π β refl
β€π π π β€π π β refl
β€π π π β€π β€π β refl
β€π π π β€π β€Ο β refl
β€π π π β€Ο π β refl
β€π π π β€Ο π β refl
β€π π π β€Ο β€π β refl
β€π π π β€Ο β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π β€π π β refl
β€π π π β€π π β refl
β€π π π β€π β€π β refl
β€π π π β€π β€Ο β refl
β€π π π β€Ο π β refl
β€π π π β€Ο π β refl
β€π π π β€Ο β€π β refl
β€π π π β€Ο β€Ο β refl
β€π π β€π π π β refl
β€π π β€π π π β refl
β€π π β€π π β€π β refl
β€π π β€π π β€Ο β refl
β€π π β€π π π β refl
β€π π β€π π π β refl
β€π π β€π π β€π β refl
β€π π β€π π β€Ο β refl
β€π π β€π β€π π β refl
β€π π β€π β€π π β refl
β€π π β€π β€π β€π β refl
β€π π β€π β€π β€Ο β refl
β€π π β€π β€Ο π β refl
β€π π β€π β€Ο π β refl
β€π π β€π β€Ο β€π β refl
β€π π β€π β€Ο β€Ο β refl
β€π π β€Ο π π β refl
β€π π β€Ο π π β refl
β€π π β€Ο π β€π β refl
β€π π β€Ο π β€Ο β refl
β€π π β€Ο π π β refl
β€π π β€Ο π π β refl
β€π π β€Ο π β€π β refl
β€π π β€Ο π β€Ο β refl
β€π π β€Ο β€π π β refl
β€π π β€Ο β€π π β refl
β€π π β€Ο β€π β€π β refl
β€π π β€Ο β€π β€Ο β refl
β€π π β€Ο β€Ο π β refl
β€π π β€Ο β€Ο π β refl
β€π π β€Ο β€Ο β€π β refl
β€π π β€Ο β€Ο β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π β€π π β refl
β€π π π β€π π β refl
β€π π π β€π β€π β refl
β€π π π β€π β€Ο β refl
β€π π π β€Ο π β refl
β€π π π β€Ο π β refl
β€π π π β€Ο β€π β refl
β€π π π β€Ο β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π π π β refl
β€π π π π π β refl
β€π π π π β€π β refl
β€π π π π β€Ο β refl
β€π π π β€π π β refl
β€π π π β€π π β refl
β€π π π β€π β€π β refl
β€π π π β€π β€Ο β refl
β€π π π β€Ο π β refl
β€π π π β€Ο π β refl
β€π π π β€Ο β€π β refl
β€π π π β€Ο β€Ο β refl
β€π π β€π π π β refl
β€π π β€π π π β refl
β€π π β€π π β€π β refl
β€π π β€π π β€Ο β refl
β€π π β€π π π β refl
β€π π β€π π π β refl
β€π π β€π π β€π β refl
β€π π β€π π β€Ο β refl
β€π π β€π β€π π β refl
β€π π β€π β€π π β refl
β€π π β€π β€π β€π β refl
β€π π β€π β€π β€Ο β refl
β€π π β€π β€Ο π β refl
β€π π β€π β€Ο π β refl
β€π π β€π β€Ο β€π β refl
β€π π β€π β€Ο β€Ο β refl
β€π π β€Ο π π β refl
β€π π β€Ο π π β refl
β€π π β€Ο π β€π β refl
β€π π β€Ο π β€Ο β refl
β€π π β€Ο π π β refl
β€π π β€Ο π π β refl
β€π π β€Ο π β€π β refl
β€π π β€Ο π β€Ο β refl
β€π π β€Ο β€π π β refl
β€π π β€Ο β€π π β refl
β€π π β€Ο β€π β€π β refl
β€π π β€Ο β€π β€Ο β refl
β€π π β€Ο β€Ο π β refl
β€π π β€Ο β€Ο π β refl
β€π π β€Ο β€Ο β€π β refl
β€π π β€Ο β€Ο β€Ο β refl
β€π β€π π π π β refl
β€π β€π π π π β refl
β€π β€π π π β€π β refl
β€π β€π π π β€Ο β refl
β€π β€π π π π β refl
β€π β€π π π π β refl
β€π β€π π π β€π β refl
β€π β€π π π β€Ο β refl
β€π β€π π β€π π β refl
β€π β€π π β€π π β refl
β€π β€π π β€π β€π β refl
β€π β€π π β€π β€Ο β refl
β€π β€π π β€Ο π β refl
β€π β€π π β€Ο π β refl
β€π β€π π β€Ο β€π β refl
β€π β€π π β€Ο β€Ο β refl
β€π β€π π π π β refl
β€π β€π π π π β refl
β€π β€π π π β€π β refl
β€π β€π π π β€Ο β refl
β€π β€π π π π β refl
β€π β€π π π π β refl
β€π β€π π π β€π β refl
β€π β€π π π β€Ο β refl
β€π β€π π β€π π β refl
β€π β€π π β€π π β refl
β€π β€π π β€π β€π β refl
β€π β€π π β€π β€Ο β refl
β€π β€π π β€Ο π β refl
β€π β€π π β€Ο π β refl
β€π β€π π β€Ο β€π β refl
β€π β€π π β€Ο β€Ο β refl
β€π β€π β€π π π β refl
β€π β€π β€π π π β refl
β€π β€π β€π π β€π β refl
β€π β€π β€π π β€Ο β refl
β€π β€π β€π π π β refl
β€π β€π β€π π π β refl
β€π β€π β€π π β€π β refl
β€π β€π β€π π β€Ο β refl
β€π β€π β€π β€π π β refl
β€π β€π β€π β€π π β refl
β€π β€π β€π β€π β€π β refl
β€π β€π β€π β€π β€Ο β refl
β€π β€π β€π β€Ο π β refl
β€π β€π β€π β€Ο π β refl
β€π β€π β€π β€Ο β€π β refl
β€π β€π β€π β€Ο β€Ο β refl
β€π β€π β€Ο π π β refl
β€π β€π β€Ο π π β refl
β€π β€π β€Ο π β€π β refl
β€π β€π β€Ο π β€Ο β refl
β€π β€π β€Ο π π β refl
β€π β€π β€Ο π π β refl
β€π β€π β€Ο π β€π β refl
β€π β€π β€Ο π β€Ο β refl
β€π β€π β€Ο β€π π β refl
β€π β€π β€Ο β€π π β refl
β€π β€π β€Ο β€π β€π β refl
β€π β€π β€Ο β€π β€Ο β refl
β€π β€π β€Ο β€Ο π β refl
β€π β€π β€Ο β€Ο π β refl
β€π β€π β€Ο β€Ο β€π β refl
β€π β€π β€Ο β€Ο β€Ο β refl
β€π β€Ο π π π β refl
β€π β€Ο π π π β refl
β€π β€Ο π π β€π β refl
β€π β€Ο π π β€Ο β refl
β€π β€Ο π π π β refl
β€π β€Ο π π π β refl
β€π β€Ο π π β€π β refl
β€π β€Ο π π β€Ο β refl
β€π β€Ο π β€π π β refl
β€π β€Ο π β€π π β refl
β€π β€Ο π β€π β€π β refl
β€π β€Ο π β€π β€Ο β refl
β€π β€Ο π β€Ο π β refl
β€π β€Ο π β€Ο π β refl
β€π β€Ο π β€Ο β€π β refl
β€π β€Ο π β€Ο β€Ο β refl
β€π β€Ο π π π β refl
β€π β€Ο π π π β refl
β€π β€Ο π π β€π β refl
β€π β€Ο π π β€Ο β refl
β€π β€Ο π π π β refl
β€π β€Ο π π π β refl
β€π β€Ο π π β€π β refl
β€π β€Ο π π β€Ο β refl
β€π β€Ο π β€π π β refl
β€π β€Ο π β€π π β refl
β€π β€Ο π β€π β€π β refl
β€π β€Ο π β€π β€Ο β refl
β€π β€Ο π β€Ο π β refl
β€π β€Ο π β€Ο π β refl
β€π β€Ο π β€Ο β€π β refl
β€π β€Ο π β€Ο β€Ο β refl
β€π β€Ο β€π π π β refl
β€π β€Ο β€π π π β refl
β€π β€Ο β€π π β€π β refl
β€π β€Ο β€π π β€Ο β refl
β€π β€Ο β€π π π β refl
β€π β€Ο β€π π π β refl
β€π β€Ο β€π π β€π β refl
β€π β€Ο β€π π β€Ο β refl
β€π β€Ο β€π β€π π β refl
β€π β€Ο β€π β€π π β refl
β€π β€Ο β€π β€π β€π β refl
β€π β€Ο β€π β€π β€Ο β refl
β€π β€Ο β€π β€Ο π β refl
β€π β€Ο β€π β€Ο π β refl
β€π β€Ο β€π β€Ο β€π β refl
β€π β€Ο β€π β€Ο β€Ο β refl
β€π β€Ο β€Ο π π β refl
β€π β€Ο β€Ο π π β refl
β€π β€Ο β€Ο π β€π β refl
β€π β€Ο β€Ο π β€Ο β refl
β€π β€Ο β€Ο π π β refl
β€π β€Ο β€Ο π π β refl
β€π β€Ο β€Ο π β€π β refl
β€π β€Ο β€Ο π β€Ο β refl
β€π β€Ο β€Ο β€π π β refl
β€π β€Ο β€Ο β€π π β refl
β€π β€Ο β€Ο β€π β€π β refl
β€π β€Ο β€Ο β€π β€Ο β refl
β€π β€Ο β€Ο β€Ο π β refl
β€π β€Ο β€Ο β€Ο π β refl
β€π β€Ο β€Ο β€Ο β€π β refl
β€π β€Ο β€Ο β€Ο β€Ο β refl
β€Ο π π π π β refl
β€Ο π π π π β refl
β€Ο β€π π π π β refl
β€Ο β€Ο π π π β refl
β€Ο _ π π π β refl
β€Ο _ π π β€π β refl
β€Ο _ π π β€Ο β refl
β€Ο _ π π π β refl
β€Ο _ π π π β refl
β€Ο _ π π β€π β refl
β€Ο _ π π β€Ο β refl
β€Ο _ π β€π π β refl
β€Ο _ π β€π π β refl
β€Ο _ π β€π β€π β refl
β€Ο _ π β€π β€Ο β refl
β€Ο _ π β€Ο π β refl
β€Ο _ π β€Ο π β refl
β€Ο _ π β€Ο β€π β refl
β€Ο _ π β€Ο β€Ο β refl
β€Ο _ π π π β refl
β€Ο _ π π π β refl
β€Ο _ π π β€π β refl
β€Ο _ π π β€Ο β refl
β€Ο _ π π π β refl
β€Ο _ π π π β refl
β€Ο _ π π β€π β refl
β€Ο _ π π β€Ο β refl
β€Ο _ π β€π π β refl
β€Ο _ π β€π π β refl
β€Ο _ π β€π β€π β refl
β€Ο _ π β€π β€Ο β refl
β€Ο _ π β€Ο π β refl
β€Ο _ π β€Ο π β refl
β€Ο _ π β€Ο β€π β refl
β€Ο _ π β€Ο β€Ο β refl
β€Ο _ β€π π π β refl
β€Ο _ β€π π π β refl
β€Ο _ β€π π β€π β refl
β€Ο _ β€π π β€Ο β refl
β€Ο _ β€π π π β refl
β€Ο _ β€π π π β refl
β€Ο _ β€π π β€π β refl
β€Ο _ β€π π β€Ο β refl
β€Ο _ β€π β€π π β refl
β€Ο _ β€π β€π π β refl
β€Ο _ β€π β€π β€π β refl
β€Ο _ β€π β€π β€Ο β refl
β€Ο _ β€π β€Ο π β refl
β€Ο _ β€π β€Ο π β refl
β€Ο _ β€π β€Ο β€π β refl
β€Ο _ β€π β€Ο β€Ο β refl
β€Ο _ β€Ο π π β refl
β€Ο _ β€Ο π π β refl
β€Ο _ β€Ο π β€π β refl
β€Ο _ β€Ο π β€Ο β refl
β€Ο _ β€Ο π π β refl
β€Ο _ β€Ο π π β refl
β€Ο _ β€Ο π β€π β refl
β€Ο _ β€Ο π β€Ο β refl
β€Ο _ β€Ο β€π π β refl
β€Ο _ β€Ο β€π π β refl
β€Ο _ β€Ο β€π β€π β refl
β€Ο _ β€Ο β€π β€Ο β refl
β€Ο _ β€Ο β€Ο π β refl
β€Ο _ β€Ο β€Ο π β refl
β€Ο _ β€Ο β€Ο β€π β refl
β€Ο _ β€Ο β€Ο β€Ο β refl
opaque
linear-or-affine-has-factoring-nr :
Is-factoring-nr linear-or-affine-has-nr
linear-or-affine-has-factoring-nr = record
{ nrβ = nrβ
; nrββ’π = Ξ» {p} {r} β πβ§pβ’π (r + p)
; nr-factoring = Ξ» {p} {r} {z} {s} {n} β nr-factoring p r z s n
}
where
open Semiring-with-meet linear-or-affine-semiring-with-meet
hiding (π; π; _+_; _Β·_; _β§_; _β€_)
nrβ : Opβ Linear-or-affine
nrβ p r = π β§ (r + p)
πβ§β€π+pβ‘β€1+p : β p β π β§ (β€π + p) β‘ β€π + p
πβ§β€π+pβ‘β€1+p π = refl
πβ§β€π+pβ‘β€1+p π = refl
πβ§β€π+pβ‘β€1+p β€π = refl
πβ§β€π+pβ‘β€1+p β€Ο = refl
πβ§π+pβ‘1+p : β p β π β§ (π + p) β‘ π + p
πβ§π+pβ‘1+p π = refl
πβ§π+pβ‘1+p π = refl
πβ§π+pβ‘1+p β€π = refl
πβ§π+pβ‘1+p β€Ο = refl
lemma : β p z s n β p β’ π
β (p Β· n + s) β§ (n + z) β‘ p Β· n + s β§ z
lemma π z s n pβ’π = β₯-elim (pβ’π refl)
lemma π z s n pβ’π rewrite Β·-identityΛ‘ n =
sym (+-distribΛ‘-β§ n s z)
lemma β€π z s π pβ’π = refl
lemma β€π π π π pβ’π = refl
lemma β€π π π π pβ’π = refl
lemma β€π β€π π π pβ’π = refl
lemma β€π β€Ο π π pβ’π = refl
lemma β€π π π π pβ’π = refl
lemma β€π π π π pβ’π = refl
lemma β€π β€π π π pβ’π = refl
lemma β€π β€Ο π π pβ’π = refl
lemma β€π π β€π π pβ’π = refl
lemma β€π π β€π π pβ’π = refl
lemma β€π β€π β€π π pβ’π = refl
lemma β€π β€Ο β€π π pβ’π = refl
lemma β€π z β€Ο π pβ’π = refl
lemma β€π z s β€π pβ’π = sym (+-distribΛ‘-β§ β€π s z)
lemma β€π z s β€Ο pβ’π = sym (+-distribΛ‘-β§ β€Ο s z)
lemma β€Ο z s π pβ’π = refl
lemma β€Ο z s π pβ’π rewrite β€Ο+ s rewrite β€Ο+ (s β§ z) = refl
lemma β€Ο z s β€π pβ’π rewrite β€Ο+ s rewrite β€Ο+ (s β§ z) = refl
lemma β€Ο z s β€Ο pβ’π = sym (+-distribΛ‘-β§ β€Ο s z)
nr-factoring : (p r z s n : Linear-or-affine)
β nr p r z s n β‘ nrβ p r Β· n + nr p r z s π
nr-factoring p π z s n rewrite Β·-zeroΚ³ (π β§ p) =
lemma (π β§ p) z s n (πβ§pβ’π p)
nr-factoring p π z s n rewrite Β·-zeroΚ³ (π + p) =
+-congΚ³ (Β·-congΚ³ (sym (πβ§π+pβ‘1+p p)))
nr-factoring p β€π z s n rewrite Β·-zeroΚ³ (β€π + p) =
+-congΚ³ (Β·-congΚ³ (sym (πβ§β€π+pβ‘β€1+p p)))
nr-factoring p β€Ο z s n rewrite β€Ο+ p = Β·-distribΛ‘-+ Ο n (s + z)
opaque
nr-greatest-factoring :
(has-nr : Has-nr linear-or-affine-semiring-with-meet)
(is-factoring-nr : Is-factoring-nr has-nr) β
β p r z s n β Has-nr.nr has-nr p r z s n β€ nr p r z s n
nr-greatest-factoring has-nr is-factoring-nr = Ξ» where
p r β€Ο s n β lemma $ begin
nrβ² p r β€Ο s n β‘β¨ nr-factoring β©
nrββ² p r Β· n + nrβ² p r β€Ο s π β€β¨ +-monotoneΚ³ {r = nrββ² p r Β· n} (nr-zero refl) β©
nrββ² p r Β· n + β€Ο β‘β¨ +-zeroΚ³ (nrββ² p r Β· n) β©
β€Ο β
p r z β€Ο n β lemma $ begin
nrβ² p r z β€Ο n β€β¨ nr-suc β©
β€Ο + p Β· n + r Β· nrβ² p r z β€Ο n β‘β¨ +-zeroΛ‘ (p Β· n + r Β· nrβ² p r z β€Ο n) β©
β€Ο β
p r z s β€Ο β lemma $ begin
nrβ² p r z s β€Ο β‘β¨ nr-factoring β©
nrββ² p r Β· β€Ο + nrβ² p r z s π β‘β¨ +-congΚ³ (β’πΒ·β€Ο nrββ’π) β©
β€Ο + nrβ² p r z s π β‘β¨ +-zeroΛ‘ (nrβ² p r z s π) β©
β€Ο β
p r π π π β begin
nrβ² p r π π π β‘β¨ nrβ²-π β©
π β‘Λβ¨ nr-π r .projβ (refl , refl , refl) β©
nr p r π π π β
β€Ο r z s π β pnβ‘Οβnrβ²β€ refl
β€Ο r z s β€π β pnβ‘Οβnrβ²β€ refl
π r z π π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
π r z β€π π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
π r z π β€π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
β€π r z π π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
β€π r z π β€π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
π r z β€π β€π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
β€π r z β€π π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
β€π r z β€π β€π β pn,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r π π π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r π β€π π β nβ’πβnrβ²β€ (Ξ» ()) Ξ» ()
p r π s π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r β€π s π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r π π β€π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r π β€π β€π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r π s β€π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p r β€π s β€π β nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p β€Ο π π π β nrβ²pΟβ€ Ξ» ()
p β€Ο π π β€π β nrβ²pΟβ€ Ξ» ()
p β€Ο π π n β nrβ²pΟβ€ Ξ» ()
p β€Ο π β€π n β nrβ²pΟβ€ Ξ» ()
p β€Ο π s n β nrβ²pΟβ€ Ξ» ()
p β€Ο β€π s n β nrβ²pΟβ€ Ξ» ()
π π z s π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
π π z s β€π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
β€π π z s π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
β€π π z s β€π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
π β€π z s π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
π β€π z s β€π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
β€π β€π z s π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
β€π β€π z s β€π β p,r,nβ’πβnrβ²β€ (Ξ» ()) (Ξ» ()) (Ξ» ())
p π z π n β r,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p π z β€π n β r,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p β€π z π n β r,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p β€π z β€π n β r,sβ’πβnrβ²β€ (Ξ» ()) (Ξ» ())
p π z s π β begin
nrβ² p π z s π β€β¨ β§-greatest-lower-bound
(β€-trans nr-sucβ² (β€-reflexive (+-identityΚ³ s)))
(nr-zero refl) β©
s β§ z β‘β¨β©
(π + s) β§ z β‘Λβ¨ β§-congΚ³ (+-congΚ³ (Β·-zeroΚ³ (π β§ p))) β©
((π β§ p) Β· π + s) β§ z β‘β¨β©
nr p π z s π β
p π π π n β
let β€pn : nrβ² p π π π n β€ p Β· n
β€pn = begin
nrβ² p π π π n β€β¨ nr-suc β©
π + p Β· n + π Β· nrβ² p π π π π β‘β¨β©
p Β· n + π β‘β¨ +-identityΚ³ (p Β· n) β©
p Β· n β
β€n : nrβ² p π π π n β€ n
β€n = begin
nrβ² p π π π n β‘β¨ nr-factoring β©
nrββ² p π Β· n + nrβ² p π π π π β‘β¨ +-congΛ‘ {nrββ² p π Β· n} nrβ²-π β©
nrββ² p π Β· n + π β‘β¨ +-identityΚ³ (nrββ² p π Β· n) β©
nrββ² p π Β· n β€β¨ Β·-monotoneΛ‘ (β’πββ€π nrββ’π) β©
π Β· n β‘β¨ Β·-identityΛ‘ n β©
n β
in begin
nrβ² p π π π n β€β¨ β§-greatest-lower-bound β€n β€pn β©
n β§ p Β· n β‘Λβ¨ β§-congΚ³ (β§-idem n) β©
(n β§ n) β§ p Β· n β‘β¨ β§-assoc n n (p Β· n) β©
n β§ n β§ p Β· n β‘β¨ β§-comm n (n β§ p Β· n) β©
(n β§ p Β· n) β§ n β‘Λβ¨ β§-congΚ³ (β§-congΚ³ (Β·-identityΛ‘ n)) β©
(π Β· n β§ p Β· n) β§ n β‘Λβ¨ β§-congΚ³ (Β·-distribΚ³-β§ n π p) β©
((π β§ p) Β· n) β§ n β‘Λβ¨ β§-cong (+-identityΚ³ ((π β§ p) Β· n)) (+-identityΚ³ n) β©
((π β§ p) Β· n + π) β§ (n + π) β‘β¨β©
nr p π π π n β
p π z π π β begin
nrβ² p π z π π β€β¨ nr-zero refl β©
z β‘β¨β©
π + z β‘Λβ¨ +-congΚ³ (Β·-zeroΚ³ (π + p)) β©
(π + p) Β· π + z β‘β¨β©
nr p π z π π β
π π π π n β begin
nrβ² π π π π n β‘β¨ nr-factoring β©
nrββ² π π Β· n + nrβ² π π π π π β‘β¨ +-congΛ‘ {nrββ² π π Β· n} nrβ²-π β©
nrββ² π π Β· n + π β€β¨ +-monotoneΛ‘ (Β·-monotoneΛ‘ (β’πββ€π nrββ’π)) β©
π Β· n + π β‘β¨β©
nr π π π π n β
π β€π π π n β begin
nrβ² π β€π π π n β€β¨ nr-suc β©
π + π Β· n + β€π Β· nrβ² π β€π π π n β‘β¨β©
β€π Β· nrβ² π β€π π π n β‘β¨ Β·-congΛ‘ {β€π} nr-factoring β©
β€π Β· (nrββ² π β€π Β· n + nrβ² π β€π π π π) β‘β¨ Β·-congΛ‘ {β€π} (+-congΛ‘ {nrββ² π β€π Β· n} nrβ²-π) β©
β€π Β· (nrββ² π β€π Β· n + π) β‘β¨ Β·-distribΛ‘-+ β€π (nrββ² π β€π Β· n) π β©
β€π Β· nrββ² π β€π Β· n + π β€β¨ +-monotoneΛ‘ {r = π} (Β·-monotoneΚ³ {r = β€π}
(Β·-monotoneΛ‘ (β’πββ€π nrββ’π))) β©
β€π Β· π Β· n + π β‘β¨ +-congΚ³ {π} (Β·-congΛ‘ {β€π} (Β·-identityΛ‘ n)) β©
β€π Β· n + π β‘β¨β©
nr π β€π π π n β
p β€π z π π β begin
nrβ² p β€π z π π β€β¨ nr-sucβ² β©
π + β€π Β· nrβ² p β€π z π π β€β¨ +-monotoneΚ³ {r = π} (Β·-monotoneΚ³ {r = β€π} (nr-zero refl)) β©
π + β€π Β· z β‘Λβ¨ +-congΚ³ (Β·-zeroΚ³ (β€π + p)) β©
(β€π + p) Β· π + β€π Β· z β‘β¨β©
nr p β€π z π π β
where
open Is-factoring-nr is-factoring-nr renaming (nrβ to nrββ²)
open Has-nr has-nr renaming (nr to nrβ²; nr-positive to nrβ²-positive)
open Addition linear-or-affine-semiring-with-meet
open Meet linear-or-affine-semiring-with-meet
open Multiplication linear-or-affine-semiring-with-meet
open PartialOrder linear-or-affine-semiring-with-meet
open Semiring-with-meet linear-or-affine-semiring-with-meet
hiding (π; π; Ο; _+_; _Β·_; _β§_; _β€_)
open Tools.Reasoning.PartialOrder β€-poset
lemma : nrβ² p r z s n β€ β€Ο β nrβ² p r z s n β€ nr p r z s n
lemma {p} {r} {z} {s} {n} nrβ²β€Ο =
β€-trans nrβ²β€Ο (β€Οβ€ (nr p r z s n))
nr-sucβ² : nrβ² p r z s π β€ s + r Β· nrβ² p r z s π
nr-sucβ² {p} {r} {z} {s} = begin
nrβ² p r z s π β€β¨ nr-suc β©
s + p Β· π + r Β· nrβ² p r z s π β‘β¨ +-congΛ‘ {s} (+-congΚ³ (Β·-zeroΚ³ p)) β©
s + π + r Β· nrβ² p r z s π β‘β¨β©
s + r Β· nrβ² p r z s π β
nrβ²-π : nrβ² p r π π π β‘ π
nrβ²-π = Natrec.nr-π linear-or-affine-semiring-with-meet β¦ has-nr β¦
pnβ‘Οβnrβ²β€ : p Β· n β‘ β€Ο β nrβ² p r z s n β€ nr p r z s n
pnβ‘Οβnrβ²β€ {p} {n} {r} {z} {s} pnβ‘Ο = lemma $ begin
nrβ² p r z s n β€β¨ nr-suc β©
s + p Β· n + r Β· nrβ² p r z s n β‘β¨ +-congΛ‘ {s} (+-congΚ³ pnβ‘Ο) β©
s + β€Ο + r Β· nrβ² p r z s n β‘β¨ +-congΛ‘ {s} (+-zeroΛ‘ (r Β· nrβ² p r z s n)) β©
s + β€Ο β‘β¨ +-zeroΚ³ s β©
β€Ο β
pn,sβ’πβnrβ²β€ : p Β· n β’ π β s β’ π β nrβ² p r z s n β€ nr p r z s n
pn,sβ’πβnrβ²β€ {p} {n} {s} {r} {z} pnβ’π sβ’π = lemma $ begin
nrβ² p r z s n β€β¨ nr-suc β©
s + p Β· n + r Β· nrβ² p r z s n β‘Λβ¨ +-assoc s (p Β· n) (r Β· nrβ² p r z s n) β©
(s + p Β· n) + r Β· nrβ² p r z s n β‘β¨ +-congΚ³ (β’π+β’π sβ’π pnβ’π) β©
β€Ο + r Β· nrβ² p r z s n β‘β¨ +-zeroΛ‘ (r Β· nrβ² p r z s n) β©
β€Ο β
nβ’πβnrβ²β€ : n β’ π β Β¬ (z β‘ π Γ s β‘ π) β nrβ² p r z s n β€ nr p r z s n
nβ’πβnrβ²β€ {n} {z} {s} {p} {r} nβ’π z,sβ’π = lemma $ begin
nrβ² p r z s n β‘β¨ nr-factoring β©
nrββ² p r Β· n + nrβ² p r z s π β‘β¨ β’π+β’π (β’πΒ·β’π nrββ’π nβ’π) (Ξ» nrβ²β‘π β
let zβ‘π , sβ‘π , _ = nrβ²-positive nrβ²β‘π
in z,sβ’π (zβ‘π , sβ‘π)) β©
β€Ο β
nrβ²pΟβ€ : Β¬ (z β‘ π Γ s β‘ π Γ n β‘ π) β nrβ² p β€Ο z s n β€ nr p β€Ο z s n
nrβ²pΟβ€ {z} {s} {n} {p} β’π = lemma $ begin
nrβ² p β€Ο z s n β€β¨ nr-suc β©
s + p Β· n + β€Ο Β· nrβ² p β€Ο z s n β‘β¨ +-congΛ‘ {s} (+-congΛ‘ {p Β· n} (β€ΟΒ·β’π (β’π ββ nrβ²-positive))) β©
s + p Β· n + β€Ο β‘β¨ +-congΛ‘ {s} (+-zeroΚ³ (p Β· n)) β©
s + β€Ο β‘β¨ +-zeroΚ³ s β©
β€Ο β
p,r,nβ’πβnrβ²β€ : p β’ π β r β’ π β n β’ π β nrβ² p r z s n β€ nr p r z s n
p,r,nβ’πβnrβ²β€ {p} {r} {n} {z} {s} pβ’π rβ’π nβ’π = lemma $ begin
nrβ² p r z s n β€β¨ nr-suc β©
s + p Β· n + r Β· nrβ² p r z s n β‘β¨ +-congΛ‘ {s} (β’π+β’π (β’πΒ·β’π pβ’π nβ’π)
(β’πΒ·β’π rβ’π (nβ’π ββ projβ ββ projβ ββ nrβ²-positive))) β©
s + β€Ο β‘β¨ +-zeroΚ³ s β©
β€Ο β
r,sβ’πβnrβ²β€ : r β’ π β s β’ π β nrβ² p r z s n β€ nr p r z s n
r,sβ’πβnrβ²β€ {r} {s} {p} {z} {n} rβ’π sβ’π = lemma $ begin
nrβ² p r z s n β€β¨ nr-suc β©
s + p Β· n + r Β· nrβ² p r z s n β‘β¨ +-congΛ‘ {s} (+-comm (p Β· n) (r Β· nrβ² p r z s n)) β©
s + r Β· nrβ² p r z s n + p Β· n β‘Λβ¨ +-assoc s (r Β· nrβ² p r z s n) (p Β· n) β©
(s + r Β· nrβ² p r z s n) + p Β· n β‘β¨ +-congΚ³ (β’π+β’π sβ’π
(β’πΒ·β’π rβ’π (sβ’π ββ projβ ββ projβ ββ nrβ²-positive))) β©
β€Ο + p Β· n β‘β¨ +-zeroΛ‘ (p Β· n) β©
β€Ο β
opaque
nr-linearity-like-for-π :
Has-nr.Linearity-like-nr-for-π linear-or-affine-has-nr
nr-linearity-like-for-π = refl
opaque
nr-linearity-like-for-π :
Has-nr.Linearity-like-nr-for-π linear-or-affine-has-nr
nr-linearity-like-for-π = refl
Suitable-for-full-reduction :
β variant β
Type-restrictions (linear-or-affine variant) β
Usage-restrictions (linear-or-affine variant) β
Set
Suitable-for-full-reduction variant rs us =
(UnitΛ’-allowed β StarΛ’-sink) Γ
(UnitΚ·-allowed β Β¬ UnitΚ·-Ξ·) Γ
(β p β Β¬ Ξ£Λ’-allowed π p) Γ
(β p β Β¬ Ξ£Λ’-allowed β€π p) Γ
(β p β Β¬ Ξ£Λ’-allowed β€Ο p)
where
open Type-restrictions rs
open Usage-restrictions us
suitable-for-full-reduction :
Type-restrictions (linear-or-affine variant) β
β Ξ» rs β Suitable-for-full-reduction variant rs urs
suitable-for-full-reduction {urs} rs =
record rs
{ Unit-allowed = Ξ» where
π€ β UnitΛ’-allowed Γ StarΛ’-sink
π¨ β UnitΚ·-allowed Γ Β¬ UnitΚ·-Ξ·
; Ξ Ξ£-allowed = Ξ» b p q β
Ξ Ξ£-allowed b p q Γ (b β‘ BMΞ£ π€ β p β‘ π)
; []-cong-allowed = Ξ» where
π€ β β₯
π¨ β []-congΚ·-allowed Γ Β¬ UnitΚ·-Ξ·
; []-congβErased = Ξ» where
{s = π€} ()
{s = π¨} (ok , no-Ξ·) β
case []-congβErased ok of Ξ»
(okβ , okβ) β
(okβ , no-Ξ·) , okβ , (Ξ» ())
; []-congβΒ¬Trivial = Ξ» where
{s = π€} ()
{s = π¨} β []-congβΒ¬Trivial ββ projβ
}
, projβ
, projβ
, (Ξ» _ β ((Ξ» ()) ββ (_$ PE.refl)) ββ projβ)
, (Ξ» _ β ((Ξ» ()) ββ (_$ PE.refl)) ββ projβ)
, (Ξ» _ β ((Ξ» ()) ββ (_$ PE.refl)) ββ projβ)
where
open Type-restrictions rs
open Usage-restrictions urs
full-reduction-assumptions :
Suitable-for-full-reduction variant trs urs β
Full-reduction-assumptions trs urs
full-reduction-assumptions (sink , no-Ξ· , Β¬π , Β¬β€π , Β¬β€Ο) = record
{ sinkβπβ€π = Ξ» where
{s = π€} ok _ β injβ (refl , sink ok)
{s = π¨} _ (injβ ())
{s = π¨} ok (injβ Ξ·) β β₯-elim (no-Ξ· ok Ξ·)
; β‘πβπβ€π = Ξ» where
{p = π} ok β β₯-elim (Β¬π _ ok)
{p = β€π} ok β β₯-elim (Β¬β€π _ ok)
{p = β€Ο} ok β β₯-elim (Β¬β€Ο _ ok)
{p = π} _ β injβ refl
}
full-reduction-assumptions-suitable :
Full-reduction-assumptions trs urs β
Suitable-for-full-reduction variant trs urs
full-reduction-assumptions-suitable {urs = urs} as =
(Ξ» ok β case sinkβπβ€π ok (injβ refl) of Ξ» where
(injβ (_ , sink)) β sink
(injβ ()))
, (Ξ» ok Ξ· β case sinkβπβ€π ok (injβ Ξ·) of Ξ» where
(injβ (() , _))
(injβ ()))
, (Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (_ , _ , ())))
, (Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (() , _)))
, Ξ» p Ξ£-ok β case β‘πβπβ€π Ξ£-ok of Ξ» where
(injβ ())
(injβ (() , _))
where
open Full-reduction-assumptions as
open Usage-restrictions urs
open Subtraction linear-or-affine-semiring-with-meet
opaque
Ο-pβ‘Ο : β p β β€Ο - p β‘ β€Ο
Ο-pβ‘Ο p = β-pβ‘β PE.refl p
opaque
π-πβ‘π : π - π β‘ π
π-πβ‘π =
refl ,
Ξ» where
π _ β refl
π ()
β€π ()
β€Ο ()
opaque
β€π-β€πβ‘π : β€π - β€π β‘ π
β€π-β€πβ‘π =
refl ,
Ξ» where
π _ β refl
π ()
β€π ()
β€Ο ()
opaque
β€π-πβ‘π : β€π - π β‘ π
β€π-πβ‘π =
refl ,
Ξ» where
π _ β refl
π ()
β€π ()
β€Ο ()
opaque
p-Οβ° : p - β€Ο β€ q β p β‘ β€Ο
p-Οβ° {(π)} {(π)} ()
p-Οβ° {(π)} {(π)} ()
p-Οβ° {(π)} {(β€π)} ()
p-Οβ° {(π)} {(β€Ο)} ()
p-Οβ° {(π)} {(π)} ()
p-Οβ° {(π)} {(π)} ()
p-Οβ° {(π)} {(β€π)} ()
p-Οβ° {(π)} {(β€Ο)} ()
p-Οβ° {(β€π)} {(π)} ()
p-Οβ° {(β€π)} {(π)} ()
p-Οβ° {(β€π)} {(β€π)} ()
p-Οβ° {(β€π)} {(β€Ο)} ()
p-Οβ° {(β€Ο)} _ = refl
opaque
p-Οβ’ : p - β€Ο β‘ q β p β‘ β€Ο
p-Οβ’ {q} = p-Οβ° {q = q} ββ projβ
opaque
π-β€πβ° : π - β€π β€ p β β₯
π-β€πβ° {(π)} ()
π-β€πβ° {(π)} ()
π-β€πβ° {(β€π)} ()
π-β€πβ° {(β€Ο)} ()
opaque
π-β€πβ’ : π - β€π β‘ p β β₯
π-β€πβ’ {p} = π-β€πβ° {p} ββ projβ
opaque
supports-subtraction : Supports-subtraction
supports-subtraction {p} {(β€Ο)} {r} x =
case p-Οβ° {q = r} x of Ξ» {
refl β
β€Ο , Ο-pβ‘Ο β€Ο }
supports-subtraction {p} {(π)} {r} x =
p , p-πβ‘p
supports-subtraction {(β€Ο)} {q} _ =
β€Ο , Ο-pβ‘Ο q
supports-subtraction {(π)} {r} x =
case π-pβ€q {q = r} x of Ξ» {
(refl , refl) β
π , p-πβ‘p }
supports-subtraction {(π)} {(π)} _ =
π , p-pβ€π ,
Ξ» where
π _ β refl
π ()
β€π ()
β€Ο ()
supports-subtraction {(β€π)} {(π)} x =
π , β€π-πβ‘π
supports-subtraction {(β€π)} {(β€π)} x =
π , p-pβ€π ,
Ξ» where
π _ β refl
π ()
β€π ()
β€Ο ()
supports-subtraction {(π)} {(β€π)} {r} x =
β₯-elim (π-β€πβ° {p = r} x)
data _-_β‘β²_ : (p q r : Linear-or-affine) β Set where
Ο-pβ‘β²Ο : β€Ο - p β‘β² β€Ο
p-πβ‘β²p : p - π β‘β² p
π-πβ‘β²π : π - π β‘β² π
β€π-β€πβ‘β²π : β€π - β€π β‘β² π
β€π-πβ‘β²π : β€π - π β‘β² π
opaque
-β‘β-β‘β² : β p q r β (p - q β‘ r) β (p - q β‘β² r)
-β‘β-β‘β² p q r = left p q r , right
where
left : β p q r β p - q β‘ r β p - q β‘β² r
left β€Ο q r p-qβ‘r =
case -β‘-functional {q = q} p-qβ‘r (Ο-pβ‘Ο q) of Ξ» {
refl β
Ο-pβ‘β²Ο }
left p π r p-qβ‘r =
case -β‘-functional p-qβ‘r p-πβ‘p of Ξ» {
refl β
p-πβ‘β²p }
left π q r p-qβ‘r =
case π-pβ‘q p-qβ‘r of Ξ» {
(refl , refl) β
p-πβ‘β²p}
left π π r p-qβ‘r =
case -β‘-functional p-qβ‘r π-πβ‘π of Ξ» {
refl β
π-πβ‘β²π }
left β€π β€π r p-qβ‘r =
case -β‘-functional p-qβ‘r β€π-β€πβ‘π of Ξ» {
refl β
β€π-β€πβ‘β²π }
left β€π π r p-qβ‘r =
case -β‘-functional p-qβ‘r β€π-πβ‘π of Ξ» {
refl β
β€π-πβ‘β²π }
left π β€π r p-qβ‘r =
β₯-elim (π-β€πβ’ {r} p-qβ‘r)
left π β€Ο r p-qβ‘r =
case p-Οβ’ p-qβ‘r of Ξ» ()
left β€π β€Ο r p-qβ‘r =
case p-Οβ’ p-qβ‘r of Ξ» ()
right : p - q β‘β² r β p - q β‘ r
right Ο-pβ‘β²Ο = Ο-pβ‘Ο p
right p-πβ‘β²p = p-πβ‘p
right π-πβ‘β²π = π-πβ‘π
right β€π-β€πβ‘β²π = β€π-β€πβ‘π
right β€π-πβ‘β²π = β€π-πβ‘π
opaque
nr-nrα΅’-GLB :
let π = linear-or-affine-semiring-with-meet in
β r β Semiring-with-meet.Greatest-lower-bound
π (nr π r z s π) (Semiring-with-meet.nrα΅’ π r z s)
nr-nrα΅’-GLB = Ξ» where
π β GLB-congΚ³ (sym (trans (β§-congΚ³ (+-congΚ³ (Β·-zeroΚ³ (π β§ π))))
(β§-comm _ _))) nrα΅’-π-GLB
π β lemma-π _ _
β€π β lemma-β€π _ _
β€Ο β lemma-Ο _ _
where
open Semiring-with-meet linear-or-affine-semiring-with-meet
hiding (π; π; Ο; _β§_; _Β·_; _+_)
open GLB linear-or-affine-semiring-with-meet
open Natrec linear-or-affine-semiring-with-meet
open PartialOrder linear-or-affine-semiring-with-meet
lemmaβ² : β {z} i β nrα΅’ π z π i β‘ z
lemmaβ² 0 = refl
lemmaβ² (1+ i) = trans (Β·-identityΛ‘ _) (lemmaβ² i)
lemma : β {r z s} i β
nrα΅’ r z s i β‘ β€Ο β Greatest-lower-bound β€Ο (nrα΅’ r z s)
lemma {r} {z} {s} i nrα΅’β‘Ο =
(Ξ» i β β€Οβ€ (nrα΅’ r z s i)) , Ξ» q qβ€ β β€-trans (qβ€ i) (β€-reflexive nrα΅’β‘Ο)
lemma-π : β z s β Greatest-lower-bound (β€Ο Β· s + z) (nrα΅’ π z s)
lemma-π π π = GLB-nrα΅’-π
lemma-π π π = lemma 2 refl
lemma-π π β€π = lemma 2 refl
lemma-π π β€Ο = lemma 1 refl
lemma-π π π = GLB-const lemmaβ²
lemma-π π π = lemma 1 refl
lemma-π π β€π = lemma 1 refl
lemma-π π β€Ο = lemma 1 refl
lemma-π β€π π = GLB-const lemmaβ²
lemma-π β€π π = lemma 1 refl
lemma-π β€π β€π = lemma 1 refl
lemma-π β€π β€Ο = lemma 1 refl
lemma-π β€Ο π = lemma 0 refl
lemma-π β€Ο π = lemma 0 refl
lemma-π β€Ο β€π = lemma 0 refl
lemma-π β€Ο β€Ο = lemma 0 refl
lemma-β€π : β z s β Greatest-lower-bound (β€Ο Β· s + β€π Β· z) (nrα΅’ β€π z s)
lemma-β€π π π = GLB-nrα΅’-π
lemma-β€π π π = lemma 2 refl
lemma-β€π π β€π = lemma 2 refl
lemma-β€π π β€Ο = lemma 1 refl
lemma-β€π π π =
(Ξ» { 0 β refl
; (1+ i) β β€-reflexive (lem i)}) ,
Ξ» { π qβ€ β case qβ€ 0 of Ξ» ()
; π qβ€ β case qβ€ 1 of Ξ» ()
; β€π qβ€ β refl
; β€Ο qβ€ β refl}
where
lem : β i β β€π β‘ nrα΅’ β€π π π (1+ i)
lem 0 = refl
lem (1+ i) = Β·-congΛ‘ {x = β€π} (lem i)
lemma-β€π π π = lemma 1 refl
lemma-β€π π β€π = lemma 1 refl
lemma-β€π π β€Ο = lemma 1 refl
lemma-β€π β€π π = GLB-const lem
where
lem : β i β nrα΅’ β€π β€π π i β‘ β€π
lem 0 = refl
lem (1+ i) = Β·-congΛ‘ {x = β€π} (lem i)
lemma-β€π β€π π = lemma 1 refl
lemma-β€π β€π β€π = lemma 1 refl
lemma-β€π β€π β€Ο = lemma 1 refl
lemma-β€π β€Ο π = lemma 0 refl
lemma-β€π β€Ο π = lemma 0 refl
lemma-β€π β€Ο β€π = lemma 0 refl
lemma-β€π β€Ο β€Ο = lemma 0 refl
lemma-Ο : β z s β Greatest-lower-bound (β€Ο Β· (s + z)) (nrα΅’ β€Ο z s)
lemma-Ο π π = GLB-nrα΅’-π
lemma-Ο π π = lemma 1 refl
lemma-Ο β€π π = lemma 1 refl
lemma-Ο β€Ο π = lemma 0 refl
lemma-Ο π π = lemma 2 refl
lemma-Ο π π = lemma 1 refl
lemma-Ο β€π π = lemma 1 refl
lemma-Ο β€Ο π = lemma 0 refl
lemma-Ο π β€π = lemma 2 refl
lemma-Ο π β€π = lemma 1 refl
lemma-Ο β€π β€π = lemma 1 refl
lemma-Ο β€Ο β€π = lemma 0 refl
lemma-Ο π β€Ο = lemma 1 refl
lemma-Ο π β€Ο = lemma 1 refl
lemma-Ο β€π β€Ο = lemma 1 refl
lemma-Ο β€Ο β€Ο = lemma 0 refl
opaque
nrα΅’-GLB :
let π = linear-or-affine-semiring-with-meet in
β r z s β β Ξ» p β
Semiring-with-meet.Greatest-lower-bound
π p (Semiring-with-meet.nrα΅’ π r z s)
nrα΅’-GLB r z s = _ , nr-nrα΅’-GLB r
opaque
linear-or-affine-supports-glb-for-natrec :
Has-well-behaved-GLBs linear-or-affine-semiring-with-meet
linear-or-affine-supports-glb-for-natrec = record
{ +-GLBΛ‘ = Ξ» {_} {_} {q} β +-GLBΛ‘ {q = q}
; Β·-GLBΛ‘ = Ξ» {_} {_} {q} β Β·-GLBΛ‘ {q = q}
; Β·-GLBΚ³ = commβ§Β·-GLBΛ‘βΒ·-GLBΚ³ Β·-comm (Ξ» {_} {_} {q} β Β·-GLBΛ‘ {q = q})
; +nrα΅’-GLB = +nrα΅’-GLB
}
where
open Semiring-with-meet linear-or-affine-semiring-with-meet
hiding (π; π; Ο; _+_; _Β·_; _β§_; _β€_)
open GLB linear-or-affine-semiring-with-meet
open Multiplication linear-or-affine-semiring-with-meet
open PartialOrder linear-or-affine-semiring-with-meet
Β·-GLBΛ‘ :
{pα΅’ : Sequence Linear-or-affine} β
Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (q Β· p) (Ξ» i β q Β· pα΅’ i)
Β·-GLBΛ‘ {q = π} p-glb = GLB-constβ²
Β·-GLBΛ‘ {q = π} p-glb =
GLB-cong (sym (Β·-identityΛ‘ _))
(Ξ» _ β sym (Β·-identityΛ‘ _))
p-glb
Β·-GLBΛ‘ {q = β€π} {pα΅’} p-glb = lemma _ p-glb
where
lemmaβ² : π β€ β€π Β· p β p β‘ π
lemmaβ² {(π)} _ = refl
lemmaβ² {(π)} ()
lemmaβ² {(β€π)} ()
lemmaβ² {(β€Ο)} ()
lemmaβ³ : β p β π β€ β€π Β· p β β₯
lemmaβ³ π ()
lemmaβ³ π ()
lemmaβ³ β€π ()
lemmaβ³ β€Ο ()
lemmaβ΄ : β€π β€ β€π Β· p β β€π β€ p
lemmaβ΄ {(π)} _ = refl
lemmaβ΄ {(π)} _ = refl
lemmaβ΄ {(β€π)} _ = refl
lemmaβ΄ {(β€Ο)} ()
lemmaβ : Greatest-lower-bound β€Ο pα΅’ β (β i β β€π β€ pα΅’ i) β β₯
lemmaβ Ο-glb β€pα΅’ = case Ο-glb .projβ β€π β€pα΅’ of Ξ» ()
lemma :
β p β Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (β€π Β· p) (Ξ» i β β€π Β· pα΅’ i)
lemma π p-glb =
GLB-const (Ξ» i β Β·-congΛ‘ {x = β€π} (π-GLB-inv p-glb i))
lemma π p-glb =
(Ξ» i β Β·-monotoneΚ³ {r = β€π} (p-glb .projβ i))
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β refl
; β€Ο qβ€ β refl}
lemma β€π p-glb =
(Ξ» i β Β·-monotoneΚ³ {r = β€π} (p-glb .projβ i))
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β refl
; β€Ο qβ€ β refl}
lemma β€Ο p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β β₯-elim (lemmaβ p-glb (Ξ» i β lemmaβ΄ (qβ€ i)))
; β€Ο qβ€ β refl}
Β·-GLBΛ‘ {q = β€Ο} {pα΅’} p-glb = lemma _ p-glb
where
lemmaβ² : π β€ β€Ο Β· p β p β‘ π
lemmaβ² {(π)} _ = refl
lemmaβ² {(π)} ()
lemmaβ² {(β€π)} ()
lemmaβ² {(β€Ο)} ()
lemmaβ³ : β p β π β€ β€Ο Β· p β β₯
lemmaβ³ π ()
lemmaβ³ π ()
lemmaβ³ β€π ()
lemmaβ³ β€Ο ()
lemmaβ΄ : β€π β€ β€Ο Β· p β p β‘ π
lemmaβ΄ {(π)} _ = refl
lemmaβ΄ {(π)} ()
lemmaβ΄ {(β€π)} ()
lemmaβ΄ {(β€Ο)} ()
lemma :
β p β Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (β€Ο Β· p) (Ξ» i β β€Ο Β· pα΅’ i)
lemma π p-glb =
GLB-const (Ξ» i β Β·-congΛ‘ {x = β€Ο} (π-GLB-inv p-glb i))
lemma π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ΄ ββ qβ€))
; β€Ο qβ€ β refl}
lemma β€π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ΄ ββ qβ€))
; β€Ο qβ€ β refl}
lemma β€Ο p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² ββ qβ€))
; π qβ€ β β₯-elim (lemmaβ³ (pα΅’ 0) (qβ€ 0))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ΄ ββ qβ€))
; β€Ο qβ€ β refl}
+-GLBΛ‘ :
{pα΅’ : Sequence Linear-or-affine} β
Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (q + p) (Ξ» i β q + pα΅’ i)
+-GLBΛ‘ {q = π} p-glb = p-glb
+-GLBΛ‘ {q = π} {pα΅’} p-glb = lemma _ p-glb
where
lemmaβ² : β p q β q β’ β€Ο β q β€ π + p β p β‘ π
lemmaβ² π π _ _ = refl
lemmaβ² π π _ _ = refl
lemmaβ² π β€π _ _ = refl
lemmaβ² p β€Ο qβ’Ο _ = β₯-elim (qβ’Ο refl)
lemmaβ² π π qβ’Ο ()
lemmaβ² π π qβ’Ο ()
lemmaβ² π β€π qβ’Ο ()
lemmaβ² β€π π qβ’Ο ()
lemmaβ² β€π π qβ’Ο ()
lemmaβ² β€π β€π qβ’Ο ()
lemmaβ² β€Ο π qβ’Ο ()
lemmaβ² β€Ο π qβ’Ο ()
lemmaβ² β€Ο β€π qβ’Ο ()
lemma :
β p β Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (π + p) (Ξ» i β π + pα΅’ i)
lemma π p-glb =
GLB-const (Ξ» i β +-congΛ‘ {x = π} (π-GLB-inv p-glb i))
lemma π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl}
lemma β€π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl}
lemma β€Ο p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl}
+-GLBΛ‘ {q = β€π} {pα΅’} p-glb = lemma _ p-glb
where
lemma :
β p β Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (β€π + p) (Ξ» i β β€π + pα΅’ i)
lemmaβ² : β p q β q β’ β€Ο β q β€ β€π + p β p β‘ π
lemmaβ² π _ _ _ = refl
lemmaβ² _ β€Ο qβ’Ο _ = β₯-elim (qβ’Ο refl)
lemmaβ² π π _ ()
lemmaβ² π π _ ()
lemmaβ² π β€π _ ()
lemmaβ² β€π π _ ()
lemmaβ² β€π π _ ()
lemmaβ² β€π β€π _ ()
lemmaβ² β€Ο π _ ()
lemmaβ² β€Ο π _ ()
lemmaβ² β€Ο β€π _ ()
lemma π p-glb =
GLB-const (Ξ» i β +-congΛ‘ {x = β€π} (π-GLB-inv p-glb i))
lemma π p-glb =
(Ξ» _ β refl)
, (Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl})
lemma β€π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl}
lemma β€Ο p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€π qβ€ β β₯-elim (β’p-GLB-inv (Ξ» ()) p-glb (lemmaβ² _ _ (Ξ» ()) ββ qβ€))
; β€Ο qβ€ β refl}
+-GLBΛ‘ {q = β€Ο} {pα΅’} p-glb = lemma _ p-glb
where
lemmaβ² : β p q β q β’ β€Ο β q β€ β€Ο + p β β₯
lemmaβ² p π qβ’Ο x rewrite β€Ο+ p = case x of Ξ» ()
lemmaβ² p π qβ’Ο x rewrite β€Ο+ p = case x of Ξ» ()
lemmaβ² p β€π qβ’Ο x rewrite β€Ο+ p = case x of Ξ» ()
lemmaβ² p β€Ο qβ’Ο _ = qβ’Ο refl
lemma :
β p β Greatest-lower-bound p pα΅’ β
Greatest-lower-bound (β€Ο + p) (Ξ» i β β€Ο + pα΅’ i)
lemma π p-glb =
GLB-const (Ξ» i β +-congΛ‘ {x = β€Ο} (π-GLB-inv p-glb i))
lemma π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€Ο qβ€ β refl}
lemma β€π p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€Ο qβ€ β refl}
lemma β€Ο p-glb =
(Ξ» _ β refl)
, Ξ» { π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€π qβ€ β β₯-elim (lemmaβ² (pα΅’ 0) _ (Ξ» ()) (qβ€ 0))
; β€Ο qβ€ β refl}
open Tools.Reasoning.PartialOrder β€-poset
+nrα΅’-GLB :
β {pβ pβ} β
Greatest-lower-bound pβ (nrα΅’ r zβ sβ) β
Greatest-lower-bound pβ (nrα΅’ r zβ sβ) β
β Ξ» q β Greatest-lower-bound q (nrα΅’ r (zβ + zβ) (sβ + sβ)) Γ
pβ + pβ β€ q
+nrα΅’-GLB {r} {zβ} {sβ} {zβ} {sβ} {pβ} {pβ} pβ-glb pβ-glb =
_ , nr-nrα΅’-GLB r , (begin
pβ + pβ β‘β¨ +-cong (GLB-unique pβ-glb (nr-nrα΅’-GLB r))
(GLB-unique pβ-glb (nr-nrα΅’-GLB r)) β©
nr π r zβ sβ π + nr π r zβ sβ π β€β¨ Has-nr.nr-+ linear-or-affine-has-nr {π} {r} β©
nr π r (zβ + zβ) (sβ + sβ) π β)