# HG changeset patch
# User ryokka
# Date 1577354440 -32400
# Node ID cf00bc7af3695acedac5896142e28d6eca065718
# Parent  d45e98211d7df844f79ae5a38a0602e90bf77ae3
...

diff -r d45e98211d7d -r cf00bc7af369 whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 26 18:34:27 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 19:00:40 2019 +0900
@@ -228,12 +228,18 @@
   → (whileTestStateP s2 input ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)
 loopPPSem {l} {t} input output refl s2p = loopPPSemInduct (varn input) input  refl refl s2p
   where
-    loopPPSemInduct : (n : ℕ) → (current : Envc) → varn current ≡ n →  output ≡ loopPP n  current {!!}
+    lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡  Envc.c10 output
+    lem eq with <-cmp 0 (Envc.varn input)
+    lem record { c10 = c10 ; varn = varn ; vari = vari } | aa = {!!}
+    loopPPSemInduct : (n : ℕ) → (current : Envc) → (eq : n ≡ varn current) →  output ≡ loopPP n  current eq
       → (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 = {!!}
+    loopPPSemInduct zero current refl eq refl = proof (λ x → lem {!!} {!!})
+    -- loopPPSemInduct zero curernt refl refl refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof (λ x → lem {!!})
+    loopPPSemInduct (suc n) current refl eq s2p with <-cmp 0 (suc n)
+    loopPPSemInduct (suc n) current refl eq s2p | tri< a ¬b ¬c with whileLoopPSem {_} {(whileTestStateP s2 current) implies (whileTestStateP s2 output )} current s2p (λ output x → {!!}) λ output x → {!!}
+    ... | aa = {!!}
+
+--    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | aa = {!!}