# HG changeset patch
# User ryokka
# Date 1577349596 -32400
# Node ID 52acd110df185e9a0fafd0b2bc127e41ad456012
# Parent  66ba3b1eec0a1aec5ca80281fd68079c3bc6d6cd
fix

diff -r 66ba3b1eec0a -r 52acd110df18 whileTestGears.agda
--- a/whileTestGears.agda	Wed Dec 25 17:15:17 2019 +0900
+++ b/whileTestGears.agda	Thu Dec 26 17:39:56 2019 +0900
@@ -211,11 +211,6 @@
 whileLoopPSem env s next exit | tri≈ ¬a b ¬c rewrite (sym b) = exit env (proof (λ z → z))
 whileLoopPSem env s next exit | tri< a ¬b ¬c  = next env (proof (λ z → z))
 
-{-# TERMINATING #-}
-loopPP : (input : Envc ) → Envc
-loopPP input with <-cmp 0 (varn input)
-loopPP input | tri≈ ¬a b ¬c = input
-loopPP input | tri< a ¬b ¬c = loopPP (whileLoopP input (λ next → loopPP next) (λ output → output))
 
 
 whileLoopPSem' : {l : Level} {t : Set l}   → (input : Envc ) → whileTestStateP s2 input
@@ -225,21 +220,23 @@
 whileLoopPSem' env@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) s next exit = next env (proof (λ z → z))
 
 
-loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
-loopPP' n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+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)
 
--- Maybe "Z-Conbinater"
--- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
+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
+  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 = {!!}
 
-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)
 
 
 lpc : (input : Envc ) → Envc
 lpc input@(record { c10 = c10 ; varn = zero ; vari = vari }) = input
-
--- Maybe "Z-Conbinater"
--- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
-
 lpc input@(record { c10 = c10 ; varn = (suc varn₁) ; vari = vari }) = whileLoopP (record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ x → lpc record { c10 = c10 ; varn = (varn₁) ; vari = vari }) (λ output → output)
 
 
@@ -255,10 +252,11 @@
 whileLoopPSemSound : (input output : Envc )
    → whileTestStateP s2 input
    →  output ≡ lpc input
-   -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound input output pre refl with (lpc input)
-whileLoopPSemSound record { c10 = c11 ; varn = varn₁ ; vari = vari₁ } .(lpc (record { c10 = c11 ; varn = varn₁ ; vari = vari₁ })) pre refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof λ x → {!!}
+whileLoopPSemSound input output pre eq = {!!}
+
+-- with (lpc input)
+-- record { c10 = c11 ; varn = varn₁ ; vari = vari₁ } .(lpc (record { c10 = c11 ; varn = varn₁ ; vari = vari₁ })) pre refl | record { c10 = c10 ; varn = varn ; vari = vari } = proof λ x → {!!}
   -- where
   --   lem : (whileTestStateP s2 input ) → (varn input + vari input ≡ c10 input)
   --     implies (vari output ≡ c10 output)