--- a/whileTestGears.agda	Sat Dec 21 18:28:46 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 19:37:41 2019 +0900
@@ -178,6 +178,7 @@
 loopPwP : {l : Level} {t : Set l} → (env : Envc ) → whileTestStateP s2 env → (exit : (env : Envc ) → whileTestStateP sf env → t) → t
 loopPwP env s exit = whileLoopPwP env s (λ env s → loopPwP env s exit ) exit
 
+
 whileTestPCallwP : (c :  ℕ ) → Set
 whileTestPCallwP c = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → vari env ≡ c )  ) where
     conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
@@ -189,7 +190,9 @@
 
 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
 
-ProofConnect : {l : Level} {t : Set l} → (prev : Envc → Set → Set) → (Envc → Set → (Envc → Set → t)) → (Envc → Set → Set)
+
+
+ProofConnect : {l : Level} {t : Set l} → (pr1 : Envc → Set → Set) → (Envc → Set → (Envc → Set → t)) → (pr2 : Envc → Set → Set)
 ProofConnect prev f env post with f env ({!!}) {!!} 
 ... | tt = {!!}
 
@@ -197,60 +200,9 @@
 Proof2 _ refl = refl 
 
 
-{--
-  Proof1 env s with Proof2 ? ?
-  ... | tt = ?
-のとき agda2 が停まらなくなる
---}
-
+-- Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → ((env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env) → vari env ≡ c10 env
 Proof1 : (env : Envc) → (s : varn env + vari env ≡ c10 env) → loopPwP env s ( λ env s → vari env ≡ c10 env ) 
-Proof1 env s = {!!} -- with Proof2 ? ? <- agda2 don't stop
-  where
-    lemm : whileLoopPwP env s (λ env s → {!!} ) (λ env s → {!!} )
-    lemm = {!!} -- with Proof2 ? ?
+Proof1 env s = {!!} 
 
 Proof : (c :  ℕ ) → whileTestPCallwP c
-Proof zero = whileTestPwP {_} {_} zero ( λ env s → loopPwP env (conv env s) ( λ env s → refl)  )
-  where
-    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-    conv e record { pi1 = refl ; pi2 = refl } = +zero
-Proof (suc c) = whileTestPwP {_} {_} c ( λ env s → loopPwP env (conv env s) ( λ env s → lem ))
-  where
-    lem : whileLoopPwP (record { c10 = suc c ; varn = c ; vari = 0 + 1 }) ({!!})
-      (λ env s → loopPwP env s (λ env₁ s₁ → vari env₁ ≡ suc c)) (λ env s3 → {!!})
-    lem = {!!}
-    conv : (env : Envc ) → (vari env ≡ 0) /\ (varn env ≡ c10 env) → varn env + vari env ≡ c10 env
-    conv e record { pi1 = refl ; pi2 = refl } = +zero
-
-
-{--
--- whileLoopPwP : {l : Level} {t : Set l}   → (env : Envc ) → whileTestStateP s2 env
---     → (next : (env : Envc ) → whileTestStateP s2 env  → t)
---     → (exit : (env : Envc ) → whileTestStateP sf env  → t) → t
-
-next : (whileTestGears.proof5
-     (record { c10 = suc c ; varn = suc c ; vari = 0 })
-     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt)
-     (λ x →
-        Relation.Nullary.Reflects.invert (ofⁿ (λ ())) (≡⇒≡ᵇ 0 (suc c) x))
-     (<⇒≯ (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
-     (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁))
-      (record { pi1 = refl ; pi2 = refl }))
-     (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
-     (λ env₁ s₁ → vari env₁ ≡ suc c)
-     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
-
-exit : (whileTestGears.conv (suc c) (whileTestP (suc c) (λ env₁ → env₁))
-      (record { pi1 = refl ; pi2 = refl }))
-     (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
-     (λ env₁ s₁ → vari env₁ ≡ suc c)
-     (<ᵇ⇒< 0 (suc c) Agda.Builtin.Unit.⊤.tt))
-    (λ env₁ s₁ → loopPwP env₁ s₁ (λ env₂ s₂ → vari env₂ ≡ suc c))
-    (λ env₁ s₁ → vari env₁ ≡ suc c)
-
-    | (<-cmp 0 c
-       | Relation.Nullary.Decidable.Core.map′ (≡ᵇ⇒≡ 0 c) (≡⇒≡ᵇ 0 c)
-         (Data.Bool.Properties.T? (0 ≡ᵇ c))
-       | Data.Bool.Properties.T? (0 <ᵇ c))
-
---}
+Proof c = {!!}

--- a/whileTestPrimProof.agda	Sat Dec 21 18:28:46 2019 +0900
+++ b/whileTestPrimProof.agda	Sat Dec 21 19:37:41 2019 +0900
@@ -71,6 +71,7 @@
 --        (Seq (PComm (λ env → record env {vari = ((vari env) + 1)} ))
 --          $ PComm (λ env → record env {varn = ((varn env) - 1)} ))
 
+
 proof1 : (c10 : ℕ) → HTProof initCond (program c10 ) (termCond {c10})
 proof1 c10 =
       SeqRule {λ e → true} ( PrimRule (init-case {c10} ))
@@ -279,3 +280,10 @@
 PrimSoundness : {bPre : Cond} -> {cm : Comm} -> {bPost : Cond} ->
             HTProof bPre cm bPost -> Satisfies bPre cm bPost
 PrimSoundness {bPre} {cm} {bPost} ht = Soundness ht
+
+
+proofOfProgram : (c10 : ℕ) → (input output : Env )
+  → initCond input ≡ true
+  → (SemComm (program c10) input output)
+  → termCond {c10} output ≡ true
+proofOfProgram c10 input output ic sem  = PrimSoundness (proof1 c10) input output ic sem