Todd Waugh Ambridge, January 2024

# Verification of signed-digit operations

\begin{code}
{-# OPTIONS --without-K --safe #-}

open import MLTT.Spartan
open import UF.FunExt

open import TWA.Thesis.Chapter2.Sequences
open import TWA.Thesis.Chapter5.SignedDigit
open import TWA.Thesis.Chapter5.IntervalObject hiding (⟨_⟩)

module TWA.Thesis.Chapter5.SignedDigitIntervalObject
 {𝓦 : Universe}
 (fe : FunExt)
 (io : Interval-object fe 𝓦)
 where

open import TWA.Thesis.Chapter5.IntervalObjectApproximation fe io
open basic-interval-object-development fe io hiding (βˆ’1 ; O ; +1)
\end{code}

## Representation map

\begin{code}
⟨_⟩ : πŸ› β†’ 𝕀
⟨ βˆ’1 ⟩ = u
⟨  O ⟩ = u βŠ• v
⟨ +1 ⟩ = v

βŸͺ_⟫ : πŸ›α΄Ί β†’ 𝕀
βŸͺ Ξ± ⟫ = M (map ⟨_⟩ Ξ±)

_realisesΒΉ_ : (πŸ›α΄Ί β†’ πŸ›α΄Ί) β†’ (𝕀 β†’ 𝕀) β†’ 𝓦  Μ‡
f realisesΒΉ f' = (Ξ± : πŸ›α΄Ί) β†’ f' βŸͺ Ξ± ⟫ ＝ βŸͺ f Ξ± ⟫

_realisesΒ²_ : (πŸ›α΄Ί β†’ πŸ›α΄Ί β†’ πŸ›α΄Ί) β†’ (𝕀 β†’ 𝕀 β†’ 𝕀) β†’ 𝓦 Μ‡
f realisesΒ² f' = (Ξ± Ξ² : πŸ›α΄Ί) β†’ βŸͺ f Ξ± Ξ² ⟫ ＝ f' βŸͺ Ξ± ⟫ βŸͺ Ξ² ⟫

_pw-realisesΒΉ_ : (πŸ› β†’ πŸ›) β†’ (𝕀 β†’ 𝕀) β†’ 𝓦 Μ‡
f pw-realisesΒΉ f' = (a : πŸ›) β†’ f' ⟨ a ⟩ ＝ ⟨ f a ⟩

_pw-realisesΒ²_ : (πŸ› β†’ πŸ› β†’ πŸ›) β†’ (𝕀 β†’ 𝕀 β†’ 𝕀) β†’ 𝓦 Μ‡
f pw-realisesΒ² f' = (a b : πŸ›) β†’ f' ⟨ a ⟩ ⟨ b ⟩ ＝ ⟨ f a b ⟩

_realises'_ : (πŸ› β†’ πŸ›α΄Ί β†’ πŸ›α΄Ί) β†’ (𝕀 β†’ 𝕀 β†’ 𝕀) β†’ 𝓦 Μ‡
f realises' f' = (a : πŸ›) (Ξ² : πŸ›α΄Ί) β†’ βŸͺ f a Ξ² ⟫ ＝ f' ⟨ a ⟩ βŸͺ Ξ² ⟫

id-realiser : id realisesΒΉ id
id-realiser Ξ± = refl

∘-realiser : {f g : πŸ›α΄Ί β†’ πŸ›α΄Ί} {f' g' : 𝕀 β†’ 𝕀}
           β†’ f realisesΒΉ f'
           β†’ g realisesΒΉ g'
           β†’ (f ∘ g) realisesΒΉ (f' ∘ g')
∘-realiser {f} {g} {f'} {g'} fβ†’ gβ†’ Ξ±
 = ap f' (gβ†’ Ξ±) βˆ™ fβ†’ (g Ξ±)

map-realiser : (f : πŸ› β†’ πŸ›) (f' : 𝕀 β†’ 𝕀)
             β†’ f pw-realisesΒΉ f'
             β†’ is-βŠ•-homomorphism fe π“˜ π“˜ f'
             β†’ (map f) realisesΒΉ f'
map-realiser f f' fβ†’ fβŠ• Ξ± = βŠ•-homs-are-M-homs f' fβŠ• (map ⟨_⟩ Ξ±)
                          βˆ™ ap M (dfunext (fe 𝓀₀ 𝓦) (Ξ» i β†’ fβ†’ (Ξ± i)))

map-realiserΒ² : (f : πŸ› β†’ πŸ›α΄Ί β†’ πŸ›α΄Ί) (f' : 𝕀 β†’ 𝕀 β†’ 𝕀)
              β†’ f realises' f'
              β†’ ((a : πŸ›) β†’ is-βŠ•-homomorphism fe π“˜ π“˜ (f' ⟨ a ⟩))
              β†’ (Ξ± Ξ² : πŸ›α΄Ί)
              β†’ M (map βŸͺ_⟫ (zipWith f Ξ± (repeat Ξ²)))
              ＝ M (Ξ» n β†’ f' ⟨ Ξ± n ⟩ βŸͺ Ξ² ⟫)
map-realiserΒ² f f' fβ†’ fβŠ• Ξ± Ξ²
 = ap M (dfunext (fe 𝓀₀ 𝓦) (Ξ» i β†’ fβ†’ (Ξ± i) Ξ²))
\end{code}

## Negation

\begin{code}
flip-realiser : flip pw-realisesΒΉ βˆ’_
flip-realiser βˆ’1 = βˆ’1-inverse
flip-realiser  O =  O-inverse
flip-realiser +1 = +1-inverse

neg-realiser : neg realisesΒΉ βˆ’_
neg-realiser
 = map-realiser flip βˆ’_ flip-realiser βˆ’-is-βŠ•-homomorphism
\end{code}

## Binary midpoint

\begin{code}
half : 𝟝 β†’ 𝕀
half βˆ’2 = u
half βˆ’1 = u /2
half  O = u βŠ• v
half +1 = v /2
half +2 = v

βŠ•-hom-l : {a b c : 𝕀} β†’ a βŠ• (b βŠ• c) ＝ (a βŠ• b) βŠ• (a βŠ• c)
βŠ•-hom-l {a} {b} {c} = βŠ•-is-βŠ•-homomorphism-r fe π“˜ a b c

βŠ•-idem' = Ξ» {a}             β†’ βŠ•-idem a
βŠ•-comm' = Ξ» {a} {b}         β†’ βŠ•-comm a b
βŠ•-tran' = Ξ» {a} {b} {c} {d} β†’ βŠ•-tran a b c d 
βŠ•-canc' = Ξ» {a} {b} {c}     β†’ βŠ•-canc a b c 

div2-aux-＝ : (x y : 𝟝) (z : 𝕀) β†’ let (a , b) = div2-aux x y in
             ⟨ a ⟩ βŠ• (half b βŠ• z) ＝ (half x βŠ• (half y βŠ• z))
div2-aux-＝ βˆ’2 y z = refl
div2-aux-＝ βˆ’1 βˆ’2 z = ap (_βŠ• ((u βŠ• v) βŠ• z)) βŠ•-idem' ⁻¹ βˆ™ βŠ•-tran'
div2-aux-＝ βˆ’1 βˆ’1 z = ap (_βŠ• ((v βŠ• (u βŠ• v)) βŠ• z)) (βŠ•-idem' ⁻¹ βˆ™ βŠ•-idem' ⁻¹)
                   βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• ((u βŠ• u) βŠ• z)) βŠ•-tran'
                   βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• ((u βŠ• (u βŠ• v)) βŠ• z))
                                (βŠ•-comm' βˆ™ ap (_βŠ• (u βŠ• v)) βŠ•-idem')
div2-aux-＝ βˆ’1  O z = ap (_βŠ• (u βŠ• z)) βŠ•-idem' ⁻¹ βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• ((u βŠ• v) βŠ• z)) βŠ•-comm'
div2-aux-＝ βˆ’1 +1 z = ap (_βŠ• ((u βŠ• (u βŠ• v)) βŠ• z))
                       (βŠ•-comm' βˆ™ ap (_βŠ• u) βŠ•-idem' ⁻¹)
                   βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• (u βŠ• z)) βŠ•-tran' βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• ((v βŠ• (u βŠ• v)) βŠ• z))
                       (βŠ•-comm' βˆ™ ap (u βŠ•_) βŠ•-comm')
div2-aux-＝ βˆ’1 +2 z = βŠ•-tran'
div2-aux-＝  O  y z = refl
div2-aux-＝ +1 βˆ’2 z = ap (_βŠ• ((u βŠ• v) βŠ• z)) βŠ•-comm' βˆ™ βŠ•-tran'
div2-aux-＝ +1 βˆ’1 z = ap (Ξ» - β†’ ((- βŠ• v) βŠ• ((v βŠ• (u βŠ• v)) βŠ• z))) βŠ•-idem' ⁻¹
                          βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• (v βŠ• z)) βŠ•-tran'
                          βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• ((u βŠ• (u βŠ• v)) βŠ• z)) βŠ•-comm'
div2-aux-＝ +1  O z = ap (_βŠ• (v βŠ• z)) βŠ•-idem' ⁻¹ βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• ((u βŠ• v) βŠ• z)) βŠ•-comm'
div2-aux-＝ +1 +1 z = ap (_βŠ• ((u βŠ• (u βŠ• v)) βŠ• z)) (βŠ•-idem' ⁻¹ βˆ™ βŠ•-idem' ⁻¹)
                   βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• ((v βŠ• v) βŠ• z)) βŠ•-tran' βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• ((v βŠ• (u βŠ• v)) βŠ• z))
                        (βŠ•-comm' βˆ™ ap (_βŠ• (v βŠ• u)) βŠ•-idem' βˆ™ ap (v βŠ•_) βŠ•-comm')
div2-aux-＝ +1 +2 z = ap (_βŠ• ((u βŠ• v) βŠ• z)) βŠ•-idem' ⁻¹ βˆ™ βŠ•-tran'
div2-aux-＝ +2 y z = refl

div2-approx' : Π (fg-n-approx' (map ⟨_⟩ ∘ div2) (map half))
div2-approx' n f Ξ±
 = (z , w)
 , (ap ((map ⟨_⟩ ∘ div2) Ξ± 0 βŠ•_) (prβ‚‚ IH)
 βˆ™ div2-aux-＝ (Ξ± 0) (Ξ± 1)
     (m (append-one w ((first- n) (tail (map half (b ∷ x)))))))
 where
  b = prβ‚‚ (div2-aux (Ξ± 0) (Ξ± 1))
  x = tail (tail Ξ±)
  IH = f (b ∷ x)
  z w : 𝕀
  z = pr₁ (pr₁ IH)
  w = prβ‚‚ (pr₁ IH)

