1 files changed, 38 insertions, 6 deletions
diff --git a/src/Data/Term/Property.idr b/src/Data/Term/Property.idr
index 62f4caa..958c1c2 100644
--- a/src/Data/Term/Property.idr
+++ b/src/Data/Term/Property.idr
@@ -232,8 +232,8 @@ transitive prf1 prf2 = MkLte
   }
 
 export
-varMax : (f : Fin k -> Term sig m) -> f <= Var
-varMax f = MkLte f (\i => Refl)
+varUniqueMax : (f : Fin k -> Term sig m) -> f <= Var
+varUniqueMax f = MkLte f (\i => Refl)
 
 export
 compLte : f <= g -> (h : Fin k -> Term sig m) -> f . h <= g . h
@@ -255,6 +255,34 @@ lteExtend :
   (Extension p g).Prop prf.sub
 lteExtend prf x = p.cong _ _ prf.prf x
 
+-- Maximal ---------------------------------------------------------------------
+
+public export
+record Maximal (p : Property sig k) (f : Fin k -> Term sig n) where
+  constructor MkMaximal
+  valid : p.Prop f
+  universal : forall j. (g : Fin k -> Term sig j) -> p.Prop g -> Fin n -> Term sig j
+  factors :
+    forall j.
+    (g : Fin k -> Term sig j) ->
+    (v : p.Prop g) ->
+    g .=. universal g v . f
+
+public export
+Max : Property sig k -> Property sig k
+Max p = MkProp
+  { Prop = Maximal p
+  , cong = \f, g, prf, mg =>
+    MkMaximal
+      { valid = p.cong f g prf mg.valid
+      , universal = mg.universal
+      , factors = \h, v, x => Calc $
+        |~ h x
+        ~~ mg.universal h v <$> f x ...(mg.factors h v x)
+        ~~ mg.universal h v <$> g x ...(compCongR (mg.universal h v) prf x)
+      }
+  }
+
 -- Most General ----------------------------------------------------------------
 
 public export
@@ -278,6 +306,10 @@ record MostGeneral (p : Property sig k) (f : Fin k -> Term sig n) where
 %name MostGeneral mg
 
 export
+mostGeneralIsMaximal : MostGeneral p f -> Maximal p f
+mostGeneralIsMaximal mg = MkMaximal mg.valid mg.universal mg.factors
+
+export
 varMostGeneral : p.Prop Var -> MostGeneral p Var
 varMostGeneral v =
   MkMostGeneral
@@ -288,8 +320,8 @@ varMostGeneral v =
     }
 
 public export
-Max : Property sig k -> Property sig k
-Max p = MkProp
+UniqueMax : Property sig k -> Property sig k
+UniqueMax p = MkProp
   { Prop = MostGeneral p
   , cong = \f, g, prf, mg =>
     MkMostGeneral
@@ -309,7 +341,7 @@ Max p = MkProp
   }
 
 export
-maxCong : p <=> q -> Max p <=> Max q
+maxCong : p <=> q -> UniqueMax p <=> UniqueMax q
 maxCong prf = MkEquivalence
   { leftToRight = \f, mg =>
     MkMostGeneral
@@ -429,7 +461,7 @@ failTail :
   {ps : Vect _ (Property sig j)} ->
   {a : Fin j -> Term sig k} ->
   {f : Fin k -> Term sig m} ->
-  (Max (Extension p a)).Prop f ->
+  (UniqueMax (Extension p a)).Prop f ->
   Nothing (Extension (All ps) (f . a)) ->
   Nothing (Extension (All (p :: ps)) a)
 failTail mg absurd g (v :: vs) =