# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1672030857 -32400
# Node ID c90eec304cfa5eeca85008139c58ec8488b53bdf
# Parent  c2501d308c95820cfa005ecf3e36a70c6ef8315c
PFOD

diff -r c2501d308c95 -r c90eec304cfa src/ODUtil.agda
--- a/src/ODUtil.agda	Sun Dec 25 10:12:56 2022 +0900
+++ b/src/ODUtil.agda	Mon Dec 26 14:00:57 2022 +0900
@@ -184,15 +184,17 @@
                lemma :  nat→ω (ω→nato ltd) ≡ * x₁
                lemma = trans  (cong (λ k →  nat→ω  k) (lemma2 {x₁} {_} ltd (subst (λ k → infinite-d k ) (sym &iso) ltd)  &iso ) ) ( prev {* x₁} lemma0 lemma1 )
 
+                                                   
+ω→nat-iso0 : (x : Nat) → {ox : Ordinal } → (ltd : infinite-d ox) → * ox ≡ nat→ω x → ω→nato ltd ≡ x                                  
+ω→nat-iso0 Zero iφ eq = refl                                                                                                     
+ω→nat-iso0 (Suc x) iφ eq = ⊥-elim ( ωs≠0 _ (trans (sym eq) o∅≡od∅ )) 
+ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (subst (λ k → k ≡ od∅  ) *iso eq ))
+ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where
+       lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
+       lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
+            ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
+                (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
+
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = lemma i (ω∋nat→ω {i}) *iso where
-   lemma : {x : Ordinal } → ( i : Nat ) → (ltd : infinite-d x ) → * x ≡  nat→ω i → ω→nato ltd ≡ i
-   lemma {x} Zero iφ eq = refl
-   lemma {x} (Suc i) iφ eq = ⊥-elim ( ωs≠0 (nat→ω i) (trans (sym eq) o∅≡od∅ )) -- Union (nat→ω i , (nat→ω i , nat→ω i)) ≡ od∅
-   lemma Zero (isuc {x} ltd) eq = ⊥-elim ( ωs≠0 (* x) (subst (λ k → k ≡ od∅  ) *iso eq ))
-   lemma (Suc i) (isuc {x} ltd) eq = cong (λ k → Suc k ) (lemma i ltd (lemma1 eq) )  where -- * x ≡ nat→ω i
-           lemma1 :  * (& (Union (* x , (* x , * x)))) ≡ Union (nat→ω i , (nat→ω i , nat→ω i)) → * x ≡ nat→ω i
-           lemma1 eq = subst (λ k → * x ≡ k ) *iso (cong (λ k → * k)
-                ( ω-prev-eq (subst (λ k → _ ≡ k ) &iso (cong (λ k → & k ) (sym
-                    (subst (λ k → _ ≡ Union ( k , ( k , k ))) (sym *iso ) eq ))))))
+ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso  
 
diff -r c2501d308c95 -r c90eec304cfa src/PFOD.agda
--- a/src/PFOD.agda	Sun Dec 25 10:12:56 2022 +0900
+++ b/src/PFOD.agda	Mon Dec 26 14:00:57 2022 +0900
@@ -138,13 +138,33 @@
     le02 : infinite ∋ * x
     le02 = power→ infinite _ lt (subst (λ k → odef X k) (sym &iso) Xx) 
     le01 : (wx : odef infinite (& (* x))) → ω2→f X lt (ω→nat (* x) wx) ≡ i1
-    le01 wx  = ?
+    le01 wx   with ODC.∋-p O X (nat→ω (ω→nat _ wx) )
+    ... | yes p  = refl
+    ... | no ¬p  = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where
+        le03 :  x ≡ & (nat→ω (ω→nato wx))
+        le03 = subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
+
+¬i0≡i1 : ¬ ( i0 ≡ i1 )
+¬i0≡i1 ()
+
+¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 
+¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
+¬i0→i1 {i1} ne = refl
+
+¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
+¬i1→i0 {i0} ne = refl
+¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
 
 fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f
-fω→2-iso f = f-extensionality le01 where
+fω→2-iso f = f-extensionality (λ x → le01 x ) where
     le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
-    le01 Zero = ?
-    le01 (Suc x) = ?
+    le01 x with  ODC.∋-p O (fω→2 f) (nat→ω x) 
+    le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where
+        le02 :  infinite-d (& (* (& (nat→ω x))))
+        le02 = proj1 (proj2 p )
+    le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where
+        le04 : ¬ f x ≡ i1
+        le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → infinite-d k) (sym &iso) (ω∋nat→ω {x})  , le05 ⟫ ⟫ where
+            le05 : (lt : infinite-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
+            le05 lt = trans (cong f (ω→nat-iso0 x lt (trans *iso *iso))) fx=1
 
-
-