div2-realiser : (Ξ± : 𝟝ᴺ) β†’ βŸͺ div2 Ξ± ⟫ ＝ M (map half Ξ±)
div2-realiser = fg-approx-holds (map ⟨_⟩ ∘ div2) (map half) div2-approx'

half-add-realiser : (Ξ± Ξ² : πŸ›α΄Ί) β†’ M (map half (add2 Ξ± Ξ²)) ＝ (βŸͺ Ξ± ⟫ βŠ• βŸͺ Ξ² ⟫)
half-add-realiser Ξ± Ξ² = ap M (dfunext (fe 𝓀₀ 𝓦) (Ξ» i β†’ Ξ³ (Ξ± i) (Ξ² i)))
                      βˆ™ M-hom (map ⟨_⟩ Ξ±) (map ⟨_⟩ Ξ²) ⁻¹
 where
  Ξ³ : (a b : πŸ›) β†’ half (a +πŸ› b) ＝ (⟨ a ⟩ βŠ• ⟨ b ⟩)
  Ξ³ βˆ’1 βˆ’1 = βŠ•-idem' ⁻¹
  Ξ³ βˆ’1  O = refl
  Ξ³ βˆ’1 +1 = refl
  Ξ³  O βˆ’1 = βŠ•-comm'
  Ξ³  O  O = βŠ•-idem' ⁻¹
  Ξ³  O +1 = βŠ•-comm'
  Ξ³ +1 βˆ’1 = βŠ•-comm'
  Ξ³ +1  O = refl
  Ξ³ +1 +1 = βŠ•-idem' ⁻¹

