# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625442920 -32400
# Node ID 7264f87493691f5c26477b62f47272215592b297
# Parent  4b3dfce33fa3eb01643dd273c6d602ada0ae435f
... uniquness

diff -r 4b3dfce33fa3 -r 7264f8749369 src/HyperReal.agda
--- a/src/HyperReal.agda	Mon Jul 05 00:46:17 2021 +0900
+++ b/src/HyperReal.agda	Mon Jul 05 08:55:20 2021 +0900
@@ -44,6 +44,7 @@
 i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0
 i≤0→i≡0 {0} z≤n = refl
 
+
 nxn : NxN
 nxn = record {
      nxn→n = λ p → nxn→n (proj1 p) (proj2 p)
@@ -76,6 +77,42 @@
          suc (i + suc (i + nxn→n 0 i)) ≡⟨ cong ( λ k → suc (i + suc k)) (nid20 i)  ⟩
          suc (i + suc (nxn→n i 0)) ∎  where open ≡-Reasoning
 
+     nid4 : {i j : ℕ} →  i + 1 + j ≡ i + suc j
+     nid4 {zero} {j} = refl
+     nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
+     nid5 : {i j k : ℕ} →  i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
+     nid5 {zero} {j} {k} = begin
+          suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
+          1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
+          (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
+          suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
+          suc j + suc (suc k) ∎ where open ≡-Reasoning
+     nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
+
+     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
+     nid2 zero zero = refl
+     nid2 zero (suc j) = refl
+     nid2 (suc i) zero = begin
+          suc (nxn→n (suc i) 1)  ≡⟨ refl ⟩
+          suc (suc (i + 1 + suc (nxn→n i 1)))  ≡⟨ cong (λ k → suc (suc k)) nid4  ⟩
+          suc (suc (i + suc (suc (nxn→n i 1))))  ≡⟨ cong (λ k →  suc (suc (i + suc (suc k)))) (nid3 i) ⟩
+          suc (suc (i + suc (suc (i + suc (nxn→n i 0)))))  ≡⟨ refl ⟩
+          nxn→n (suc (suc i)) zero ∎ where
+             open ≡-Reasoning
+             nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
+             nid3 zero = refl
+             nid3 (suc i) = begin
+                 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
+                 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
+                 suc (i + suc (suc (i + suc (nxn→n i 0))))
+              ∎
+     nid2 (suc i) (suc j) = begin
+          suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
+          suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
+          suc (suc (i + suc (suc j) + suc      (i + suc j + suc (nxn→n i (suc j)))))  ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
+          suc (suc (i + suc j       + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
+          nxn→n (suc (suc i)) (suc j) ∎ where
+             open ≡-Reasoning
      nn : ( i  : ℕ) → NN i nxn→n n→nxn
      nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl
         ;  nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) }
@@ -117,8 +154,19 @@
                suc 0 ≤⟨ s≤s z≤n  ⟩
                suc y ≡⟨ sym (cong proj2 eq1) ⟩
                proj2 (n→nxn i)  ∎ ))  where open ≤-Reasoning
+            --  nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
             nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫
-            nn04 = ?
+            nn04 {zero} {suc k0} eq = {!!} -- k0 + suc (nxn→n zero k0) ≡ suc i -- 
+            nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where
+               nn05 : nxn→n j0 (suc k0) ≡ i
+               nn05 = begin
+                  nxn→n j0 (suc k0)  ≡⟨ cong pred ( begin 
+                    suc (nxn→n j0 (suc k0))  ≡⟨ nid2 j0 k0 ⟩
+                    nxn→n (suc j0) k0  ≡⟨ eq1 ⟩
+                    suc i ∎ ) ⟩
+                  i ∎   where open ≡-Reasoning 
+               nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ 
+               nn06 = NN.nn-unique (nn i)
      ... | suc k  | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = {!!} ; ni = {!!}
          ; k1 = {!!} ; k0 = {!!} ;  nn-unique = {!!} }
 
