From f668bbbc963271a0158e03a2fb28229ee1029aa5 Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Mon, 15 Dec 2025 14:23:52 -0500
Subject: [PATCH 1/6] port of fixpointab and fixpointab_ne sections

---
 src/Iris/Algebra/OFE.lean | 178 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 178 insertions(+)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index f44b0327..c872b427 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -802,6 +802,184 @@ theorem OFE.ContractiveHom.fixpoint_ind [COFE α] [Inhabited α] (f : α -c> α)
 
 end Fixpoint
 
+section FixpointAB
+
+class ContractiveABA [OFE α] [OFE β] (fA : α → β → α) where
+  dL_dist_dist : DistLater n x₁ x₂ → y₁ ≡{n}≡ y₂ → fA x₁ y₁ ≡{n}≡ fA x₂ y₂
+  non_exp : NonExpansive₂ fA := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    apply dL_dist_dist
+    exact Dist.distLater Hx
+    exact Hy
+  ⟩
+class ContractiveABB [OFE α] [OFE β] (fB : α → β → β) where
+  dL_dL_dist : DistLater n x₁ x₂ → DistLater n y₁ y₂ → fB x₁ y₁ ≡{n}≡ fB x₂ y₂
+  non_exp : NonExpansive₂ fB := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    apply dL_dL_dist
+    exact Dist.distLater Hx
+    exact Dist.distLater Hy
+  ⟩
+
+def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fB : α → β → β) [ContractiveABB fB]
+  (x : α) : β :=
+by
+  let con_hom : β -c> β := {
+    f := fB x,
+    contractive := {
+      distLater_dist := fun dl => ContractiveABB.dL_dL_dist DistLater.rfl dl
+    }
+  }
+  exact OFE.ContractiveHom.fixpoint con_hom
+
+theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fB : α → β → β) [fB_Contractive: ContractiveABB fB]
+  : Contractive (fixpointAB fB) where
+  distLater_dist := by
+    intro n y1 y2 Dl
+    apply OFE.ContractiveHom.fixpoint_ne.ne
+    intro y
+    apply fB_Contractive.dL_dL_dist
+    exact Dl
+    exact DistLater.rfl
+
+def fixpointAA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [ContractiveABB fB]
+  (x : α) : α := fA x (fixpointAB fB x)
+
+theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive: ContractiveABA fA]
+  [fB_Contractive: ContractiveABB fB]
+  : Contractive (fixpointAA fA fB) where
+  distLater_dist := by
+    intro n y1 y2 Dl
+    apply fA_Contractive.dL_dist_dist
+    exact Dl
+    apply (fixpointAB_contractive fB).distLater_dist
+    exact Dl
+
+def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [ContractiveABB fB]
+  : α :=
+by
+  let con_hom : α -c> α := {
+    f := fixpointAA fA fB,
+    contractive := {
+      distLater_dist := by
+        intro n y1 y2 Dl
+        apply fA_Contractive.dL_dist_dist
+        exact Dl
+        apply (fixpointAB_contractive fB).distLater_dist
+        exact Dl
+    }
+  }
+  exact OFE.ContractiveHom.fixpoint con_hom
+
+
+def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fB_Contractive : ContractiveABB fB]
+  : β := fixpointAB fB <| fixpointA fA fB
+
+theorem fixpointA_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fB_Contractive : ContractiveABB fB]
+: fA (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointA fA fB) := by
+  exact .symm (fixpoint_unfold _)
+
+theorem fixpointB_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fB_Contractive : ContractiveABB fB]
+: fB (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointB fA fB) := by
+  exact .symm (fixpoint_unfold _)
+
+theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fB_Contractive : ContractiveABB fB]
+  p q
+: fA p q ≡ p → fB p q ≡ q → p ≡ (fixpointA fA fB) := by
+  intro Hp Hq
+  refine .trans Hp.symm ?_
+  apply fixpoint_unique
+  have := fA_Contractive.non_exp
+  refine NonExpansive₂.eqv Hp.symm ?_
+  apply fixpoint_unique
+  have := fB_Contractive.non_exp
+  refine .trans ?_ (NonExpansive₂.eqv Hp.symm Equiv.rfl)
+  exact Hq.symm
+
+theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fB : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fB_Contractive : ContractiveABB fB]
+  p q
+: fA p q ≡ p → fB p q ≡ q → q ≡ (fixpointB fA fB) := by
+  intro Hp Hq
+  apply fixpoint_unique
+  have := fB_Contractive.non_exp
+  refine .trans Hq.symm (NonExpansive₂.eqv ?_ Equiv.rfl)
+  apply fixpointA_unique fA fB p q
+  exact Hp
+  exact Hq
+
+theorem fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fA' : α → β → α)
+  (fB : α → β → β)
+  (fB' : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fA'_Contractive : ContractiveABA fA']
+  [fB_Contractive : ContractiveABB fB]
+  [fB'_Contractive : ContractiveABB fB']
+  n : (∀ x y, fA x y ≡{n}≡ fA' x y) →
+      (∀ x y, fB x y ≡{n}≡ fB' x y) →
+      fixpointA fA fB ≡{n}≡ fixpointA fA' fB' := by
+  intros HfA HfB
+  apply OFE.ContractiveHom.fixpoint_ne.ne
+  intro z1
+  refine .trans (fA_Contractive.non_exp.ne Dist.rfl ?_) (HfA z1 _)
+  apply OFE.ContractiveHom.fixpoint_ne.ne
+  intro z2
+  exact HfB z1 z2
+
+
+theorem fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA : α → β → α)
+  (fA' : α → β → α)
+  (fB : α → β → β)
+  (fB' : α → β → β)
+  [fA_Contractive : ContractiveABA fA]
+  [fA'_Contractive : ContractiveABA fA']
+  [fB_Contractive : ContractiveABB fB]
+  [fB'_Contractive : ContractiveABB fB']
+  n : (∀ x y, fA x y ≡{n}≡ fA' x y) →
+      (∀ x y, fB x y ≡{n}≡ fB' x y) →
+      fixpointB fA fB ≡{n}≡ fixpointB fA' fB' := by
+  intros HfA HfB
+  apply OFE.ContractiveHom.fixpoint_ne.ne
+  intro z1
+  refine .trans (fB_Contractive.non_exp.ne ?_ Dist.rfl) (HfB _ z1)
+  apply fixpointA_ne
+  exact HfA
+  exact HfB
+
+end FixpointAB
+
 section Later
 
 structure Later (A : Type u) : Type (u+1) where

From 02684ebdef6ef5f1c141533d9668a91bdcfeb847 Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Tue, 16 Dec 2025 11:50:41 -0500
Subject: [PATCH 2/6] new structures to make ne proof an instance of
 nonexpansive

---
 src/Iris/Algebra/OFE.lean | 113 ++++++++++++++++++++++----------------
 1 file changed, 65 insertions(+), 48 deletions(-)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index c872b427..380f7380 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -806,19 +806,50 @@ section FixpointAB
 
 class ContractiveABA [OFE α] [OFE β] (fA : α → β → α) where
   dL_dist_dist : DistLater n x₁ x₂ → y₁ ≡{n}≡ y₂ → fA x₁ y₁ ≡{n}≡ fA x₂ y₂
-  non_exp : NonExpansive₂ fA := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
-    apply dL_dist_dist
+
+@[ext] structure ContractiveABAHom (α β : Type _) [OFE α] [OFE β] where
+  f: α → β → α
+  [contractive: ContractiveABA f]
+  ne₂: NonExpansive₂ f := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    apply contractive.dL_dist_dist
     exact Dist.distLater Hx
     exact Hy
   ⟩
+
+instance [OFE α] [OFE β] : OFE (ContractiveABAHom α β) where
+  Equiv f g := f.f ≡ g.f
+  Dist n f g := f.f ≡{n}≡ g.f
+  dist_eqv := {
+    refl _ := dist_eqv.refl _
+    symm h := dist_eqv.symm h
+    trans h1 h2 := dist_eqv.trans h1 h2
+  }
+  equiv_dist := equiv_dist
+  dist_lt := dist_lt
+
 class ContractiveABB [OFE α] [OFE β] (fB : α → β → β) where
   dL_dL_dist : DistLater n x₁ x₂ → DistLater n y₁ y₂ → fB x₁ y₁ ≡{n}≡ fB x₂ y₂
-  non_exp : NonExpansive₂ fB := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
-    apply dL_dL_dist
+
+@[ext] structure ContractiveABBHom (α β : Type _) [OFE α] [OFE β] where
+  f: α → β → β
+  [contractive: ContractiveABB f]
+  ne₂: NonExpansive₂ f := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    apply contractive.dL_dL_dist
     exact Dist.distLater Hx
     exact Dist.distLater Hy
   ⟩
 
+instance [OFE α] [OFE β] : OFE (ContractiveABBHom α β) where
+  Equiv f g := f.f ≡ g.f
+  Dist n f g := f.f ≡{n}≡ g.f
+  dist_eqv := {
+    refl _ := dist_eqv.refl _
+    symm h := dist_eqv.symm h
+    trans h1 h2 := dist_eqv.trans h1 h2
+  }
+  equiv_dist := equiv_dist
+  dist_lt := dist_lt
+
 def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   (fB : α → β → β) [ContractiveABB fB]
   (x : α) : β :=
@@ -865,7 +896,7 @@ def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   (fA : α → β → α)
   (fB : α → β → β)
   [fA_Contractive : ContractiveABA fA]
-  [ContractiveABB fB]
+  [fB_Contractive : ContractiveABB fB]
   : α :=
 by
   let con_hom : α -c> α := {
@@ -881,6 +912,9 @@ by
   }
   exact OFE.ContractiveHom.fixpoint con_hom
 
+nonrec abbrev OFE.ContractiveHom.fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA: ContractiveABAHom α β) (fB: ContractiveABBHom α β) : α :=
+    fixpointA (fA_Contractive := fA.contractive) (fB_Contractive := fB.contractive) fA.f fB.f
 
 def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   (fA : α → β → α)
@@ -889,6 +923,10 @@ def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   [fB_Contractive : ContractiveABB fB]
   : β := fixpointAB fB <| fixpointA fA fB
 
+nonrec abbrev OFE.ContractiveHom.fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
+  (fA: ContractiveABAHom α β) (fB: ContractiveABBHom α β) : β :=
+    fixpointB (fA_Contractive := fA.contractive) (fB_Contractive := fB.contractive) fA.f fB.f
+
 theorem fixpointA_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   (fA : α → β → α)
   (fB : α → β → β)
@@ -915,10 +953,10 @@ theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   intro Hp Hq
   refine .trans Hp.symm ?_
   apply fixpoint_unique
-  have := fA_Contractive.non_exp
+  have := ({f := fA} : ContractiveABAHom α β).ne₂
   refine NonExpansive₂.eqv Hp.symm ?_
   apply fixpoint_unique
-  have := fB_Contractive.non_exp
+  have := ({f := fB} : ContractiveABBHom α β).ne₂
   refine .trans ?_ (NonExpansive₂.eqv Hp.symm Equiv.rfl)
   exact Hq.symm
 
@@ -931,52 +969,31 @@ theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
 : fA p q ≡ p → fB p q ≡ q → q ≡ (fixpointB fA fB) := by
   intro Hp Hq
   apply fixpoint_unique
-  have := fB_Contractive.non_exp
+  have := ({f := fB} : ContractiveABBHom α β).ne₂
   refine .trans Hq.symm (NonExpansive₂.eqv ?_ Equiv.rfl)
   apply fixpointA_unique fA fB p q
   exact Hp
   exact Hq
 
-theorem fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fA' : α → β → α)
-  (fB : α → β → β)
-  (fB' : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fA'_Contractive : ContractiveABA fA']
-  [fB_Contractive : ContractiveABB fB]
-  [fB'_Contractive : ContractiveABB fB']
-  n : (∀ x y, fA x y ≡{n}≡ fA' x y) →
-      (∀ x y, fB x y ≡{n}≡ fB' x y) →
-      fixpointA fA fB ≡{n}≡ fixpointA fA' fB' := by
-  intros HfA HfB
-  apply OFE.ContractiveHom.fixpoint_ne.ne
-  intro z1
-  refine .trans (fA_Contractive.non_exp.ne Dist.rfl ?_) (HfA z1 _)
-  apply OFE.ContractiveHom.fixpoint_ne.ne
-  intro z2
-  exact HfB z1 z2
-
-
-theorem fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fA' : α → β → α)
-  (fB : α → β → β)
-  (fB' : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fA'_Contractive : ContractiveABA fA']
-  [fB_Contractive : ContractiveABB fB]
-  [fB'_Contractive : ContractiveABB fB']
-  n : (∀ x y, fA x y ≡{n}≡ fA' x y) →
-      (∀ x y, fB x y ≡{n}≡ fB' x y) →
-      fixpointB fA fB ≡{n}≡ fixpointB fA' fB' := by
-  intros HfA HfB
-  apply OFE.ContractiveHom.fixpoint_ne.ne
-  intro z1
-  refine .trans (fB_Contractive.non_exp.ne ?_ Dist.rfl) (HfB _ z1)
-  apply fixpointA_ne
-  exact HfA
-  exact HfB
+instance OFE.ContractiveHom.fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
+  NonExpansive₂ (OFE.ContractiveHom.fixpointA (α := α) (β := β)) where
+  ne n fA fA' HfA fB fB' HfB := by
+    apply OFE.ContractiveHom.fixpoint_ne.ne
+    intro z₁
+    refine .trans (fA.ne₂.ne Dist.rfl ?_) (HfA z₁ _)
+    apply OFE.ContractiveHom.fixpoint_ne.ne
+    intro z₂
+    exact HfB z₁ z₂
+
+instance OFE.ContractiveHom.fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
+  NonExpansive₂ (OFE.ContractiveHom.fixpointB (α := α) (β := β)) where
+  ne n fA fA' HfA fB fB' HfB := by
+    apply OFE.ContractiveHom.fixpoint_ne.ne
+    intro z₁
+    refine .trans (fB.ne₂.ne ?_ Dist.rfl) (HfB _ z₁)
+    apply OFE.ContractiveHom.fixpointA_ne.ne
+    exact HfA
+    exact HfB
 
 end FixpointAB
 

From 248509d4105d86659c93dc6835b0ded07aef2820 Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Tue, 16 Dec 2025 12:10:09 -0500
Subject: [PATCH 3/6] fix translation of proper

---
 src/Iris/Algebra/OFE.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 380f7380..4f7539a7 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -805,7 +805,7 @@ end Fixpoint
 section FixpointAB
 
 class ContractiveABA [OFE α] [OFE β] (fA : α → β → α) where
-  dL_dist_dist : DistLater n x₁ x₂ → y₁ ≡{n}≡ y₂ → fA x₁ y₁ ≡{n}≡ fA x₂ y₂
+  dL_dist_dist : ∀ ⦃n x₁ x₂⦄, DistLater n x₁ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → fA x₁ y₁ ≡{n}≡ fA x₂ y₂
 
 @[ext] structure ContractiveABAHom (α β : Type _) [OFE α] [OFE β] where
   f: α → β → α
@@ -828,7 +828,7 @@ instance [OFE α] [OFE β] : OFE (ContractiveABAHom α β) where
   dist_lt := dist_lt
 
 class ContractiveABB [OFE α] [OFE β] (fB : α → β → β) where
-  dL_dL_dist : DistLater n x₁ x₂ → DistLater n y₁ y₂ → fB x₁ y₁ ≡{n}≡ fB x₂ y₂
+  dL_dL_dist : ∀ ⦃n x₁ x₂⦄, DistLater n x₁ x₂ → ∀ ⦃y₁ y₂⦄, DistLater n y₁ y₂ → fB x₁ y₁ ≡{n}≡ fB x₂ y₂
 
 @[ext] structure ContractiveABBHom (α β : Type _) [OFE α] [OFE β] where
   f: α → β → β

From 97542bd2eedd628193c878b3bb015f8dbc5b6073 Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Tue, 16 Dec 2025 16:01:48 -0500
Subject: [PATCH 4/6] eliminate unnecessary 2-argument contractive classes by
 relying on -c> and -n>

---
 src/Iris/Algebra/OFE.lean | 174 ++++++++++++--------------------------
 1 file changed, 54 insertions(+), 120 deletions(-)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 4f7539a7..5460352a 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -804,196 +804,130 @@ end Fixpoint
 
 section FixpointAB
 
-class ContractiveABA [OFE α] [OFE β] (fA : α → β → α) where
-  dL_dist_dist : ∀ ⦃n x₁ x₂⦄, DistLater n x₁ x₂ → ∀ ⦃y₁ y₂⦄, y₁ ≡{n}≡ y₂ → fA x₁ y₁ ≡{n}≡ fA x₂ y₂
-
-@[ext] structure ContractiveABAHom (α β : Type _) [OFE α] [OFE β] where
-  f: α → β → α
-  [contractive: ContractiveABA f]
-  ne₂: NonExpansive₂ f := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
-    apply contractive.dL_dist_dist
-    exact Dist.distLater Hx
-    exact Hy
-  ⟩
-
-instance [OFE α] [OFE β] : OFE (ContractiveABAHom α β) where
-  Equiv f g := f.f ≡ g.f
-  Dist n f g := f.f ≡{n}≡ g.f
-  dist_eqv := {
-    refl _ := dist_eqv.refl _
-    symm h := dist_eqv.symm h
-    trans h1 h2 := dist_eqv.trans h1 h2
-  }
-  equiv_dist := equiv_dist
-  dist_lt := dist_lt
+/-- A composition of a contractive function and a NonExpansive function is NonExpansive₂. -/
+instance ne₂_of_contractive_ne [OFE α] [OFE β] (fA : α -c> β -n> α) : NonExpansive₂ fun x => (fA.f x).f where
+  ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    refine .trans ?_ ((fA.f x₂).ne.ne Hy)
+    apply fA.ne.ne Hx
 
-class ContractiveABB [OFE α] [OFE β] (fB : α → β → β) where
-  dL_dL_dist : ∀ ⦃n x₁ x₂⦄, DistLater n x₁ x₂ → ∀ ⦃y₁ y₂⦄, DistLater n y₁ y₂ → fB x₁ y₁ ≡{n}≡ fB x₂ y₂
+/-- A composition of two contractive functions is NonExpansive₂. -/
+instance ne₂_of_contractive [OFE α] [OFE β] (fB : α -c> β -c> β) : NonExpansive₂ fun x => (fB.f x).f where
+  ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
+    refine .trans ?_ ((fB.f x₂).ne.ne Hy)
+    apply fB.ne.ne Hx
 
-@[ext] structure ContractiveABBHom (α β : Type _) [OFE α] [OFE β] where
-  f: α → β → β
-  [contractive: ContractiveABB f]
-  ne₂: NonExpansive₂ f := ⟨fun n x₁ x₂ Hx y₁ y₂ Hy => by
-    apply contractive.dL_dL_dist
-    exact Dist.distLater Hx
-    exact Dist.distLater Hy
-  ⟩
-
-instance [OFE α] [OFE β] : OFE (ContractiveABBHom α β) where
-  Equiv f g := f.f ≡ g.f
-  Dist n f g := f.f ≡{n}≡ g.f
-  dist_eqv := {
-    refl _ := dist_eqv.refl _
-    symm h := dist_eqv.symm h
-    trans h1 h2 := dist_eqv.trans h1 h2
-  }
-  equiv_dist := equiv_dist
-  dist_lt := dist_lt
 
 def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fB : α → β → β) [ContractiveABB fB]
+  (fB : α -c> β -c> β)
   (x : α) : β :=
 by
   let con_hom : β -c> β := {
     f := fB x,
     contractive := {
-      distLater_dist := fun dl => ContractiveABB.dL_dL_dist DistLater.rfl dl
+      distLater_dist := fun dl => by
+        apply (fB x).contractive.distLater_dist
+        exact dl
     }
   }
   exact OFE.ContractiveHom.fixpoint con_hom
 
 theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fB : α → β → β) [fB_Contractive: ContractiveABB fB]
+  (fB : α -c> β -c> β)
   : Contractive (fixpointAB fB) where
   distLater_dist := by
-    intro n y1 y2 Dl
+    intro n x₁ x₂ Dl
     apply OFE.ContractiveHom.fixpoint_ne.ne
-    intro y
-    apply fB_Contractive.dL_dL_dist
+    apply fB.contractive.distLater_dist
     exact Dl
-    exact DistLater.rfl
 
 def fixpointAA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   (x : α) : α := fA x (fixpointAB fB x)
 
 theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive: ContractiveABA fA]
-  [fB_Contractive: ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   : Contractive (fixpointAA fA fB) where
   distLater_dist := by
-    intro n y1 y2 Dl
-    apply fA_Contractive.dL_dist_dist
-    exact Dl
-    apply (fixpointAB_contractive fB).distLater_dist
+    intro n x₁ x₂ Dl
+    refine .trans ?_ ((fA x₂).ne.ne ((fixpointAB_contractive fB).distLater_dist Dl))
+    apply fA.contractive.distLater_dist
     exact Dl
 
 def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   : α :=
 by
   let con_hom : α -c> α := {
     f := fixpointAA fA fB,
     contractive := {
       distLater_dist := by
-        intro n y1 y2 Dl
-        apply fA_Contractive.dL_dist_dist
-        exact Dl
-        apply (fixpointAB_contractive fB).distLater_dist
-        exact Dl
+        intro n x₁ x₂ Dl
+        exact (fixpointAA_contractive fA fB).distLater_dist Dl
     }
   }
   exact OFE.ContractiveHom.fixpoint con_hom
 
-nonrec abbrev OFE.ContractiveHom.fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA: ContractiveABAHom α β) (fB: ContractiveABBHom α β) : α :=
-    fixpointA (fA_Contractive := fA.contractive) (fB_Contractive := fB.contractive) fA.f fB.f
 
 def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   : β := fixpointAB fB <| fixpointA fA fB
 
-nonrec abbrev OFE.ContractiveHom.fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA: ContractiveABAHom α β) (fB: ContractiveABBHom α β) : β :=
-    fixpointB (fA_Contractive := fA.contractive) (fB_Contractive := fB.contractive) fA.f fB.f
-
 theorem fixpointA_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
 : fA (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointA fA fB) := by
   exact .symm (fixpoint_unfold _)
 
 theorem fixpointB_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
 : fB (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointB fA fB) := by
   exact .symm (fixpoint_unfold _)
 
 theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   p q
 : fA p q ≡ p → fB p q ≡ q → p ≡ (fixpointA fA fB) := by
   intro Hp Hq
   refine .trans Hp.symm ?_
   apply fixpoint_unique
-  have := ({f := fA} : ContractiveABAHom α β).ne₂
-  refine NonExpansive₂.eqv Hp.symm ?_
+  have := ne₂_of_contractive_ne fA
+  refine NonExpansive₂.eqv (f := fun x => (fA.f x).f) Hp.symm ?_
   apply fixpoint_unique
-  have := ({f := fB} : ContractiveABBHom α β).ne₂
-  refine .trans ?_ (NonExpansive₂.eqv Hp.symm Equiv.rfl)
-  exact Hq.symm
+  have := ne₂_of_contractive fB
+  exact .trans Hq.symm (NonExpansive₂.eqv (f := fun x => (fB.f x).f) Hp.symm Equiv.rfl)
 
 theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α → β → α)
-  (fB : α → β → β)
-  [fA_Contractive : ContractiveABA fA]
-  [fB_Contractive : ContractiveABB fB]
+  (fA : α -c> β -n> α)
+  (fB : α -c> β -c> β)
   p q
 : fA p q ≡ p → fB p q ≡ q → q ≡ (fixpointB fA fB) := by
   intro Hp Hq
   apply fixpoint_unique
-  have := ({f := fB} : ContractiveABBHom α β).ne₂
-  refine .trans Hq.symm (NonExpansive₂.eqv ?_ Equiv.rfl)
-  apply fixpointA_unique fA fB p q
-  exact Hp
-  exact Hq
-
-instance OFE.ContractiveHom.fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
-  NonExpansive₂ (OFE.ContractiveHom.fixpointA (α := α) (β := β)) where
+  have := ne₂_of_contractive fB
+  refine .trans Hq.symm (NonExpansive₂.eqv (f := fun x => (fB.f x).f) ?_ Equiv.rfl)
+  exact fixpointA_unique fA fB p q Hp Hq
+
+instance fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
+  NonExpansive₂ (fixpointA (α := α) (β := β)) where
   ne n fA fA' HfA fB fB' HfB := by
     apply OFE.ContractiveHom.fixpoint_ne.ne
     intro z₁
-    refine .trans (fA.ne₂.ne Dist.rfl ?_) (HfA z₁ _)
-    apply OFE.ContractiveHom.fixpoint_ne.ne
-    intro z₂
-    exact HfB z₁ z₂
+    refine .trans ((ne₂_of_contractive_ne fA).ne Dist.rfl ?_) (HfA z₁ _)
+    exact OFE.ContractiveHom.fixpoint_ne.ne (HfB z₁)
 
-instance OFE.ContractiveHom.fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
-  NonExpansive₂ (OFE.ContractiveHom.fixpointB (α := α) (β := β)) where
+instance fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
+  NonExpansive₂ (fixpointB (α := α) (β := β)) where
   ne n fA fA' HfA fB fB' HfB := by
     apply OFE.ContractiveHom.fixpoint_ne.ne
     intro z₁
-    refine .trans (fB.ne₂.ne ?_ Dist.rfl) (HfB _ z₁)
-    apply OFE.ContractiveHom.fixpointA_ne.ne
-    exact HfA
-    exact HfB
+    refine .trans ((ne₂_of_contractive fB).ne ?_ Dist.rfl) (HfB _ z₁)
+    exact fixpointA_ne.ne HfA HfB
 
 end FixpointAB
 

From 47a90dbfa142784c8e56af0aa4d681f535de482f Mon Sep 17 00:00:00 2001
From: GenericMonkey <pransrin@umich.edu>
Date: Wed, 17 Dec 2025 11:46:27 -0500
Subject: [PATCH 5/6] adding function coersion for fA and fB

---
 src/Iris/Algebra/OFE.lean | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 5460352a..40599af4 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -804,14 +804,17 @@ end Fixpoint
 
 section FixpointAB
 
-/-- A composition of a contractive function and a NonExpansive function is NonExpansive₂. -/
-instance ne₂_of_contractive_ne [OFE α] [OFE β] (fA : α -c> β -n> α) : NonExpansive₂ fun x => (fA.f x).f where
+instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -n> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩
+instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -c> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩
+
+/-- A Contractive function with NonExpansive function codomain is NonExpansive₂. -/
+instance ne₂_of_contractive_ne [OFE α] [OFE β] [OFE γ] (fA : α -c> β -n> γ) : NonExpansive₂ fA where
   ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
     refine .trans ?_ ((fA.f x₂).ne.ne Hy)
     apply fA.ne.ne Hx
 
-/-- A composition of two contractive functions is NonExpansive₂. -/
-instance ne₂_of_contractive [OFE α] [OFE β] (fB : α -c> β -c> β) : NonExpansive₂ fun x => (fB.f x).f where
+/-- A Contractive function with Contractive function codomain is NonExpansive₂. -/
+instance ne₂_of_contractive [OFE α] [OFE β] [OFE γ] (fB : α -c> β -c> γ) : NonExpansive₂ fB where
   ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
     refine .trans ?_ ((fB.f x₂).ne.ne Hy)
     apply fB.ne.ne Hx
@@ -825,7 +828,7 @@ by
     f := fB x,
     contractive := {
       distLater_dist := fun dl => by
-        apply (fB x).contractive.distLater_dist
+        apply (fB.f x).contractive.distLater_dist
         exact dl
     }
   }
@@ -851,7 +854,7 @@ theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   : Contractive (fixpointAA fA fB) where
   distLater_dist := by
     intro n x₁ x₂ Dl
-    refine .trans ?_ ((fA x₂).ne.ne ((fixpointAB_contractive fB).distLater_dist Dl))
+    refine .trans ?_ ((fA.f x₂).ne.ne ((fixpointAB_contractive fB).distLater_dist Dl))
     apply fA.contractive.distLater_dist
     exact Dl
 
@@ -897,10 +900,10 @@ theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   refine .trans Hp.symm ?_
   apply fixpoint_unique
   have := ne₂_of_contractive_ne fA
-  refine NonExpansive₂.eqv (f := fun x => (fA.f x).f) Hp.symm ?_
+  refine NonExpansive₂.eqv (f := fA) Hp.symm ?_
   apply fixpoint_unique
   have := ne₂_of_contractive fB
-  exact .trans Hq.symm (NonExpansive₂.eqv (f := fun x => (fB.f x).f) Hp.symm Equiv.rfl)
+  exact .trans Hq.symm (NonExpansive₂.eqv (f := fB) Hp.symm Equiv.rfl)
 
 theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   (fA : α -c> β -n> α)
@@ -910,7 +913,7 @@ theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
   intro Hp Hq
   apply fixpoint_unique
   have := ne₂_of_contractive fB
-  refine .trans Hq.symm (NonExpansive₂.eqv (f := fun x => (fB.f x).f) ?_ Equiv.rfl)
+  refine .trans Hq.symm (NonExpansive₂.eqv (f := fB) ?_ Equiv.rfl)
   exact fixpointA_unique fA fB p q Hp Hq
 
 instance fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :

From 8a2e79f610dfb2e766cc273a68f8c220cef17aa8 Mon Sep 17 00:00:00 2001
From: Markus de Medeiros <markusdemedeiros@outlook.com>
Date: Sat, 20 Dec 2025 00:32:23 -0500
Subject: [PATCH 6/6] chore: cleanup

---
 src/Iris/Algebra/OFE.lean | 109 ++++++++++++++------------------------
 1 file changed, 40 insertions(+), 69 deletions(-)

diff --git a/src/Iris/Algebra/OFE.lean b/src/Iris/Algebra/OFE.lean
index 40599af4..23999fc9 100644
--- a/src/Iris/Algebra/OFE.lean
+++ b/src/Iris/Algebra/OFE.lean
@@ -804,132 +804,103 @@ end Fixpoint
 
 section FixpointAB
 
+open OFE
+
 instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -n> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩
 instance [OFE α] [OFE β] [OFE γ] : CoeFun (α -c> β -c> γ) (fun _ => α → β → γ) := ⟨fun f x => (f.f x).f⟩
 
 /-- A Contractive function with NonExpansive function codomain is NonExpansive₂. -/
 instance ne₂_of_contractive_ne [OFE α] [OFE β] [OFE γ] (fA : α -c> β -n> γ) : NonExpansive₂ fA where
-  ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
+  ne n x₁ x₂ Hx y₁ y₂ Hy := by
     refine .trans ?_ ((fA.f x₂).ne.ne Hy)
     apply fA.ne.ne Hx
 
 /-- A Contractive function with Contractive function codomain is NonExpansive₂. -/
 instance ne₂_of_contractive [OFE α] [OFE β] [OFE γ] (fB : α -c> β -c> γ) : NonExpansive₂ fB where
-  ne := fun n x₁ x₂ Hx y₁ y₂ Hy => by
+  ne n x₁ x₂ Hx y₁ y₂ Hy := by
     refine .trans ?_ ((fB.f x₂).ne.ne Hy)
     apply fB.ne.ne Hx
 
-
-def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fB : α -c> β -c> β)
-  (x : α) : β :=
-by
+def fixpointAB [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fB : α -c> β -c> β) (x : α) : β := by
   let con_hom : β -c> β := {
     f := fB x,
-    contractive := {
-      distLater_dist := fun dl => by
-        apply (fB.f x).contractive.distLater_dist
-        exact dl
-    }
+    contractive := ⟨fB.f x |>.contractive.distLater_dist⟩
   }
-  exact OFE.ContractiveHom.fixpoint con_hom
+  exact con_hom.fixpoint
 
-theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fB : α -c> β -c> β)
-  : Contractive (fixpointAB fB) where
-  distLater_dist := by
-    intro n x₁ x₂ Dl
-    apply OFE.ContractiveHom.fixpoint_ne.ne
+theorem fixpointAB_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fB : α -c> β -c> β) :
+    Contractive (fixpointAB fB) where
+  distLater_dist {n _ _} Dl := by
+    apply ContractiveHom.fixpoint_ne.ne
     apply fB.contractive.distLater_dist
     exact Dl
 
-def fixpointAA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  (x : α) : α := fA x (fixpointAB fB x)
+def fixpointAA [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α)
+    (fB : α -c> β -c> β) (x : α) : α :=
+  fA x (fixpointAB fB x)
 
 theorem fixpointAA_contractive [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  : Contractive (fixpointAA fA fB) where
-  distLater_dist := by
-    intro n x₁ x₂ Dl
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) : Contractive (fixpointAA fA fB) where
+  distLater_dist {_ _ x₂} Dl := by
     refine .trans ?_ ((fA.f x₂).ne.ne ((fixpointAB_contractive fB).distLater_dist Dl))
     apply fA.contractive.distLater_dist
     exact Dl
 
-def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  : α :=
-by
+def fixpointA [COFE α] [COFE β] [Inhabited α] [Inhabited β] (fA : α -c> β -n> α)
+    (fB : α -c> β -c> β) : α := by
   let con_hom : α -c> α := {
     f := fixpointAA fA fB,
-    contractive := {
-      distLater_dist := by
-        intro n x₁ x₂ Dl
-        exact (fixpointAA_contractive fA fB).distLater_dist Dl
-    }
+    contractive := ⟨(fixpointAA_contractive fA fB).distLater_dist⟩
   }
-  exact OFE.ContractiveHom.fixpoint con_hom
-
+  exact con_hom.fixpoint
 
 def fixpointB [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  : β := fixpointAB fB <| fixpointA fA fB
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) : β :=
+  fixpointAB fB <| fixpointA fA fB
 
 theorem fixpointA_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-: fA (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointA fA fB) := by
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) :
+    fA (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointA fA fB) := by
   exact .symm (fixpoint_unfold _)
 
 theorem fixpointB_unfold [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-: fB (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointB fA fB) := by
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) :
+    fB (fixpointA fA fB) (fixpointB fA fB) ≡ (fixpointB fA fB) := by
   exact .symm (fixpoint_unfold _)
 
 theorem fixpointA_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  p q
-: fA p q ≡ p → fB p q ≡ q → p ≡ (fixpointA fA fB) := by
-  intro Hp Hq
-  refine .trans Hp.symm ?_
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : fA p q ≡ p) (Hq : fB p q ≡ q) :
+    p ≡ (fixpointA fA fB) := by
+  refine Hp.symm.trans ?_
   apply fixpoint_unique
   have := ne₂_of_contractive_ne fA
   refine NonExpansive₂.eqv (f := fA) Hp.symm ?_
   apply fixpoint_unique
   have := ne₂_of_contractive fB