mid-realiser : mid realisesΒ² _βŠ•_
mid-realiser Ξ± Ξ² = div2-realiser (add2 Ξ± Ξ²)
                 βˆ™ half-add-realiser Ξ± Ξ²
\end{code}

## Infinitary midpoint

\begin{code}
quarter : 𝟑 β†’ 𝕀
quarter βˆ’4 = u
quarter βˆ’3 = u βŠ• (u βŠ• (u βŠ• v))
quarter βˆ’2 = u βŠ• (u βŠ• v)
quarter βˆ’1 = u βŠ• (v βŠ• (u βŠ• v))
quarter  O = u βŠ• v
quarter +1 = v βŠ• (u βŠ• (u βŠ• v))
quarter +2 = v βŠ• (u βŠ• v)
quarter +3 = v βŠ• (v βŠ• (u βŠ• v))
quarter +4 = v

l : {a b c : 𝕀} β†’ a ＝ b β†’ (a βŠ• c) ＝ (b βŠ• c)
l refl = refl

r : {a b c : 𝕀} β†’ b ＝ c β†’ (a βŠ• b) ＝ (a βŠ• c)
r refl = refl

div4-aux-＝ : (x y : 𝟑) (z : 𝕀)
            β†’ let (a , b) = div4-aux x y in
              ⟨ a ⟩ βŠ• (quarter b βŠ• z)
            ＝ (quarter x βŠ• (quarter y βŠ• z))
