# HG changeset patch
# User ryokka
# Date 1576667338 -32400
# Node ID 2edb44c5bf52722906a8fa9756516d735bb5c77a
# Parent  91d6d8097a39a8bdf2b5dac7838695392782c8a2
add s1~3, proofs

diff -r 91d6d8097a39 -r 2edb44c5bf52 whileTestGears.agda
--- a/whileTestGears.agda	Wed Dec 18 19:26:24 2019 +0900
+++ b/whileTestGears.agda	Wed Dec 18 20:08:58 2019 +0900
@@ -133,6 +133,21 @@
 
 open EnvP
 
+s1 : (c10 : ℕ) → EnvP
+s1 c10 = record {env = record {vari = 0 ; varn = c10} ; c10 = c10 ; cx = pstate1 (record {pi1 = refl ; pi2 = refl})}
+
+s2 : (e : EnvP) → varn (env e) > 0 → varn (env e) < c10 e → EnvP
+s2 e n>0 n<c10 with <-cmp 0 (varn (env e))
+s2 e n>0 n<c10 | tri< a ¬b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pstate2 {!!} {!!} {!!} }
+s2 e n>0 n<c10 | tri≈ ¬a b ¬c = record { env = record { varn = varn (env e) - 1 ; vari = vari (env e) + 1 } ; c10 = c10 e ; cx = pfinstate {!!} {!!} }
+
+s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e
+s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!}
+
+proofs : (c : ℕ) (e : EnvP) → vari (env e) ≡ c10 e
+proofs c e = s3 (s2 (s1 {!!}) {!!} {!!}) {!!}
+
+
 whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t
 whileTestPwithProof {l} {t} c10 next = next record { env = env1 ; c10 = c10 ; cx = cx1 } where
     env1 : Env