# HG changeset patch
# User ryokka
# Date 1577351795 -32400
# Node ID 6f26de2fb7fe15a3de21e568a264b24051c8bac5
# Parent  52acd110df185e9a0fafd0b2bc127e41ad456012
...

diff -r 52acd110df18 -r 6f26de2fb7fe whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 26 17:39:56 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 18:16:35 2019 +0900
@@ -224,14 +224,17 @@
 loopPP n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
 loopPP n input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → loopPP (n - 1)  (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) refl) (λ output → output)
 
-loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) → loopPP (varn input)  input refl ≡  output
-  → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
-loopPPSem {l} {t} input output refl = loopPPSemInduct (varn input) input refl
+loopPPSem : {l : Level} {t : Set l} → (input output : Envc ) →  output ≡ loopPP (varn input)  input refl
+  → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
+loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input refl s2p (proof (λ x → {!!}))
   where
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n  → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
-    loopPPSemInduct zero current refl = proof λ x → {!!}
-    loopPPSemInduct (suc n) current refl with whileLoopPSem current {!!} {!!} {!!}
-    ... | aa = {!!}
+    -- lem1 :  (ncurrent : Envc) → suc (varn ncurrent) + vari ncurrent ≡ c10 ncurrent → varn ncurrent + suc (vari ncurrent) ≡ c10 ncurrent
+    -- lem1 current eq = {!!}
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n → (whileTestStateP s2 current ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct zero current refl refl imp with loopPP (varn current) current refl -- = proof λ x → {!!}
+    loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl refl imp | record { c10 = c10 ; varn = varn ; vari = vari } = proof {!!}
+    loopPPSemInduct (suc n) current refl s2p imp with <-cmp 0 (suc n) | whileLoopPSem current s2p (λ output x → proof {!!}) λ output x → proof λ x₁ → {!!}
+    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl s2p imp | tri< a ¬b ¬c | proof x = {!!}