module Graded.Modality.Instances.Linear-or-affine where
import Tools.Algebra
open import Tools.Bool using (T)
open import Tools.Empty
open import Tools.Function
open import Tools.Level
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β)
open import Tools.Unit
import Graded.Modality
open import Graded.FullReduction.Assumptions
import Graded.Modality.Properties.Addition as Addition
import Graded.Modality.Properties.Meet as Meet
import Graded.Modality.Properties.Multiplication as Multiplication
import Graded.Modality.Properties.PartialOrder as PartialOrder
import Graded.Modality.Properties.Star as Star
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 40 _β§_
_β§_ : 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 β p β‘ π
π-maximal {p = π} 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
+β‘π : 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 = π} _ = refl , refl
β§β‘π {p = π} {q = π} ()
β§β‘π {p = π} {q = β€π} ()
β§β‘π {p = π} {q = β€Ο} ()
Β·-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
β€ΟΒ·β’π : β 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
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
; +-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
; β§-positiveΛ‘ = Ξ» where
{p = π} {q = π} _ β refl
{p = π} {q = π} _ β refl
{p = π} {q = β€π} ()
{p = π} {q = β€Ο} ()
}
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 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) β
bad-linear-or-affine : Modality-variant β Modality
bad-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
; has-nr = Ξ» _ β
Star.has-nr _
β¦ has-star = 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-π = Ξ» {p = _} {r = r} β nr-π r .projβ (refl , refl , refl)
; 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
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
; has-nr = Ξ» _ β linear-or-affine-has-nr
}
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 = π¨} (ok , no-Ξ·) β
case []-congβErased ok of Ξ»
(okβ , okβ) β
(okβ , no-Ξ·) , okβ , (Ξ» ())
; []-congβΒ¬Trivial = Ξ» where
{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