--- 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