@@ -135,47 +183,12 @@
      nid1 (suc i) 0<p2 with  n→nxn (suc i) 
      ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa )
      ... | ⟪ x , suc y ⟫ = refl
-     nid4 : {i j : ℕ} →  i + 1 + j ≡ i + suc j
-     nid4 {zero} {j} = refl
-     nid4 {suc i} {j} = cong suc (nid4 {i} {j} )
-     nid5 : {i j k : ℕ} →  i + suc (suc j) + suc k ≡ i + suc j + suc (suc k )
-     nid5 {zero} {j} {k} = begin
-          suc (suc j) + suc k ≡⟨ +-assoc 1 (suc j) _ ⟩
-          1 + (suc j + suc k) ≡⟨ +-comm 1 _ ⟩
-          (suc j + suc k) + 1 ≡⟨ +-assoc (suc j) (suc k) _ ⟩
-          suc j + (suc k + 1) ≡⟨ cong (λ k → suc j + k ) (+-comm (suc k) 1) ⟩
-          suc j + suc (suc k) ∎ where open ≡-Reasoning
-     nid5 {suc i} {j} {k} = cong suc (nid5 {i} {j} {k} )
      nid0 : (i : ℕ) → 0 ≡ proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ 0 , suc ( proj1 ( n→nxn i )) ⟫
      nid0 zero eq = refl
      nid0 (suc i) eq with n→nxn (suc i)
      ... | ⟪ x , zero ⟫ = refl
      nid-case0 : (i : ℕ) → suc (pred (proj2 (n→nxn (suc i))) + suc (nxn→n ( pred (proj2 (n→nxn (suc i)))) 0)) ≡ suc (nxn→n (proj1 (n→nxn i)) 0) 
      nid-case0 = {!!}
-     nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
-     nid2 zero zero = refl
-     nid2 zero (suc j) = refl
-     nid2 (suc i) zero = begin
-          suc (nxn→n (suc i) 1)  ≡⟨ refl ⟩
-          suc (suc (i + 1 + suc (nxn→n i 1)))  ≡⟨ cong (λ k → suc (suc k)) nid4  ⟩
-          suc (suc (i + suc (suc (nxn→n i 1))))  ≡⟨ cong (λ k →  suc (suc (i + suc (suc k)))) (nid3 i) ⟩
-          suc (suc (i + suc (suc (i + suc (nxn→n i 0)))))  ≡⟨ refl ⟩
-          nxn→n (suc (suc i)) zero ∎ where
-             open ≡-Reasoning
-             nid3 : (i : ℕ) → nxn→n i 1 ≡ i + suc (nxn→n i 0)
-             nid3 zero = refl
-             nid3 (suc i) = begin
-                 suc (i + 1 + suc (nxn→n i 1)) ≡⟨ cong suc nid4 ⟩
-                 suc (i + suc (suc (nxn→n i 1))) ≡⟨ cong (λ k →  suc (i + suc (suc k))) (nid3 i) ⟩
-                 suc (i + suc (suc (i + suc (nxn→n i 0))))
-              ∎
-     nid2 (suc i) (suc j) = begin
-          suc (nxn→n (suc i) (suc (suc j)))  ≡⟨ refl ⟩
-          suc (suc (i + suc (suc j) + suc (nxn→n i (suc (suc j)))))  ≡⟨ cong (λ k → suc (suc (i + suc (suc j) + k))) (nid2 i (suc j)) ⟩
-          suc (suc (i + suc (suc j) + suc      (i + suc j + suc (nxn→n i (suc j)))))  ≡⟨ cong ( λ k → suc (suc k)) nid5 ⟩
-          suc (suc (i + suc j       + suc (suc (i + suc j + suc (nxn→n i (suc j)))))) ≡⟨ refl ⟩
-          nxn→n (suc (suc i)) (suc j) ∎ where
-             open ≡-Reasoning
      nid6 : {i : ℕ } → 0 < i  → suc (pred i) ≡ i
      nid6 {suc i} 0<i = refl
      n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i