# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1625316029 -32400
# Node ID e423b498f3febeaa360be02242ad536ac08dd789
# Parent  a9fc3ece852a54cadbd3bc6e77fed8b4badf5cd5
...

diff -r a9fc3ece852a -r e423b498f3fe src/HyperReal.agda
--- a/src/HyperReal.agda	Sat Jul 03 14:27:01 2021 +0900
+++ b/src/HyperReal.agda	Sat Jul 03 21:40:29 2021 +0900
@@ -49,7 +49,11 @@
      n→nxn (suc i) with n→nxn i
      ... | ⟪ x , zero ⟫ = ⟪ zero  , suc x ⟫
      ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫
-     nid1 : (i : ℕ) → 0 < proj2 ( n→nxn i)  → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
+     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
+     nid1 : (i : ℕ) → 0 < proj2 (n→nxn i) → n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
      nid1 (suc i) 0<p2 with  n→nxn (suc i) 
      ... | ⟪ x , zero ⟫ = ⊥-elim ( nat-≤> 0<p2 a<sa )
      ... | ⟪ x , suc y ⟫ = refl
@@ -64,6 +68,8 @@
           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} )
+     nid20 : (i : ℕ) →  i +  (nxn→n 0 i) ≡ nxn→n i 0
+     nid20 i = {!!}
      nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
      nid2 zero zero = refl
      nid2 zero (suc j) = refl
@@ -92,10 +98,47 @@
      nid6 {suc i} 0<i = refl
      n-id :  (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i
      n-id 0 = refl
-     n-id (suc i) with proj2 (n→nxn (suc i))  | inspect  proj2 (n→nxn (suc i))
-     ... | zero  | record { eq = eq } = {!!}
-     ... | suc x | record { eq = eq } with  proj2 (n→nxn i) | inspect proj2 (n→nxn i) 
-     ... | zero  | record { eq = eqy } = {!!}
+     n-id (suc i) with proj2 (n→nxn (suc i))  | inspect  proj2 (n→nxn (suc i))  -- ⟪ pred n , 1 ⟫  → ⟪ n , 0 ⟫
+     ... | zero  | record { eq = eq } with  proj1 (n→nxn (suc i)) | inspect  proj1 (n→nxn (suc i))
+     ... | zero | record { eq = eqx } = {!!}
+     ... | suc x | record { eq = eqx } with proj2 (n→nxn i) | inspect  proj2 (n→nxn i)
+     -- i +  (nxn→n 0 i) ≡ nxn→n i 0
+     ... | zero | record { eq = eqy } = begin
+          suc (x + suc (nxn→n x 0)) ≡⟨ {!!}  ⟩
+         suc (nxn→n (proj1 (n→nxn i)) 0) ≡⟨ cong (λ k → suc (nxn→n (proj1 (n→nxn i)) k)) (sym eqy) ⟩
+         suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
+         suc i ∎ where
+             open ≡-Reasoning
+     ... | suc y | record { eq = eqy } = begin
+         nxn→n (suc x) 0 ≡⟨ sym (nid2 x 0) ⟩
+         suc (nxn→n x 1)  ≡⟨ cong₂ (λ j k → suc (nxn→n j k) ) nid9 nid10 ⟩
+         suc (nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i))) ≡⟨ cong suc (n-id i) ⟩
+         suc i ∎   where
+             open ≡-Reasoning
+             nid11 : 0 < proj2 (n→nxn i)
+             nid11 = subst (λ k → 0 < k ) (sym eqy) (s≤s z≤n)
+             nid9 :  x ≡ proj1 (n→nxn i)
+             nid9 = begin
+               x ≡⟨ sym (cong pred eqx) ⟩
+               pred (proj1 (n→nxn (suc i))) ≡⟨ cong pred (cong proj1  (nid1 i nid11)) ⟩
+               pred (suc (proj1 (n→nxn i)))  ≡⟨ refl  ⟩
+               proj1 (n→nxn i)  ∎   
+             nid10 :  1 ≡ proj2 (n→nxn i)
+             nid10 = begin
+               1  ≡⟨ cong suc (sym eq) ⟩
+               suc ( proj2 (n→nxn (suc i)))  ≡⟨ cong suc (cong proj2  (nid1 i nid11)) ⟩
+               suc (pred (proj2 (n→nxn i))) ≡⟨ nid6 nid11 ⟩
+               proj2 (n→nxn i)  ∎   
+     n-id (suc i) | suc x | record { eq = eq } with  proj2 (n→nxn i) | inspect proj2 (n→nxn i)  -- ⟪ x , 0 ⟫ → ⟪ 0 , suc x ⟫
+     -- eqy : proj2 (n→nxn i) ≡ zero
+     -- eq  : proj2 (n→nxn (suc i) | n→nxn i) ≡ suc x
+     ... | zero  | record { eq = eqy } = begin
+          nxn→n (proj1 (n→nxn (suc i) )) (suc x) ≡⟨ {!!} ⟩
+          nxn→n zero (suc x) ≡⟨ {!!} ⟩
+          x + suc (nxn→n 0 x) ≡⟨ {!!} ⟩
+          x + suc (nxn→n 0 (pred (proj1 (n→nxn i)))) ≡⟨ {!!} ⟩
+          suc i ∎ where
+             open ≡-Reasoning
      ... | suc y | record { eq = eqy } = begin
           nxn→n (proj1 (n→nxn (suc i))) (suc x)   ≡⟨ cong (λ k → nxn→n (proj1 k) (suc x)) (nid1 i nid7 ) ⟩
           nxn→n (suc (proj1 (n→nxn i))) (suc x)   ≡⟨ sym (nid2 (proj1 (n→nxn i)) (suc x) ) ⟩
@@ -118,6 +161,8 @@
      f i = n→nxn (suc i) ≡ ⟪ suc (proj1 ( n→nxn i )) , pred ( proj2 ( n→nxn i )) ⟫
      g : (i j : ℕ) → Set
      g i j = suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j 
+     h : (i : ℕ) → Set
+     h i = i +  (nxn→n 0 i) ≡ nxn→n i 0
      nn-id : (i j : ℕ) → n→nxn (nxn→n i j) ≡ ⟪ i , j ⟫
      nn-id = {!!}