--- a/whileTestGears.agda	Tue Dec 24 17:28:06 2019 +0900
+++ b/whileTestGears.agda	Wed Dec 25 17:15:17 2019 +0900
@@ -123,8 +123,8 @@
      next (record env {varn = (varn env) - 1 ; vari = (vari env) + 1 })
 
 whileLoopP' : {l : Level} {t : Set l} → Envc → (next : Envc → t) → (exit : Envc → t) → t
-whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = zero } next exit = exit env
-whileLoopP' env@record { c10 = c10 ; varn = varn ; vari = (suc vari₁) } next exit = next (record env {varn = varn - 1 ; vari = (suc vari₁) + 1 })
+whileLoopP' env@record { c10 = c10 ; varn = zero ; vari = vari } next exit = exit env
+whileLoopP' env@record { c10 = c10 ; varn = (suc varn1) ; vari = vari } next exit = next (record env {varn = varn1 ; vari = vari + 1 })
 
 -- whileLoopP env next exit | tri≈ ¬a b ¬c = exit env
 -- whileLoopP env next exit | tri< a ¬b ¬c =
@@ -218,14 +218,55 @@
 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
+  → (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))
+
+
+loopPP' : (n : ℕ) → (input : Envc ) → (n ≡ varn input) → Envc
+loopPP' n input@(record { c10 = c10 ; varn = zero ; vari = vari }) refl = input
+
+-- Maybe "Z-Conbinater"
+-- Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
+
+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)
+
+
+
+
+-- loopPP' input | tri≈ ¬a b ¬c = input
+-- loopPP' input | tri< a ¬b ¬c = whileLoopP input (λ enext → loopPP' enext) (λ eout → eout)
+-- loopPP' (whileLoopP input (λ next → loopPP' next) (λ output → output))
+
+
 -- = whileLoopP input (λ next → loopPP next ) (λ output → output )
 
 whileLoopPSemSound : (input output : Envc )
    → whileTestStateP s2 input
-   →  output ≡ loopPP input
+   →  output ≡ lpc input
    -- (whileLoopP input (λ tt → whileLoopP tt {!!} {!!}) {!!}) ← y-conbinater
    → (whileTestStateP s2 input ) implies ( whileTestStateP sf output )
-whileLoopPSemSound input output pre eq = whileLoopPSem input pre {!!} {!!} -- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
+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 → {!!}
+  -- where
+  --   lem : (whileTestStateP s2 input ) → (varn input + vari input ≡ c10 input)
+  --     implies (vari output ≡ c10 output)
+  --   lem refl = proof λ x → {!!}
+
+
+-- whileLoopPSem' input pre (λ output1 x → proof (λ x₁ → ?)) (λ output₁ x → proof (λ x₁ → ?))))
+-- proof (whileLoopPwP input pre (λ e p1 p11 → {!!}) (λ e2 p2 p22 → {!!}) )
 -- with <-cmp 0 (varn input )
 -- ... | ttt = {!!}