div4-aux-＝ βˆ’4  y z = refl
div4-aux-＝ βˆ’3 βˆ’4 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
div4-aux-＝ βˆ’3 βˆ’3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹
         βˆ™ βŠ•-comm')
      βˆ™ βŠ•-tran')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3 βˆ’2 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3 βˆ’1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran'
     βˆ™ l βŠ•-comm')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3  O z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (r βŠ•-comm'
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3 +1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3 +2 z
 = l (βŠ•-idem' ⁻¹
   βˆ™ r (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’3 +3 z
 = l (βŠ•-idem' ⁻¹
   βˆ™ r (βŠ•-idem' ⁻¹
     βˆ™ r (βŠ•-idem' ⁻¹))
   βˆ™ r βŠ•-tran'
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-idem'
div4-aux-＝ βˆ’3 +4 z
 = βŠ•-tran'
div4-aux-＝ βˆ’2 βˆ’4 z = div2-aux-＝ βˆ’1 βˆ’2 z
div4-aux-＝ βˆ’2 βˆ’3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’2 βˆ’2 z = div2-aux-＝ βˆ’1 βˆ’1 z
div4-aux-＝ βˆ’2 βˆ’1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’2 O z  = div2-aux-＝ βˆ’1  O z
div4-aux-＝ βˆ’2 +1 z
 = r βŠ•-comm' βˆ™ βŠ•-tran'
 βˆ™ r (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran' βˆ™ l βŠ•-comm')
 βˆ™ βŠ•-tran' βˆ™ r βŠ•-comm'
div4-aux-＝ βˆ’2 +2 z = div2-aux-＝ βˆ’1 +1 z
div4-aux-＝ βˆ’2 +3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (βŠ•-tran'
   βˆ™ l βŠ•-idem')
 βˆ™ βŠ•-tran'
div4-aux-＝ βˆ’2 +4 z = div2-aux-＝ βˆ’1 +2 z
div4-aux-＝ βˆ’1 βˆ’4 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
div4-aux-＝ βˆ’1 βˆ’3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ l βŠ•-comm'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 βˆ’2 z
 = l (βŠ•-idem' ⁻¹
   βˆ™ l βŠ•-comm'
   βˆ™ r (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 βˆ’1 z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran'
     βˆ™ l βŠ•-comm')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 O z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
    βˆ™ r βŠ•-comm'
   βˆ™ βŠ•-tran'
   βˆ™ r βŠ•-comm')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 +1 z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹)
      βˆ™ βŠ•-tran')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 +2 z
 = r βŠ•-comm' βˆ™ βŠ•-tran'
 βˆ™ r (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ r βŠ•-comm'
div4-aux-＝ βˆ’1 +3 z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹
         βˆ™ βŠ•-comm')
      βˆ™ βŠ•-tran'
      βˆ™ l βŠ•-comm'
      βˆ™ βŠ•-tran')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ βˆ’1 +4 z = βŠ•-tran'
div4-aux-＝  O  y z = refl 
div4-aux-＝ +1 βˆ’4 z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
div4-aux-＝ +1 βˆ’3 z
 = βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ l βŠ•-comm'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 βˆ’2 z
 = βŠ•-tran'
 βˆ™ l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 βˆ’1 z
 = βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹)
      βˆ™ βŠ•-tran'
      βˆ™ l βŠ•-comm')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 O z
 = βŠ•-tran'
 βˆ™ l (r βŠ•-comm'
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 +1 z
 = βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 +2 z
 = βŠ•-tran'
 βˆ™ l (βŠ•-idem' ⁻¹
   βˆ™ r (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 +3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ l βŠ•-comm'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran'
     βˆ™ l βŠ•-comm')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +1 +4 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
div4-aux-＝ +2 βˆ’4 z = div2-aux-＝ +1 βˆ’2 z
div4-aux-＝ +2 βˆ’3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l βŠ•-comm'
   βˆ™ βŠ•-tran'
   βˆ™ l βŠ•-idem')
 βˆ™ βŠ•-tran'
div4-aux-＝ +2 βˆ’2 z = div2-aux-＝ +1 βˆ’1 z
div4-aux-＝ +2 βˆ’1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l βŠ•-comm'
   βˆ™ βŠ•-tran'
   βˆ™ l βŠ•-idem')
 βˆ™ βŠ•-tran'
div4-aux-＝ +2 O z = div2-aux-＝ +1 O z
div4-aux-＝ +2 +1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
 βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +2 +2 z = div2-aux-＝ +1 +1 z
div4-aux-＝ +2 +3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
 βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +2 +4 z = div2-aux-＝ +1 +2 z
div4-aux-＝ +3 βˆ’4 z
 = l βŠ•-comm'
 βˆ™ βŠ•-tran'
div4-aux-＝ +3 βˆ’3 z
 = l (βŠ•-idem' ⁻¹
   βˆ™ l βŠ•-comm'
   βˆ™ r (βŠ•-idem' ⁻¹
     βˆ™ l βŠ•-comm'
     βˆ™ r (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-idem'
div4-aux-＝ +3 βˆ’2 z
 = l (βŠ•-idem' ⁻¹
   βˆ™ l βŠ•-comm'
   βˆ™ r (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3 βˆ’1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran'
   βˆ™ r (l (βŠ•-idem' ⁻¹)
     βˆ™ βŠ•-tran'
     βˆ™ l βŠ•-comm')
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3  O z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (l (βŠ•-idem' ⁻¹)
   βˆ™ r βŠ•-comm'
   βˆ™ βŠ•-tran'
   βˆ™ r βŠ•-comm')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3 +1 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹)
      βˆ™ βŠ•-tran')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3 +2 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3 +3 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
 βˆ™ l (r (l (βŠ•-idem' ⁻¹)
      βˆ™ βŠ•-tran'
      βˆ™ l βŠ•-comm')
   βˆ™ l (βŠ•-idem' ⁻¹)
   βˆ™ βŠ•-tran')
 βˆ™ βŠ•-tran'
 βˆ™ l βŠ•-comm'
div4-aux-＝ +3 +4 z
 = l (βŠ•-idem' ⁻¹)
 βˆ™ βŠ•-tran'
div4-aux-＝ +4  y z = refl

div4-approx' : Π (fg-n-approx' (map ⟨_⟩ ∘ div4) (map quarter))
div4-approx' n f Ξ±
 = (z , w)
 , (ap ((map ⟨_⟩ ∘ div4) Ξ± 0 βŠ•_) (prβ‚‚ IH)
 βˆ™ div4-aux-＝ (Ξ± 0) (Ξ± 1)
     (m (append-one w ((first- n) (tail (map quarter (b ∷ x)))))))
 where
  b = prβ‚‚ (div4-aux (Ξ± 0) (Ξ± 1))
  x = tail (tail Ξ±)
  IH = f (b ∷ x)
  z w : 𝕀
  z = pr₁ (pr₁ IH)
  w = prβ‚‚ (pr₁ IH)

quarter-realiser : (Ξ± : 𝟑ᴺ) β†’ βŸͺ div4 Ξ± ⟫ ＝ M (map quarter Ξ±)
quarter-realiser = fg-approx-holds (map ⟨_⟩ ∘ div4) (map quarter)
                     div4-approx'

βŸͺβŸͺ_⟫⟫ : 𝟑ᴺ β†’ 𝕀
βŸͺβŸͺ x ⟫⟫ = M (map quarter x)

_realisesα΄Ί_ : ((β„• β†’ πŸ›α΄Ί) β†’ πŸ›α΄Ί) β†’ ((β„• β†’ 𝕀) β†’ 𝕀) β†’ 𝓦 Μ‡
f realisesα΄Ί f' = (Ξ΄s : β„• β†’ πŸ›α΄Ί) β†’ f' (map βŸͺ_⟫ Ξ΄s) ＝ βŸͺ f Ξ΄s ⟫

𝟑s-conv-＝ : (a b c : πŸ›)
           β†’ (⟨ a ⟩ βŠ• (⟨ b ⟩ βŠ• ⟨ c ⟩))
           ＝ quarter ((a +πŸ› a) +𝟝 (b +πŸ› c))
𝟑s-conv-＝ βˆ’1 βˆ’1 βˆ’1 = ap (u βŠ•_) βŠ•-idem' βˆ™ βŠ•-idem'
𝟑s-conv-＝ βˆ’1 βˆ’1  O = refl
𝟑s-conv-＝ βˆ’1 βˆ’1 +1 = refl
𝟑s-conv-＝ βˆ’1  O βˆ’1 = ap (u βŠ•_) βŠ•-comm'
𝟑s-conv-＝ βˆ’1  O  O = ap (u βŠ•_) βŠ•-idem'
𝟑s-conv-＝ βˆ’1  O +1 = ap (u βŠ•_) βŠ•-comm'
𝟑s-conv-＝ βˆ’1 +1 βˆ’1 = ap (u βŠ•_) βŠ•-comm'
𝟑s-conv-＝ βˆ’1 +1  O = refl 
𝟑s-conv-＝ βˆ’1 +1 +1 = ap (u βŠ•_) βŠ•-idem'
𝟑s-conv-＝  O βˆ’1 βˆ’1 = βŠ•-comm' βˆ™ ap (_βŠ• (u βŠ• v)) βŠ•-idem'
𝟑s-conv-＝  O βˆ’1  O = βŠ•-tran' βˆ™ ap (_βŠ• (v βŠ• (u βŠ• v))) βŠ•-idem'
𝟑s-conv-＝  O βˆ’1 +1 = βŠ•-idem'
𝟑s-conv-＝  O  O βˆ’1 = ap ((u βŠ• v) βŠ•_) βŠ•-comm' βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• (v βŠ• (u βŠ• v))) βŠ•-idem'
𝟑s-conv-＝  O  O  O = ap ((u βŠ• v) βŠ•_) βŠ•-idem' βˆ™ βŠ•-idem'
𝟑s-conv-＝  O  O +1 = βŠ•-tran' βˆ™ ap ((u βŠ• (u βŠ• v)) βŠ•_) βŠ•-idem' βˆ™ βŠ•-comm'
𝟑s-conv-＝  O +1 βˆ’1 = ap ((u βŠ• v) βŠ•_) βŠ•-comm' βˆ™ βŠ•-idem'
𝟑s-conv-＝  O +1  O = ap (_βŠ• (v βŠ• (u βŠ• v))) βŠ•-comm' βˆ™ βŠ•-tran'
                   βˆ™ ap (_βŠ• (u βŠ• (u βŠ• v))) βŠ•-idem'
𝟑s-conv-＝  O +1 +1 = βŠ•-comm' βˆ™ ap (_βŠ• (u βŠ• v)) βŠ•-idem'
𝟑s-conv-＝ +1 βˆ’1 βˆ’1 = ap (v βŠ•_) βŠ•-idem' βˆ™ βŠ•-comm'
𝟑s-conv-＝ +1 βˆ’1  O = refl
𝟑s-conv-＝ +1 βˆ’1 +1 = refl
𝟑s-conv-＝ +1  O βˆ’1 = ap (v βŠ•_) βŠ•-comm'
𝟑s-conv-＝ +1  O  O = ap (v βŠ•_) βŠ•-idem'
𝟑s-conv-＝ +1  O +1 = ap (v βŠ•_) βŠ•-comm'
𝟑s-conv-＝ +1 +1 βˆ’1 = ap (v βŠ•_) βŠ•-comm'
𝟑s-conv-＝ +1 +1  O = refl
𝟑s-conv-＝ +1 +1 +1 = ap (v βŠ•_) βŠ•-idem' βˆ™ βŠ•-idem'

M-bigMid'-＝ : (x y : πŸ›α΄Ί) (z : 𝕀)
            β†’ (βŸͺ x ⟫ βŠ• (βŸͺ y ⟫ βŠ• z))
            ＝ (⟨ x 0 ⟩ βŠ• (⟨ x 1 ⟩ βŠ• ⟨ y 0 ⟩))
            βŠ• ((βŸͺ mid (tail (tail x)) (tail y) ⟫) βŠ• z)
M-bigMid'-＝ x y z
 = ap (_βŠ• (βŸͺ y ⟫ βŠ• z))
     (M-prop₁ (map ⟨_⟩ x)
 βˆ™ ap (⟨ x 0 ⟩ βŠ•_) (M-prop₁ (map ⟨_⟩ (tail x))))
 βˆ™ ap ((⟨ x 0 ⟩ βŠ• (⟨ x 1 ⟩ βŠ• βŸͺ tail (tail x) ⟫)) βŠ•_)
     (ap (_βŠ• z) (M-prop₁ (map ⟨_⟩ y)))
 βˆ™ ap (_βŠ• ((⟨ y 0 ⟩ βŠ• βŸͺ tail y ⟫) βŠ• z)) (βŠ•-comm')
 βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• (⟨ x 0 ⟩ βŠ• z)) βŠ•-tran'
 βˆ™ βŠ•-tran' βˆ™ ap (_βŠ• ((βŸͺ tail (tail x) ⟫ βŠ• βŸͺ tail y ⟫) βŠ• z)) βŠ•-comm'
 βˆ™ ap (Ξ» - β†’ (⟨ x 0 ⟩ βŠ• (⟨ x 1 ⟩ βŠ• ⟨ y 0 ⟩)) βŠ• (- βŠ• z))
     (mid-realiser (tail (tail x)) (tail y) ⁻¹)

bigMid'-approx : Ξ  (fg-n-approx' (map βŸͺ_⟫) (map quarter ∘ bigMid'))
bigMid'-approx n f Ξ±s
 = (z , w)
 , (M-bigMid'-＝ (αs 0) (αs 1)
     (m (append-one z ((first- n) (map βŸͺ_⟫ zs))))
 βˆ™ ap (_βŠ• ((βŸͺ mid x y ⟫) βŠ• m (append-one z ((first- n) (map βŸͺ_⟫ zs)))))
      (𝟑s-conv-＝ a b c')
 βˆ™ ap (quarter ((a +πŸ› a) +𝟝 (b +πŸ› c')) βŠ•_) (prβ‚‚ IH))
 where
   x = tail (tail (Ξ±s 0))
   y = tail (Ξ±s 1)
   a = Ξ±s 0 0
   b = Ξ±s 0 1
   c' = Ξ±s 1 0
   zs = tail (tail Ξ±s)
   IH = f (mid x y ∷ zs)
   z w : 𝕀
   z = pr₁ (pr₁ IH)
   w = prβ‚‚ (pr₁ IH)

M-realiser : bigMid realisesα΄Ί M
M-realiser Ξ΄s = fg-approx-holds (map βŸͺ_⟫) (map quarter ∘ bigMid')
                  bigMid'-approx Ξ΄s
                  βˆ™ quarter-realiser (bigMid' Ξ΄s) ⁻¹
\end{code}

## Multiplication

\begin{code}
digitMul-realiser : digitMul realises' _*_
digitMul-realiser βˆ’1 Ξ±
 = neg-realiser Ξ± ⁻¹ βˆ™ *-gives-negation-r βŸͺ Ξ± ⟫ ⁻¹
digitMul-realiser  O Ξ±
 = M-idem (u βŠ• v)    βˆ™ *-gives-zero-r     βŸͺ Ξ± ⟫ ⁻¹
digitMul-realiser +1 Ξ±
 = id-realiser Ξ± ⁻¹  βˆ™ *-gives-id-r       βŸͺ Ξ± ⟫ ⁻¹

mul-realiser : mul realisesΒ² _*_
mul-realiser Ξ± Ξ² = M-realiser (zipWith digitMul Ξ± (Ξ» _ β†’ Ξ²)) ⁻¹
                 βˆ™ map-realiserΒ² digitMul _*_ digitMul-realiser
                     (Ξ» a β†’ *-is-βŠ•-homomorphism-l ⟨ a ⟩) Ξ± Ξ²
                 βˆ™ βŠ•-homs-are-M-homs (_* βŸͺ Ξ² ⟫)
                     (*-is-βŠ•-homomorphism-r βŸͺ Ξ² ⟫)
                     (map ⟨_⟩ α) ⁻¹
\end{code}