--- a/RelOp.agda	Sat Dec 21 19:37:41 2019 +0900
+++ b/RelOp.agda	Sat Dec 21 21:12:07 2019 +0900
@@ -55,7 +55,6 @@
 -- unionInf f = ⋃_{n ∈ ω} f(n)
 unionInf : ∀ {l} -> (ℕ -> Rel S l) -> Rel S l
 unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
-
 -- restPre X R = { (s1,s2) ∈ R | s1 ∈ X }
 restPre : ∀ {l} -> Pred S -> Rel S l -> Rel S l
 restPre X R a b = X a × R a b

--- a/whileTestGears.agda	Sat Dec 21 19:37:41 2019 +0900
+++ b/whileTestGears.agda	Sat Dec 21 21:12:07 2019 +0900
@@ -3,9 +3,11 @@
 open import Function
 open import Data.Nat
 open import Data.Bool hiding ( _≟_ ; _≤?_ ; _≤_ ; _<_)
+open import Data.Product
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
+open import Agda.Builtin.Unit
 
 open import utilities
 open  _/\_
@@ -174,11 +176,13 @@
          c10 env
       ∎
 
+
+-- induction にする
 {-# TERMINATING #-}
 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
 
-
+--  wP を Env のRel にする  Env → Env → Set にしちゃう
 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
@@ -191,10 +195,40 @@
 -- = whileTestPwP (suc c) (λ env s → loopPwP env (conv1 env s) (λ env₁ s₁ → {!!}))
 
 
+data GComm : Set (succ Zero) where
+  Skip  : GComm
+  Abort : GComm
+  PComm : Set → GComm
+  -- Seq   : GComm → GComm → GComm
+  -- If   : whileTestState → GComm → GComm → GComm
+  while : whileTestState → GComm → GComm
 
-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 = {!!}
+gearsSem : {l : Level} {t : Set l} → {c10 : ℕ} → Envc → Envc → (Envc → (Envc → t) → t) → Set
+gearsSem pre post = {!!}
+
+unionInf : ∀ {l} -> (ℕ -> Rel Set l) -> Rel Set l
+unionInf f a b = ∃ (λ (n : ℕ) → f n a b)
+
+comp : ∀ {l} → Rel Set l → Rel Set l → Rel Set (succ Zero Level.⊔ l)
+comp r1 r2 a b = ∃ (λ (a' : Set) → r1 a a' × r2 a' b)
+
+-- repeat : ℕ -> rel set zero -> rel set zero
+-- repeat ℕ.zero r = λ x x₁ → ⊤
+-- repeat (ℕ.suc m) r = comp (repeat m r) r
+
+GSemComm : {l : Level} {t : Set l} → GComm → Rel whileTestState (Zero)
+GSemComm Skip = λ x x₁ → ⊤
+GSemComm Abort = λ x x₁ → ⊥
+GSemComm (PComm x) = λ x₁ x₂ → x
+-- GSemComm (Seq con con₁ con₃) = λ x₁ x₂ → {!!}
+-- GSemComm (If x con con₁) = {!!}
+GSemComm (while x con) = λ x₁ x₂ → unionInf {Zero} (λ (n : ℕ) →  {!!}) {!!} {!!}
+
+ProofConnect : {l : Level} {t : Set l}
+  → (pr1 : Envc → Set → Set)
+  → (Envc → Set → (Envc → Set → t))
+  → (Envc → Set → Set)
+ProofConnect prev f env post =  {!!} -- with f env ({!!}) {!!} 
 
 Proof2 : (env : Envc) → (vari env ≡ c10 env) → vari env ≡ c10 env
 Proof2 _ refl = refl