From 8abb1b5601fabf5e7560d08faa6e633e60663e0a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 29 Apr 2021 20:58:04 +0100
Subject: Finally prove that e [ μ e / zero ] ≈ μ e.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Complete proof of generator.
---
 src/Cfe/Type/Properties.agda | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'src/Cfe/Type')

diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 21051c0..4b38c1e 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -16,7 +16,6 @@ open Setoid over using ()
   )
 
 open import Algebra
-open import Cfe.Function.Power
 open import Cfe.Language over
   hiding
   ( _≉_; ≈-refl; ≈-trans; ≈-isPartialEquivalence; ≈-isEquivalence; partialSetoid; setoid
@@ -356,19 +355,20 @@ setoid {fℓ} {lℓ} = record { isEquivalence = ≈-isEquivalence {fℓ} {lℓ}
   ; l⇒l = λ (x , w , (m , xw∈Fᵐ) , w′ , n , xwcw′∈Fⁿ) →
     Fⁿ⊨τ.l⇒l
       (m + n)
-      (-, -, ∈-resp-⊆ (step (m≤m+n m n)) xw∈Fᵐ , -, ∈-resp-⊆ (step (m≤n+m n m)) xwcw′∈Fⁿ)
+      ( x
+      , w
+      , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤m+n m n)) xw∈Fᵐ
+      , w′
+      , ∈-resp-⊆ (Iter-monoʳ mono (⊆-min (F ∅)) (m≤n+m n m)) xwcw′∈Fⁿ
+      )
   }
   where
-  Fⁿ⊨τ : ∀ n → (F ^ n) ∅ ⊨ τ
+  Fⁿ⊨τ : ∀ n → Iter F ∅ n ⊨ τ
   Fⁿ⊨τ zero    = ⊨-min τ
   Fⁿ⊨τ (suc n) = ⊨-step (Fⁿ⊨τ n)
 
   module Fⁿ⊨τ n = _⊨_ (Fⁿ⊨τ n)
 
-  step : ∀ {m n} → m ≤ⁿ n → (F ^ m) ∅ ⊆ (F ^ n) ∅
-  step {n = n} z≤n       = ⊆-min ((F  ^ n) ∅)
-  step         (s≤s m≤n) = mono (step m≤n)
-
 ------------------------------------------------------------------------
 -- Properties of _⊛_
 ------------------------------------------------------------------------
-- 
cgit v1.2.3