# HG changeset patch
# User ryokka
# Date 1577448602 -32400
# Node ID 083a18424f759a9e4b244cf939cff988ad6b927d
# Parent  8ec3fca60fde4b02e08c941f53e7055fda982e4a
fix

diff -r 8ec3fca60fde -r 083a18424f75 whileTestGears.agda
--- a/whileTestGears.agda	Thu Dec 26 20:04:49 2019 +0900
+++ b/whileTestGears.agda	Fri Dec 27 21:10:02 2019 +0900
@@ -217,27 +217,27 @@
   → (next : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP s2 output)  → t)
   → (exit : (output : Envc ) → (whileTestStateP s2 input ) implies (whileTestStateP sf output)  → t) → t
 whileLoopPSem' env@(record { c10 = c10 ; varn = zero ; vari = vari }) s next exit = exit env (proof (λ z → z))
-whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → z))
+whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → {!!}))
 
 
 loopPP : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
 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)
+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 output eq with <-cmp 0 (Envc.varn input)
-    lem output refl | tri< a ¬b ¬c = lem {!!} {!!}
-    lem output refl | tri≈ ¬a refl ¬c = s2p
+    -- lem : (output : Envc) → loopPP (varn input) input refl ≡ output → Envc.vari (loopPP (Envc.varn input) input refl) ≡  Envc.c10 output
+    -- lem output eq with <-cmp 0 (Envc.varn input)
+    -- lem output refl | tri< a ¬b ¬c = {!!}
+    -- 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 (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 zero current refl loopeq refl rewrite loopeq = proof (λ x → x) -- proof (λ x → lem {!!} {!!})
+    loopPPSemInduct (suc n) current refl loopeq s2p  with <-cmp 0 (suc n)
+    loopPPSemInduct (suc n) current refl loopeq refl | tri< a ¬b ¬c = {!!}
+    -- 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 = {!!}