-  exact .trans Hq.symm (NonExpansive₂.eqv (f := fB) Hp.symm Equiv.rfl)
+  exact Hq.symm.trans (NonExpansive₂.eqv (f := fB) Hp.symm .rfl)
 
 theorem fixpointB_unique [COFE α] [COFE β] [Inhabited α] [Inhabited β]
-  (fA : α -c> β -n> α)
-  (fB : α -c> β -c> β)
-  p q
-: fA p q ≡ p → fB p q ≡ q → q ≡ (fixpointB fA fB) := by
-  intro Hp Hq
+    (fA : α -c> β -n> α) (fB : α -c> β -c> β) (Hp : fA p q ≡ p) (Hq : fB p q ≡ q) :
+    q ≡ (fixpointB fA fB) := by
   apply fixpoint_unique
   have := ne₂_of_contractive fB
-  refine .trans Hq.symm (NonExpansive₂.eqv (f := fB) ?_ Equiv.rfl)
-  exact fixpointA_unique fA fB p q Hp Hq
+  refine Hq.symm.trans (NonExpansive₂.eqv (f := fB) ?_ .rfl)
+  exact fixpointA_unique fA fB Hp Hq
 
 instance fixpointA_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
-  NonExpansive₂ (fixpointA (α := α) (β := β)) where
+    NonExpansive₂ (fixpointA (α := α) (β := β)) where
   ne n fA fA' HfA fB fB' HfB := by
     apply OFE.ContractiveHom.fixpoint_ne.ne
     intro z₁
-    refine .trans ((ne₂_of_contractive_ne fA).ne Dist.rfl ?_) (HfA z₁ _)
-    exact OFE.ContractiveHom.fixpoint_ne.ne (HfB z₁)
+    refine ((ne₂_of_contractive_ne fA).ne .rfl ?_).trans (HfA z₁ _)
+    exact ContractiveHom.fixpoint_ne.ne (HfB z₁)
 
 instance fixpointB_ne [COFE α] [COFE β] [Inhabited α] [Inhabited β] :
-  NonExpansive₂ (fixpointB (α := α) (β := β)) where
+    NonExpansive₂ (fixpointB (α := α) (β := β)) where
   ne n fA fA' HfA fB fB' HfB := by
-    apply OFE.ContractiveHom.fixpoint_ne.ne
+    apply ContractiveHom.fixpoint_ne.ne
     intro z₁
-    refine .trans ((ne₂_of_contractive fB).ne ?_ Dist.rfl) (HfB _ z₁)
+    refine ((ne₂_of_contractive fB).ne ?_ .rfl).trans (HfB _ z₁)
     exact fixpointA_ne.ne HfA HfB
 
 end FixpointAB