{-# OPTIONS --cubical-compatible --safe #-}
open import Tactic.RingSolver.Core.AlmostCommutativeRing
module Tactic.RingSolver.NonReflective
{ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
(let open AlmostCommutativeRing ring)
where
open import Algebra.Morphism
open import Function.Base using (id; _⟨_⟩_)
open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
open import Data.Maybe.Base
open import Data.Nat.Base using (ℕ)
open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
open import Data.Vec.Base using (Vec)
open import Data.Vec.N-ary
open import Tactic.RingSolver.Core.Polynomial.Parameters
open import Tactic.RingSolver.Core.Expression public
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring
module Ops where
zero-homo : ∀ x → T (is-just (0≟ x)) → 0# ≈ x
zero-homo x _ with just p ← 0≟ x = p
homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
homo = record
{ from = record
{ rawRing = AlmostCommutativeRing.rawRing ring
; isZero = λ x → is-just (0≟ x)
}
; to = record
{ isAlmostCommutativeRing = record
{ isCommutativeSemiring = isCommutativeSemiring
; -‿cong = -‿cong
; -‿*-distribˡ = -‿*-distribˡ
; -‿+-comm = -‿+-comm
}
}
; morphism = -raw-almostCommutative⟶ ring
; Zero-C⟶Zero-R = zero-homo
}
open Eval rawRing id public
open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)
norm : ∀ {n} → Expr Carrier n → Poly n
norm (Κ x) = κ x
norm (Ι x) = ι x
norm (x ⊕ y) = norm x ⊞ norm y
norm (x ⊗ y) = norm x ⊠ norm y
norm (⊝ x) = ⊟ norm x
norm (x ⊛ i) = norm x ⊡ i
⟦_⇓⟧ : ∀ {n} → Expr Carrier n → Vec Carrier n → Carrier
$\begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2150}{\htmlId{2150}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2090}{\htmlId{2155}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\htmlId{2158}{\htmlClass{Symbol}{\text{=}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2162}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2150}{\htmlId{2167}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\htmlId{2175}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{2186}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2191}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Semantics.html}{\htmlId{2198}{\htmlClass{Module}{\text{Tactic.RingSolver.Core.Polynomial.Semantics}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#1270}{\htmlId{2242}{\htmlClass{Function}{\text{homo}}}}\,
\,\htmlId{2253}{\htmlClass{Keyword}{\text{renaming}}}\, \,\htmlId{2262}{\htmlClass{Symbol}{\text{(}}}\,\begin{pmatrix} \,\htmlId{2267}{\htmlClass{Symbol}{\text{to}}}\, \begin{pmatrix}\,\htmlId{2274}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2279}{\htmlId{2279}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2287}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2289}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{2291}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2292}{\htmlId{2292}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2293}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{2295}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2296}{\htmlId{2296}{\htmlClass{Bound}{\text{expr}}}}\, \,\htmlId{2301}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{2303}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{2308}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2292}{\htmlId{2316}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2317}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2319}{\htmlId{2319}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2321}{\htmlClass{Symbol}{\text{→}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2296}{\htmlId{2325}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2090}{\htmlId{2330}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2319}{\htmlId{2333}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{2335}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2296}{\htmlId{2339}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2319}{\htmlId{2346}{\htmlClass{Bound}{\text{ρ}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2279}{\htmlId{2350}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2358}{\htmlClass{Symbol}{\text{{}}}\,\,\htmlId{2359}{\htmlClass{Argument}{\text{n}}}\, \,\htmlId{2361}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2363}{\htmlId{2363}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2364}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{2366}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2368}{\htmlClass{Function}{\text{go}}}}\,
\,\htmlId{2375}{\htmlClass{Keyword}{\text{where}}}\,
\,\htmlId{2385}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2390}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.html}{\htmlId{2397}{\htmlClass{Module}{\text{Tactic.RingSolver.Core.Polynomial.Homomorphism}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#1270}{\htmlId{2444}{\htmlClass{Function}{\text{homo}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2454}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2457}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2459}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{2461}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2462}{\htmlId{2462}{\htmlClass{Bound}{\text{expr}}}}\, \,\htmlId{2467}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{2469}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{2474}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2363}{\htmlId{2482}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2483}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2485}{\htmlId{2485}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2487}{\htmlClass{Symbol}{\text{→}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2462}{\htmlId{2491}{\htmlClass{Bound}{\text{expr}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2090}{\htmlId{2496}{\htmlClass{Function Operator}{\text{⇓⟧}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2485}{\htmlId{2499}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{2501}{\htmlClass{Field Operator}{\text{≈}}}}\, \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2462}{\htmlId{2505}{\htmlClass{Bound}{\text{expr}}}}\, \end{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2485}{\htmlId{2512}{\htmlClass{Bound}{\text{ρ}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2518}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2521}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#558}{\htmlId{2522}{\htmlClass{InductiveConstructor}{\text{Κ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2524}{\htmlId{2524}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2525}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2529}{\htmlId{2529}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2531}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Constants.html#663}{\htmlId{2533}{\htmlClass{Function}{\text{κ-hom}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2524}{\htmlId{2539}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2529}{\htmlId{2541}{\htmlClass{Bound}{\text{ρ}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2547}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2550}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#609}{\htmlId{2551}{\htmlClass{InductiveConstructor}{\text{Ι}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2553}{\htmlId{2553}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2554}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2558}{\htmlId{2558}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2560}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables.html#953}{\htmlId{2562}{\htmlClass{Function}{\text{ι-hom}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2553}{\htmlId{2568}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2558}{\htmlId{2570}{\htmlClass{Bound}{\text{ρ}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2576}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2579}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2580}{\htmlId{2580}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#660}{\htmlId{2582}{\htmlClass{InductiveConstructor Operator}{\text{⊕}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2584}{\htmlId{2584}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{2585}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2587}{\htmlId{2587}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2589}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition.html#1285}{\htmlId{2591}{\htmlClass{Function}{\text{⊞-hom}}}}\, \,\htmlId{2597}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2598}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2580}{\htmlId{2603}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2604}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{2606}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2607}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2584}{\htmlId{2612}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{2613}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2587}{\htmlId{2615}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2617}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1693}{\htmlId{2619}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2625}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\htmlId{2627}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2628}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2580}{\htmlId{2631}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2587}{\htmlId{2633}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2635}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Algebra.Structures.html#13870}{\htmlId{2637}{\htmlClass{Function}{\text{+-cong}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2644}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2646}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2584}{\htmlId{2649}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2587}{\htmlId{2651}{\htmlClass{Bound}{\text{ρ}}}}\,\,\htmlId{2652}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2658}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2661}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2662}{\htmlId{2662}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#711}{\htmlId{2664}{\htmlClass{InductiveConstructor Operator}{\text{⊗}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2666}{\htmlId{2666}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{2667}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2669}{\htmlId{2669}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2671}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Multiplication.html#9614}{\htmlId{2673}{\htmlClass{Function}{\text{⊠-hom}}}}\, \,\htmlId{2679}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2680}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2662}{\htmlId{2685}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2686}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{2688}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2689}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2666}{\htmlId{2694}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{2695}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2669}{\htmlId{2697}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2699}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1693}{\htmlId{2701}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2707}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\htmlId{2709}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2710}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2662}{\htmlId{2713}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2669}{\htmlId{2715}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2717}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Algebra.Structures.html#13435}{\htmlId{2719}{\htmlClass{Function}{\text{*-cong}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2726}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2728}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2666}{\htmlId{2731}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2669}{\htmlId{2733}{\htmlClass{Bound}{\text{ρ}}}}\,\,\htmlId{2734}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2740}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2743}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#825}{\htmlId{2744}{\htmlClass{InductiveConstructor Operator}{\text{⊝}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2746}{\htmlId{2746}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2747}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2751}{\htmlId{2751}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2753}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation.html#1764}{\htmlId{2755}{\htmlClass{Function}{\text{⊟-hom}}}}\, \,\htmlId{2761}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2762}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2746}{\htmlId{2767}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2768}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2751}{\htmlId{2770}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2774}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1693}{\htmlId{2776}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2782}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#995}{\htmlId{2784}{\htmlClass{Function}{\text{-‿cong}}}}\, \,\htmlId{2791}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2792}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2746}{\htmlId{2795}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2751}{\htmlId{2797}{\htmlClass{Bound}{\text{ρ}}}}\,\,\htmlId{2798}{\htmlClass{Symbol}{\text{)}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2804}{\htmlClass{Function}{\text{go}}}}\, \,\htmlId{2807}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2808}{\htmlId{2808}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#768}{\htmlId{2810}{\htmlClass{InductiveConstructor Operator}{\text{⊛}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2812}{\htmlId{2812}{\htmlClass{Bound}{\text{i}}}}\,\,\htmlId{2813}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2815}{\htmlId{2815}{\htmlClass{Bound}{\text{ρ}}}}\, \,\htmlId{2817}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.RingSolver.Core.Polynomial.Homomorphism.Exponentiation.html#3304}{\htmlId{2819}{\htmlClass{Function}{\text{⊡-hom}}}}\, \,\htmlId{2825}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#1886}{\htmlId{2826}{\htmlClass{Function}{\text{norm}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2808}{\htmlId{2831}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{2832}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2812}{\htmlId{2834}{\htmlClass{Bound}{\text{i}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2815}{\htmlId{2836}{\htmlClass{Bound}{\text{ρ}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2838}{\htmlClass{Function Operator}{\text{⟨}}}}\, \,\href{Relation.Binary.Structures.html#1693}{\htmlId{2840}{\htmlClass{Function}{\text{trans}}}}\, \,\href{Function.Base.html#4341}{\htmlId{2846}{\htmlClass{Function Operator}{\text{⟩}}}}\, \,\href{Algebra.Properties.Semiring.Exp.TCOptimised.html#1217}{\htmlId{2848}{\htmlClass{Function}{\text{\^{}-congˡ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2812}{\htmlId{2856}{\htmlClass{Bound}{\text{i}}}}\, \,\htmlId{2858}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2454}{\htmlId{2859}{\htmlClass{Function}{\text{go}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2808}{\htmlId{2862}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2815}{\htmlId{2864}{\htmlClass{Bound}{\text{ρ}}}}\,\,\htmlId{2865}{\htmlClass{Symbol}{\text{)}}}\,
\,\htmlId{2870}{\htmlClass{Keyword}{\text{open}}}\, \,\htmlId{2875}{\htmlClass{Keyword}{\text{import}}}\, \,\href{Relation.Binary.Reflection.html}{\htmlId{2882}{\htmlClass{Module}{\text{Relation.Binary.Reflection}}}}\, \,\href{Algebra.Structures.html#1873}{\htmlId{2909}{\htmlClass{Function}{\text{setoid}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#609}{\htmlId{2916}{\htmlClass{InductiveConstructor}{\text{Ι}}}}\, \begin{pmatrix} \begin{pmatrix} \,\href{Tactic.RingSolver.NonReflective.html#2279}{\htmlId{2927}{\htmlClass{Function}{\text{correct}}}}\, \,\htmlId{2935}{\htmlClass{Keyword}{\text{public}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2943}{\htmlId{2943}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{2949}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{2951}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{2953}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{2954}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{2956}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Builtin.Nat.html#203}{\htmlId{2958}{\htmlClass{Datatype}{\text{ℕ}}}}\,\,\htmlId{2959}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{2961}{\htmlClass{Symbol}{\text{→}}}\,
\,\htmlId{2971}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2972}{\htmlId{2972}{\htmlClass{Bound}{\text{f}}}}\, \,\htmlId{2974}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Data.Vec.N-ary.html#1168}{\htmlId{2976}{\htmlClass{Function}{\text{N-ary}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{2982}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{2984}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{2985}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{2990}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{2998}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{2999}{\htmlClass{Symbol}{\text{)}}}\, \,\htmlId{3001}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3002}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3007}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3015}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3017}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3019}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3024}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3032}{\htmlClass{Bound}{\text{n}}}}\,\,\htmlId{3033}{\htmlClass{Symbol}{\text{))}}}\, \,\htmlId{3036}{\htmlClass{Symbol}{\text{→}}}\,
\,\href{Data.Vec.N-ary.html#2526}{\htmlId{3046}{\htmlClass{Function}{\text{Eqʰ}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3050}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{3052}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, \,\htmlId{3056}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3057}{\htmlClass{Function}{\text{curryⁿ}}}}\, \,\htmlId{3064}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2090}{\htmlId{3065}{\htmlClass{Function Operator}{\text{Ops.⟦\_⇓⟧}}}}\, \,\htmlId{3074}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{3075}{\htmlClass{Field}{\text{proj₁}}}}\, \,\htmlId{3081}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3082}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3092}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2972}{\htmlId{3094}{\htmlClass{Bound}{\text{f}}}}\,\,\htmlId{3095}{\htmlClass{Symbol}{\text{))))}}}\, \,\htmlId{3100}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3101}{\htmlClass{Function}{\text{curryⁿ}}}}\, \,\htmlId{3108}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.NonReflective.html#2090}{\htmlId{3109}{\htmlClass{Function Operator}{\text{Ops.⟦\_⇓⟧}}}}\, \,\htmlId{3118}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#650}{\htmlId{3119}{\htmlClass{Field}{\text{proj₂}}}}\, \,\htmlId{3125}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3126}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3136}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2972}{\htmlId{3138}{\htmlClass{Bound}{\text{f}}}}\,\,\htmlId{3139}{\htmlClass{Symbol}{\text{))))}}}\, \,\htmlId{3144}{\htmlClass{Symbol}{\text{→}}}\,
\,\href{Data.Vec.N-ary.html#2282}{\htmlId{3154}{\htmlClass{Function}{\text{Eq}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3158}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1462}{\htmlId{3160}{\htmlClass{Field Operator}{\text{\_≈\_}}}}\, \,\htmlId{3164}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3165}{\htmlClass{Function}{\text{curryⁿ}}}}\, \,\htmlId{3172}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#1073}{\htmlId{3173}{\htmlClass{Function Operator}{\text{Ops.⟦\_⟧}}}}\, \,\htmlId{3182}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#636}{\htmlId{3183}{\htmlClass{Field}{\text{proj₁}}}}\, \,\htmlId{3189}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3190}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3200}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2972}{\htmlId{3202}{\htmlClass{Bound}{\text{f}}}}\,\,\htmlId{3203}{\htmlClass{Symbol}{\text{))))}}}\, \,\htmlId{3208}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Vec.N-ary.html#1379}{\htmlId{3209}{\htmlClass{Function}{\text{curryⁿ}}}}\, \,\htmlId{3216}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Tactic.RingSolver.Core.Expression.html#1073}{\htmlId{3217}{\htmlClass{Function Operator}{\text{Ops.⟦\_⟧}}}}\, \,\htmlId{3226}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Data.Product.Base.html#650}{\htmlId{3227}{\htmlClass{Field}{\text{proj₂}}}}\, \,\htmlId{3233}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.Reflection.html#2116}{\htmlId{3234}{\htmlClass{Function}{\text{Ops.close}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2954}{\htmlId{3244}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2972}{\htmlId{3246}{\htmlClass{Bound}{\text{f}}}}\,\,\htmlId{3247}{\htmlClass{Symbol}{\text{))))}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#2943}{\htmlId{3252}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{3258}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Binary.Reflection.html#2522}{\htmlId{3260}{\htmlClass{Function}{\text{Ops.solve}}}}\,
\,\htmlId{3270}{\htmlClass{Symbol}{\text{{-#}}}\, \,\htmlId{3274}{\htmlClass{Keyword}{\text{INLINE}}}\, \,\href{Tactic.RingSolver.NonReflective.html#2943}{\htmlId{3281}{\htmlClass{Function}{\text{solve}}}}\, \,\htmlId{3287}{\htmlClass{Symbol}{\text{#-}}}}\,
\,\htmlId{3292}{\htmlClass{Keyword}{\text{infixl}}}\, \,\htmlId{3299}{\htmlClass{Number}{\text{6}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3305}{\htmlId{3301}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#3305}{\htmlId{3305}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3309}{\htmlClass{Symbol}{\text{:}}}\, \,\htmlId{3311}{\htmlClass{Symbol}{\text{∀}}}\, \,\htmlId{3313}{\htmlClass{Symbol}{\text{{}}}\,\,\href{Tactic.RingSolver.NonReflective.html#3314}{\htmlId{3314}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3316}{\htmlClass{Symbol}{\text{:}}}\, \,\href{Agda.Builtin.Nat.html#203}{\htmlId{3318}{\htmlClass{Datatype}{\text{ℕ}}}}\,\,\htmlId{3319}{\htmlClass{Symbol}{\text{}}}}\, \,\htmlId{3321}{\htmlClass{Symbol}{\text{→}}}\,
\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3329}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3334}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3314}{\htmlId{3342}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3344}{\htmlClass{Symbol}{\text{→}}}\,
\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3352}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3357}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3314}{\htmlId{3365}{\htmlClass{Bound}{\text{n}}}}\, \,\htmlId{3367}{\htmlClass{Symbol}{\text{→}}}\,
\,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3375}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3380}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3314}{\htmlId{3388}{\htmlClass{Bound}{\text{n}}}}\, \,\href{Data.Product.Base.html#1618}{\htmlId{3390}{\htmlClass{Function Operator}{\text{×}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#513}{\htmlId{3392}{\htmlClass{Datatype}{\text{Expr}}}}\, \,\href{Tactic.RingSolver.Core.AlmostCommutativeRing.html#1426}{\htmlId{3397}{\htmlClass{Field}{\text{Carrier}}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3314}{\htmlId{3405}{\htmlClass{Bound}{\text{n}}}}\,
\,\href{Tactic.RingSolver.NonReflective.html#3305}{\htmlId{3407}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3411}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Agda.Builtin.Sigma.html#235}{\htmlId{3413}{\htmlClass{InductiveConstructor Operator}{\text{\_,\_}}}}\,
\,\htmlId{3417}{\htmlClass{Symbol}{\text{{-#}}}\, \,\htmlId{3421}{\htmlClass{Keyword}{\text{INLINE}}}\, \,\href{Tactic.RingSolver.NonReflective.html#3305}{\htmlId{3428}{\htmlClass{Function Operator}{\text{\_⊜\_}}}}\, \,\htmlId{3432}{\htmlClass{Symbol}{\text{#-}}}}\,