# HG changeset patch
# User ryokka
# Date 1577358289 -32400
# Node ID 8ec3fca60fde4b02e08c941f53e7055fda982e4a
# Parent  cf00bc7af3695acedac5896142e28d6eca065718
...

diff -r cf00bc7af369 -r 8ec3fca60fde whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 26 19:00:40 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 20:04:49 2019 +0900
@@ -221,23 +221,23 @@
 
 
 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-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)
+loopPP zero input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+loopPP (suc n) input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) refl = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → loopPP n  (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) refl) (λ output → output)
 
 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 refl s2p
   where
     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 = {!!}
+    lem output eq with <-cmp 0 (Envc.varn input)
+    lem output refl | tri< a ¬b ¬c = lem {!!} {!!}
+    lem output refl | tri≈ ¬a refl ¬c = s2p
     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 = 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) 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 → {!!}
+    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | proof x = proof λ x₁ → {!!}
 
 --    loopPPSemInduct (suc n) record { c10 = _ ; varn = .(suc n) ; vari = _ } refl eq s2p | tri< a ¬b ¬c | aa = {!!}