---
layout: default
file: "src/FLRP/Certificates/Group/TG9x4TwoByTwo.lagda.md"
title: "FLRP.Certificates.Group.TG9x4TwoByTwo module (The Agda Universal Algebra Library)"
date: "2026-07-24"
author: "the agda-algebras development team (emitted by scripts/python/flrp)"
---
### A machine-checked representation: Con(coset action of TransitiveGroup[9, 4] on 9 cosets of H (order 2)) ≅ 2x2 (four-element Boolean lattice)
This is the [FLRP.Certificates.Group.TG9x4TwoByTwo][] module of the [Agda Universal Algebra Library][].
**This module was emitted by `scripts/python/flrp/emit_agda.py` from
`scripts/python/flrp/inputs/tg9x4_two_by_two.json`. Do not edit it by hand; rerun the emitter instead.**
The four-element Boolean lattice 2×2 as the upper interval [H, G] with G = TransitiveGroup(9,4) ≅ C3×S3 and H a point stabilizer (index 9), from the SmallLatticeReps manuscript Figure 10. Found by the issue #487 GAP subgroup-interval engine; this module is the direct-certificate route (coset action → claim → checker).
It re-verifies, end-to-end through the WP-6 certificate pipeline (#457), the
claim that the congruence lattice of the algebra "coset action of TransitiveGroup[9, 4] on 9 cosets of H (order 2)" — carrier size
9, unary operations `g0`, `g1`, `g2` — is isomorphic to the lattice
"2x2 (four-element Boolean lattice)" (4 elements). The engine's output below (normal-form
parent vectors, Freese traces, and pointer tables) is certificate data only:
the search-free checkers of [Setoid.Congruences.Certificates][] re-verify all
of it during type-checking, and the [FLRP.Certificates][] assembly turns the
checked certificate into the headline theorems — a
`Representableᵈ`{.AgdaRecord} witness for the target lattice and a
`FiniteCongruencesᵈ`{.AgdaRecord} instance for the algebra. Nothing is
believed on the engine's authority: a wrong table or trace would make a
decidable check compute to `no`{.AgdaInductiveConstructor} and break
compilation.
<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}
module FLRP.Certificates.Group.TG9x4TwoByTwo where
open import Data.Fin.Base using ( Fin )
open import Data.Fin.Patterns using ( 0F ; 1F ; 2F ; 3F ; 4F ; 5F ; 6F ; 7F ; 8F )
open import Data.List.Base using ( [] ; _∷_ )
open import Data.Vec.Base using ( Vec ; [] ; _∷_ )
open import Level using ( 0ℓ )
open import Classical.Signatures.Unary using ( Sig-Unary )
open import Classical.Structures.Unary using ( tablesToUnaryAlgebra
; tablesToUnaryAlgebra-FiniteAlgebra
; Sig-Unary-Fin-FiniteSignature )
open import FLRP.Certificates using ( MeetMatches ; meetMatches?
; certRepresentableᵈ )
open import FLRP.Problem using ( FiniteLattice ; toLattice )
open import FLRP.Representable using ( Representableᵈ )
open import Overture.Cayley using ( Table ; ⟦_⟧ ; from-yes )
open import Overture.Operations.Properties
using ( Associative? ; Commutative?
; Idempotent? ; Absorbsˡ? ; Absorbsʳ? )
open import Setoid.Algebras.Basic using ( Algebra )
open import Setoid.Algebras.Finite using ( FiniteAlgebra )
open import Setoid.Congruences.Certificates.Schema
using ( ParentVec ; Trace ; LatticeCert
; mkLatticeCert ; mkMerge
; seed ; translate )
open import Setoid.Congruences.Certificates.Congruence
using ( module CertCheck )
open import Setoid.Congruences.Certificates.Lattice
using ( module LatticeCheck )
open import Setoid.Congruences.Finite.Decidable
using ( FiniteCongruencesᵈ )
open import Setoid.Signatures.Finite using ( FiniteSignature )
```
-->
#### The algebra, from its operation tables
Row `f` of `opTables`{.AgdaFunction} is the value table of the `f`-th unary
operation; [Classical.Structures.Unary][] turns the table into the algebra
and its finiteness witnesses.
```agda
opTables : Vec (Vec (Fin 9) 9) 3
opTables = (1F ∷ 3F ∷ 4F ∷ 0F ∷ 6F ∷ 7F ∷ 2F ∷ 8F ∷ 5F ∷ [])
∷ (2F ∷ 4F ∷ 5F ∷ 6F ∷ 7F ∷ 0F ∷ 8F ∷ 1F ∷ 3F ∷ [])
∷ (1F ∷ 0F ∷ 4F ∷ 3F ∷ 2F ∷ 7F ∷ 6F ∷ 5F ∷ 8F ∷ [])
∷ []
𝑨 : Algebra {𝑆 = Sig-Unary (Fin 3)} 0ℓ 0ℓ
𝑨 = tablesToUnaryAlgebra 9 3 opTables
𝑭 : FiniteAlgebra 𝑨
𝑭 = tablesToUnaryAlgebra-FiniteAlgebra 9 3 opTables
𝑺 : FiniteSignature (Sig-Unary (Fin 3))
𝑺 = Sig-Unary-Fin-FiniteSignature 3
```
#### The target lattice, from its Cayley tables
The claimed congruence lattice "2x2 (four-element Boolean lattice)", presented exactly as the
worked lattice examples are ([Examples.Classical.Lattices.L7][]): meet and
join tables, every law discharged by decision over the finite carrier.
```agda
∧-table ∨-table : Table 4
∧-table = (0F ∷ 0F ∷ 0F ∷ 0F ∷ [])
∷ (0F ∷ 1F ∷ 0F ∷ 1F ∷ [])
∷ (0F ∷ 0F ∷ 2F ∷ 2F ∷ [])
∷ (0F ∷ 1F ∷ 2F ∷ 3F ∷ [])
∷ []
∨-table = (0F ∷ 1F ∷ 2F ∷ 3F ∷ [])
∷ (1F ∷ 1F ∷ 3F ∷ 3F ∷ [])
∷ (2F ∷ 3F ∷ 2F ∷ 3F ∷ [])
∷ (3F ∷ 3F ∷ 3F ∷ 3F ∷ [])
∷ []
open FiniteLattice
𝑳 : FiniteLattice
𝑳 .size = 3
𝑳 ._∧_ = ⟦ ∧-table ⟧
𝑳 ._∨_ = ⟦ ∨-table ⟧
𝑳 .∧-assoc = from-yes (Associative? ⟦ ∧-table ⟧)
𝑳 .∧-comm = from-yes (Commutative? ⟦ ∧-table ⟧)
𝑳 .∧-idem = from-yes (Idempotent? ⟦ ∧-table ⟧)
𝑳 .∨-assoc = from-yes (Associative? ⟦ ∨-table ⟧)
𝑳 .∨-comm = from-yes (Commutative? ⟦ ∨-table ⟧)
𝑳 .∨-idem = from-yes (Idempotent? ⟦ ∨-table ⟧)
𝑳 .absorbˡ = from-yes (Absorbsˡ? ⟦ ∧-table ⟧ ⟦ ∨-table ⟧)
𝑳 .absorbʳ = from-yes (Absorbsʳ? ⟦ ∧-table ⟧ ⟦ ∨-table ⟧)
```
#### The certificate
The engine's whole-lattice certificate (design note § 4): the congruence
list as normal-form parent vectors, indexed by the lattice's carrier; the
principal-congruence pointer table with one Freese trace per carrier pair;
and the join traces, seeded by forest edges. The meet and join tables are
the target's own tables, which is what `MeetMatches`{.AgdaFunction} pins.
```agda
open CertCheck 𝑭 𝑺 using ( arOf )
cert : LatticeCert 9 3 arOf 4
cert = mkLatticeCert partsᵛ 0F prinᵛ prinTrᵛ ∧-table ∨-table joinTrᵛ
where
partsᵛ : Vec (ParentVec 9) 4
partsᵛ = (0F ∷ 1F ∷ 2F ∷ 3F ∷ 4F ∷ 5F ∷ 6F ∷ 7F ∷ 8F ∷ [])
∷ (0F ∷ 0F ∷ 2F ∷ 0F ∷ 2F ∷ 5F ∷ 2F ∷ 5F ∷ 5F ∷ [])
∷ (0F ∷ 1F ∷ 0F ∷ 3F ∷ 1F ∷ 0F ∷ 3F ∷ 1F ∷ 3F ∷ [])
∷ (0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ 0F ∷ [])
∷ []
prinᵛ : Vec (Vec (Fin 4) 9) 9
prinᵛ = (0F ∷ 1F ∷ 2F ∷ 1F ∷ 3F ∷ 2F ∷ 3F ∷ 3F ∷ 3F ∷ [])
∷ (1F ∷ 0F ∷ 3F ∷ 1F ∷ 2F ∷ 3F ∷ 3F ∷ 2F ∷ 3F ∷ [])
∷ (2F ∷ 3F ∷ 0F ∷ 3F ∷ 1F ∷ 2F ∷ 1F ∷ 3F ∷ 3F ∷ [])
∷ (1F ∷ 1F ∷ 3F ∷ 0F ∷ 3F ∷ 3F ∷ 2F ∷ 3F ∷ 2F ∷ [])
∷ (3F ∷ 2F ∷ 1F ∷ 3F ∷ 0F ∷ 3F ∷ 1F ∷ 2F ∷ 3F ∷ [])
∷ (2F ∷ 3F ∷ 2F ∷ 3F ∷ 3F ∷ 0F ∷ 3F ∷ 1F ∷ 1F ∷ [])
∷ (3F ∷ 3F ∷ 1F ∷ 2F ∷ 1F ∷ 3F ∷ 0F ∷ 3F ∷ 2F ∷ [])
∷ (3F ∷ 2F ∷ 3F ∷ 3F ∷ 2F ∷ 1F ∷ 3F ∷ 0F ∷ 1F ∷ [])
∷ (3F ∷ 3F ∷ 3F ∷ 2F ∷ 3F ∷ 1F ∷ 2F ∷ 1F ∷ 0F ∷ [])
∷ []
prinTrᵛ : Vec (Vec (Trace 9 3 arOf) 9) 9
prinTrᵛ = ( []
∷ ( mkMerge 0F 1F (seed 0)
∷ mkMerge 1F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 8F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 0F 2F (seed 0)
∷ mkMerge 1F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 6F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 4F 7F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 6F 8F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 0F 3F (seed 0)
∷ mkMerge 1F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 5F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 0F 4F (seed 0)
∷ mkMerge 1F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 2F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 4F 8F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 0F 6F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 5F 1F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 0F 5F (seed 0)
∷ mkMerge 1F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 8F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 4F 1F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 6F 3F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 0F 6F (seed 0)
∷ mkMerge 1F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 6F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 4F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 4F 5F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 0F 4F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 6F 7F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 0F 7F (seed 0)
∷ mkMerge 1F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 5F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 4F 3F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 0F 8F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 6F 0F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 0F 8F (seed 0)
∷ mkMerge 1F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 2F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 8F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 7F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 4F 0F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 0F 7F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 5F 6F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ [] )
∷ ( ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 7F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ []
∷ ( mkMerge 1F 2F (seed 0)
∷ mkMerge 3F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 4F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 0F 6F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 6F 7F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 3F 2F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 2F 8F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 1F 3F (seed 0)
∷ mkMerge 3F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 5F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 1F 4F (seed 0)
∷ mkMerge 3F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 8F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 2F 5F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 1F 5F (seed 0)
∷ mkMerge 3F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 7F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 0F 8F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 6F 1F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 3F 5F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 7F 2F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 1F 6F (seed 0)
∷ mkMerge 3F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 6F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 0F 4F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 6F 5F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 3F 4F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 7F 3F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 1F 7F (seed 0)
∷ mkMerge 3F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 3F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 2F 0F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 1F 8F (seed 0)
∷ mkMerge 3F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 4F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 8F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 0F 7F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 6F 0F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 3F 7F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 2F 3F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ [] )
∷ ( ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 3F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 7F 4F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 8F 6F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 2F 1F (seed 0)
∷ mkMerge 4F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 0F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 7F 6F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 2F 3F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 8F 2F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ []
∷ ( mkMerge 2F 3F (seed 0)
∷ mkMerge 4F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 3F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 1F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 7F 2F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 2F 1F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 0F 8F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 2F 4F (seed 0)
∷ mkMerge 4F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 3F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 2F 5F (seed 0)
∷ mkMerge 4F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 8F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 7F 1F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 8F 3F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 2F 6F (seed 0)
∷ mkMerge 4F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 0F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 2F 7F (seed 0)
∷ mkMerge 4F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 5F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 7F 3F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 2F 8F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 0F 4F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 2F 8F (seed 0)
∷ mkMerge 4F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 5F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 8F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 6F 7F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 7F 0F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 2F 7F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 8F 1F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ [] )
∷ ( ( mkMerge 3F 0F (seed 0)
∷ mkMerge 0F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 7F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 3F 1F (seed 0)
∷ mkMerge 0F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 8F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 3F 2F (seed 0)
∷ mkMerge 0F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 4F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 1F 6F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 2F 7F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 1F 2F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 8F 0F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ []
∷ ( mkMerge 3F 4F (seed 0)
∷ mkMerge 0F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 1F 2F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 2F 8F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 1F 6F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 6F 5F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 3F 5F (seed 0)
∷ mkMerge 0F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 7F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 1F 8F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 2F 1F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 1F 5F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 4F 3F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 3F 6F (seed 0)
∷ mkMerge 0F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 4F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 2F 5F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 4F 7F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 3F 7F (seed 0)
∷ mkMerge 0F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 1F 5F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 2F 3F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 1F 8F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 8F 4F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 3F 8F (seed 0)
∷ mkMerge 0F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 6F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 7F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 2F 0F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 4F 1F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ [] )
∷ ( ( mkMerge 4F 0F (seed 0)
∷ mkMerge 6F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 1F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 2F 3F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 8F 4F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 6F 0F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 1F 5F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 4F 1F (seed 0)
∷ mkMerge 6F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 6F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 5F 2F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 4F 2F (seed 0)
∷ mkMerge 6F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 1F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 4F 3F (seed 0)
∷ mkMerge 6F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 3F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 2F 1F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 8F 2F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 6F 1F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 5F 6F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ []
∷ ( mkMerge 4F 5F (seed 0)
∷ mkMerge 6F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 7F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 2F 8F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 8F 1F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 6F 5F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 5F 3F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 4F 6F (seed 0)
∷ mkMerge 6F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 0F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 4F 7F (seed 0)
∷ mkMerge 6F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 3F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 5F 0F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 4F 8F (seed 0)
∷ mkMerge 6F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 7F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 8F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 2F 7F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 8F 0F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 6F 7F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 1F 6F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ [] )
∷ ( ( mkMerge 5F 0F (seed 0)
∷ mkMerge 7F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 3F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 1F 4F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 3F 6F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 5F 1F (seed 0)
∷ mkMerge 7F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 0F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 1F 6F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 5F 3F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 2F 7F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 5F 2F (seed 0)
∷ mkMerge 7F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 6F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 1F 7F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 3F 8F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 5F 3F (seed 0)
∷ mkMerge 7F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 3F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 1F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 1F 2F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 5F 1F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 3F 4F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 5F 4F (seed 0)
∷ mkMerge 7F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 2F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 1F 8F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 5F 6F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 3F 5F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ []
∷ ( mkMerge 5F 6F (seed 0)
∷ mkMerge 7F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 6F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 8F 4F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 1F 5F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 5F 4F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 2F 3F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 5F 7F (seed 0)
∷ mkMerge 7F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 6F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 5F 8F (seed 0)
∷ mkMerge 7F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 0F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 1F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 2F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ [] )
∷ ( ( mkMerge 6F 0F (seed 0)
∷ mkMerge 2F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 1F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 4F 3F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 5F 4F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 4F 0F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 7F 6F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 6F 1F (seed 0)
∷ mkMerge 2F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 4F 0F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 5F 6F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 4F 3F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 3F 7F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 6F 2F (seed 0)
∷ mkMerge 2F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 1F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 6F 3F (seed 0)
∷ mkMerge 2F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 1F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 5F 2F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 7F 4F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 6F 4F (seed 0)
∷ mkMerge 2F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 3F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 6F 5F (seed 0)
∷ mkMerge 2F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 7F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 4F 8F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 5F 1F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 4F 5F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 3F 2F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ []
∷ ( mkMerge 6F 7F (seed 0)
∷ mkMerge 2F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 5F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 4F 5F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 5F 3F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 4F 8F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 8F 0F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 6F 8F (seed 0)
∷ mkMerge 2F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 8F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 7F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 5F 0F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 7F 1F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ [] )
∷ ( ( mkMerge 7F 0F (seed 0)
∷ mkMerge 8F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 1F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 5F 3F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 3F 4F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 8F 0F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 0F 6F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 7F 1F (seed 0)
∷ mkMerge 8F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 6F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 0F 2F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 7F 2F (seed 0)
∷ mkMerge 8F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 4F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 5F 6F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 3F 7F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 8F 2F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 4F 0F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 7F 3F (seed 0)
∷ mkMerge 8F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 3F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 5F 1F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 3F 2F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 8F 1F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 4F 8F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 7F 4F (seed 0)
∷ mkMerge 8F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 3F 8F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 0F 5F (translate 2F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 7F 5F (seed 0)
∷ mkMerge 8F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 4F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 7F 6F (seed 0)
∷ mkMerge 8F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 5F 6F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 5F 4F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 3F 5F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 8F 4F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 0F 8F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ []
∷ ( mkMerge 7F 8F (seed 0)
∷ mkMerge 8F 5F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 1F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 3F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 4F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 2F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ [] )
∷ ( ( mkMerge 8F 0F (seed 0)
∷ mkMerge 5F 1F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 1F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 7F 3F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 0F 4F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 7F 0F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 6F 5F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 8F 1F (seed 0)
∷ mkMerge 5F 3F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 0F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 7F 0F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 0F 6F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 7F 3F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 3F 2F (translate 2F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 8F 2F (seed 0)
∷ mkMerge 5F 4F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 5F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 4F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 7F 6F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 0F 7F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 7F 2F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 1F 8F (translate 1F 0F (0F ∷ []) 2)
∷ [] )
∷ ( mkMerge 8F 3F (seed 0)
∷ mkMerge 5F 0F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 6F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 1F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 0F 2F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 1F 4F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 8F 4F (seed 0)
∷ mkMerge 5F 6F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 7F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 8F 2F (translate 2F 0F (0F ∷ []) 2)
∷ mkMerge 7F 2F (translate 0F 0F (0F ∷ []) 2)
∷ mkMerge 0F 8F (translate 1F 0F (0F ∷ []) 3)
∷ mkMerge 7F 6F (translate 2F 0F (0F ∷ []) 4)
∷ mkMerge 6F 1F (translate 1F 0F (0F ∷ []) 4)
∷ [] )
∷ ( mkMerge 8F 5F (seed 0)
∷ mkMerge 5F 7F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 0F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 2F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 4F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 8F 6F (seed 0)
∷ mkMerge 5F 2F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 8F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 7F 4F (translate 0F 0F (0F ∷ []) 1)
∷ mkMerge 0F 5F (translate 1F 0F (0F ∷ []) 2)
∷ mkMerge 1F 7F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ ( mkMerge 8F 7F (seed 0)
∷ mkMerge 5F 8F (translate 0F 0F (0F ∷ []) 0)
∷ mkMerge 3F 1F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 0F 3F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 6F 4F (translate 1F 0F (0F ∷ []) 1)
∷ mkMerge 2F 6F (translate 1F 0F (0F ∷ []) 1)
∷ [] )
∷ []
∷ [] )
∷ []
joinTrᵛ : Vec (Vec (Trace 9 3 arOf) 4) 4
joinTrᵛ = ( []
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 0F (seed 1)
∷ mkMerge 4F 2F (seed 2)
∷ mkMerge 6F 2F (seed 3)
∷ mkMerge 7F 5F (seed 4)
∷ mkMerge 8F 5F (seed 5)
∷ [] )
∷ ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (seed 1)
∷ mkMerge 5F 0F (seed 2)
∷ mkMerge 6F 3F (seed 3)
∷ mkMerge 7F 1F (seed 4)
∷ mkMerge 8F 3F (seed 5)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 2F 0F (seed 1)
∷ mkMerge 3F 0F (seed 2)
∷ mkMerge 4F 0F (seed 3)
∷ mkMerge 5F 0F (seed 4)
∷ mkMerge 6F 0F (seed 5)
∷ mkMerge 7F 0F (seed 6)
∷ mkMerge 8F 0F (seed 7)
∷ [] )
∷ [] )
∷ ( ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 0F (seed 1)
∷ mkMerge 4F 2F (seed 2)
∷ mkMerge 6F 2F (seed 3)
∷ mkMerge 7F 5F (seed 4)
∷ mkMerge 8F 5F (seed 5)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 0F (seed 1)
∷ mkMerge 4F 2F (seed 2)
∷ mkMerge 6F 2F (seed 3)
∷ mkMerge 7F 5F (seed 4)
∷ mkMerge 8F 5F (seed 5)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 0F (seed 1)
∷ mkMerge 4F 2F (seed 2)
∷ mkMerge 6F 2F (seed 3)
∷ mkMerge 7F 5F (seed 4)
∷ mkMerge 8F 5F (seed 5)
∷ mkMerge 2F 0F (seed 6)
∷ mkMerge 5F 0F (seed 8)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 3F 0F (seed 1)
∷ mkMerge 4F 2F (seed 2)
∷ mkMerge 6F 2F (seed 3)
∷ mkMerge 7F 5F (seed 4)
∷ mkMerge 8F 5F (seed 5)
∷ mkMerge 2F 0F (seed 7)
∷ mkMerge 5F 0F (seed 10)
∷ [] )
∷ [] )
∷ ( ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (seed 1)
∷ mkMerge 5F 0F (seed 2)
∷ mkMerge 6F 3F (seed 3)
∷ mkMerge 7F 1F (seed 4)
∷ mkMerge 8F 3F (seed 5)
∷ [] )
∷ ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (seed 1)
∷ mkMerge 5F 0F (seed 2)
∷ mkMerge 6F 3F (seed 3)
∷ mkMerge 7F 1F (seed 4)
∷ mkMerge 8F 3F (seed 5)
∷ mkMerge 1F 0F (seed 6)
∷ mkMerge 3F 0F (seed 7)
∷ [] )
∷ ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (seed 1)
∷ mkMerge 5F 0F (seed 2)
∷ mkMerge 6F 3F (seed 3)
∷ mkMerge 7F 1F (seed 4)
∷ mkMerge 8F 3F (seed 5)
∷ [] )
∷ ( mkMerge 2F 0F (seed 0)
∷ mkMerge 4F 1F (seed 1)
∷ mkMerge 5F 0F (seed 2)
∷ mkMerge 6F 3F (seed 3)
∷ mkMerge 7F 1F (seed 4)
∷ mkMerge 8F 3F (seed 5)
∷ mkMerge 1F 0F (seed 6)
∷ mkMerge 3F 0F (seed 8)
∷ [] )
∷ [] )
∷ ( ( mkMerge 1F 0F (seed 0)
∷ mkMerge 2F 0F (seed 1)
∷ mkMerge 3F 0F (seed 2)
∷ mkMerge 4F 0F (seed 3)
∷ mkMerge 5F 0F (seed 4)
∷ mkMerge 6F 0F (seed 5)
∷ mkMerge 7F 0F (seed 6)
∷ mkMerge 8F 0F (seed 7)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 2F 0F (seed 1)
∷ mkMerge 3F 0F (seed 2)
∷ mkMerge 4F 0F (seed 3)
∷ mkMerge 5F 0F (seed 4)
∷ mkMerge 6F 0F (seed 5)
∷ mkMerge 7F 0F (seed 6)
∷ mkMerge 8F 0F (seed 7)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 2F 0F (seed 1)
∷ mkMerge 3F 0F (seed 2)
∷ mkMerge 4F 0F (seed 3)
∷ mkMerge 5F 0F (seed 4)
∷ mkMerge 6F 0F (seed 5)
∷ mkMerge 7F 0F (seed 6)
∷ mkMerge 8F 0F (seed 7)
∷ [] )
∷ ( mkMerge 1F 0F (seed 0)
∷ mkMerge 2F 0F (seed 1)
∷ mkMerge 3F 0F (seed 2)
∷ mkMerge 4F 0F (seed 3)
∷ mkMerge 5F 0F (seed 4)
∷ mkMerge 6F 0F (seed 5)
∷ mkMerge 7F 0F (seed 6)
∷ mkMerge 8F 0F (seed 7)
∷ [] )
∷ [] )
∷ []
```
#### The verification
One decision for the whole certificate, one for the meet-table match; both
compute to `yes`{.AgdaInductiveConstructor} — that computation *is* the
re-verification of every engine claim above.
```agda
open LatticeCheck 𝑭 𝑺
certOK : LatticeCertOK cert
certOK = from-yes (latticeCertOK? cert)
certMeet : MeetMatches 𝑭 𝑺 𝑳 cert
certMeet = from-yes (meetMatches? 𝑭 𝑺 𝑳 cert)
```
#### The headline theorems
The target lattice is decidably representable, witnessed by this algebra;
and the certificate's congruence list is a complete Layer-D enumeration of
the algebra's decidable congruences.
```agda
TG9x4TwoByTwo-Representableᵈ : Representableᵈ (toLattice 𝑳)
TG9x4TwoByTwo-Representableᵈ = certRepresentableᵈ 𝑭 𝑺 𝑳 cert certOK certMeet
TG9x4TwoByTwo-FiniteCongruencesᵈ : FiniteCongruencesᵈ 𝑨
TG9x4TwoByTwo-FiniteCongruencesᵈ = certFiniteCongruencesᵈ cert certOK
```
--------------------------------------