# HG changeset patch
# User ryokka
# Date 1577352867 -32400
# Node ID d45e98211d7df844f79ae5a38a0602e90bf77ae3
# Parent  6f26de2fb7fe15a3de21e568a264b24051c8bac5
...

diff -r 6f26de2fb7fe -r d45e98211d7d whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 26 18:16:35 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 18:34:27 2019 +0900
@@ -226,15 +226,14 @@
 
 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 → {!!}))
+loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
   where
-    -- 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 = {!!}
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n →  output ≡ loopPP n  current {!!}
+      → (whileTestStateP s2 current ) → (whileTestStateP s2 current ) implies (whileTestStateP sf output)
+    loopPPSemInduct zero current refl eq refl with loopPP (varn current) current refl -- = proof λ x → {!!}
+    loopPPSemInduct zero record { c10 = _ ; varn = _ ; vari = _ } refl eq refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof (λ x → {!!})
+    loopPPSemInduct (suc n) current refl eq s2p 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 eq s2p | tri< a ¬b ¬c | proof x = {!!}