From 7dc5c9696ee7b73f1b714e3de33226b1def7b966 Mon Sep 17 00:00:00 2001
From: chi-p-3141 <232381255+chi-p-3141@users.noreply.github.com>
Date: Sat, 28 Feb 2026 18:53:07 +0100
Subject: [PATCH] changed dirCycle.pmap definition filled in 'sorry' for
 dirCycle.is_well_defined

---
 DGAlgorithms/Models/PortNumbering.lean | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

diff --git a/DGAlgorithms/Models/PortNumbering.lean b/DGAlgorithms/Models/PortNumbering.lean
index d7afbe5..0d1991f 100644
--- a/DGAlgorithms/Models/PortNumbering.lean
+++ b/DGAlgorithms/Models/PortNumbering.lean
@@ -274,16 +274,29 @@ end Examples
 
 def dirCycle (n : ℕ) : PNNetwork (Fin (n+2)) where
   deg := fun _ ↦ 2
-  pmap := fun p ↦ (ite (p.port == 0) (p.node+1) (p.node-1), ite (p.port == 0) 1 0)
+  pmap := fun p ↦ match p.2 with
+  | 0 => (p.node-1,1)
+  | 1 => (p.node+1,0)
+  | _ => p
   pmap_involutive := by
     intro v i hi
     have hi : i = 0 ∨ i = 1 := by grind
     cases' hi with hi hi
     all_goals grind
   is_well_defined := by
-    intro vp
-
-    sorry
+    intro vp hfun
+    let (node,port) := vp
+    simp [Port.port]
+    simp [Port.port, Port.node] at hfun
+    cases port with
+    | zero => linarith
+    | succ k => cases k with
+      | zero => linarith
+      | succ w =>
+        have h0 : (w+1+1≠0) := by linarith
+        have h1 : (w+1+1≠1) := by linarith
+        simp at hfun
+        contradiction
 
 -- def fooboar (A : Type*) : PNAlgorithm A A where
 --   Msg := Unit