# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1615717131 -32400
# Node ID bf50676c77af5a40615f7881c944bf1dd774ad88
# Parent  0e87089e5de464a8e8e4b9cef15949727c50a6a5
...

diff -r 0e87089e5de4 -r bf50676c77af agda/halt.agda
--- a/agda/halt.agda	Sun Mar 14 15:31:56 2021 +0900
+++ b/agda/halt.agda	Sun Mar 14 19:18:51 2021 +0900
@@ -150,16 +150,17 @@
      ntol (suc n) = ntol1 n
      xx :   (x : ℕ ) → List Bool ∧ ℕ
      xx x = ⟪ (ntol x) , lton ((ntol x))  ⟫
+     ---- div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
      lbiso1 :  (x : ℕ) → suc (lton1 (ntol1 x)) ≡ suc x
      lbiso1 zero = refl
-     lbiso1 (suc x) with div2 (suc x)
-     ... | ⟪ x1 , true ⟫ = begin
+     lbiso1 (suc x) with div2 (suc x) | inspect div2 (suc x)
+     ... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin
          suc (suc (lton1 (ntol1 x1) + lton1 (ntol1 x1))) ≡⟨ {!!} ⟩
          suc (lton1 (ntol1 x1)) + suc (lton1 (ntol1 x1)) ≡⟨ cong ( λ k → k + k ) (lbiso1 x1) ⟩
          suc x1 + suc x1 ≡⟨ {!!} ⟩
          suc (suc (x1 + x1)) ≡⟨ {!!} ⟩
          suc (suc x) ∎ 
-     ... | ⟪ x1 , false ⟫ = {!!}
+     ... | ⟪ x1 , false ⟫ | record { eq = eq1 } = {!!}
      lbiso0 :  (x : ℕ) → lton (ntol x)  ≡ x
      lbiso0 zero = refl
      lbiso0 (suc zero) = refl
diff -r 0e87089e5de4 -r bf50676c77af agda/nat.agda
--- a/agda/nat.agda	Sun Mar 14 15:31:56 2021 +0900
+++ b/agda/nat.agda	Sun Mar 14 19:18:51 2021 +0900
@@ -66,6 +66,29 @@
 div2 (suc (suc n)) =  ⟪ suc (proj1 (div2 n)) , proj2 (div2 n) ⟫ where
     open _∧_
 
+div2-rev : (ℕ ∧ Bool ) → ℕ
+div2-rev ⟪ x , true ⟫ = suc (x + x)
+div2-rev ⟪ x , false ⟫ = x + x
+
+div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x
+div2-eq zero = refl
+div2-eq (suc zero) = refl
+div2-eq (suc (suc x)) with div2 x | inspect div2 x 
+... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫
+     div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩
+     suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1  _ ) ⟩
+     suc (suc (suc (x1 + x1))) ≡⟨⟩    
+     suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 
+     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 
+     suc (suc x) ∎  where open ≡-Reasoning
+... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin
+     div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩
+     suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1  _ ) ⟩
+     suc (suc (x1 + x1)) ≡⟨⟩    
+     suc (suc (div2-rev ⟪ x1 , false ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ 
+     suc (suc (div2-rev (div2 x)))      ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ 
+     suc (suc x) ∎  where open ≡-Reasoning
+
 minus : (a b : ℕ ) →  ℕ
 minus a zero = a
 minus zero (suc b) = zero
@@ -107,14 +130,6 @@
            suc x
         ∎  where open ≡-Reasoning
 
--- open import Relation.Binary.PropositionalEquality
-
--- postulate extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
-
--- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ }  → (A a b → B a b ) → (B a b → A a b ) → A ≡ B
--- <-≡-iff {A} {B} ab ba = {!!}
-
-
 0<s : {x : ℕ } → zero < suc x
 0<s {_} = s≤s z≤n 
 
@@ -187,21 +202,6 @@
 minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n
 minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt
 
--- open import Level hiding (suc ; zero)
--- record Mind {l : Level} ( P : ℕ → Set l ) : Set (Level.suc l) where
---   field 
---      diff : ℕ
---      mind : ( n : ℕ ) → P n → P (n + diff)
-
--- minus-induction : { P : ℕ → Set } → Mind P → P zero → (n : ℕ) → P n
--- minus-induction {P} mi p0 n = mi1 n n ≤-refl  where
---     mi1 : (n n1 : ℕ) → n ≤ n1  → P n
---     mi1 zero _ _ = p0
---     mi1 (suc n) n1 n≤n1 with <-cmp (n1 + Mind.diff mi) n
---     ... | tri< a ¬b ¬c = {!!}
---     ... | tri≈ ¬a refl ¬c = {!!}
---     ... | tri> ¬a ¬b c = {!!}
-
 open import Relation.Binary.Definitions
 
 distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z)