--- a/ModelChecking.agda	Mon May 16 10:48:49 2022 +0900
+++ b/ModelChecking.agda	Mon May 16 17:55:19 2022 +0900
@@ -210,11 +210,47 @@
 new-data : {n : Level} {t : Set n} → ( c : Context ) → (ℕ → Data ) → ( Context → ℕ → t ) → t
 new-data  c x next  = alloc-data c $ λ c1 n → insertTree (Context.memory c1) n (x n) ( λ bt → next record c1 { memory = bt } n )
 
+init-AtomicNat0 :  {n : Level} {t : Set n} → Context  → ( Context →  ℕ → t ) → t
+init-AtomicNat0 c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 ptr where
+    a : ℕ → AtomicNat
+    a ptr = record { ptr = ptr ; value = 0 }
+
+init-Phil-0 : (ps : List Context) → (left right : AtomicNat ) → List Context
+init-Phil-0 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
+    p : ℕ → Phil
+    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
+    c1 :  List Context → Context
+    c1 [] =  init-context
+    c1 (c2 ∷ ct) =  c2
+
 init-AtomicNat1 :  {n : Level} {t : Set n} → Context  → ( Context →  AtomicNat → t ) → t
 init-AtomicNat1 c1  next = new-data c1  ( λ ptr → D_AtomicNat (a ptr) ) $ λ c2 ptr → next c2 (a ptr) where
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
+init-Phil-1 : (ps : List Context) → (left right : AtomicNat ) → List Context
+init-Phil-1 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
+    p : ℕ → Phil
+    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
+    c1 :  List Context → Context
+    c1 [] =  init-context
+    c1 (c2 ∷ ct) =  c2
+
+test-j0 : {n : Level} {t : Set n} → Context → (Context → AtomicNat → t) → t
+test-j0 c next = init-AtomicNat1 c next
+
+test-j2 : AtomicNat  
+test-j2 = test-j0 init-context (λ c f → f )
+
+test-i1 : Context → Context 
+test-i1 c = init-AtomicNat1 c $ λ c f → c
+
+test-i0 : Context
+test-i0 = test-i1 init-context
+
+test-i2 : Context
+test-i2 = test-i1 test-i0
+
 test20 : bt (Data)
 test20 = init-AtomicNat1 init-context $  λ c1 left → alloc-data c1
  $ λ c n → Context.memory c
@@ -241,14 +277,6 @@
     a : ℕ → AtomicNat
     a ptr = record { ptr = ptr ; value = 0 }
 
-init-Phil-1 : (ps : List Context) → (left right : AtomicNat ) → List Context
-init-Phil-1 ps left right = new-data (c1 ps) ( λ ptr → D_Phil (p ptr) )  $ λ c ptr → record c { c_Phil-API = record { next = C_thinking ; impl = p ptr }} ∷ ps where
-    p : ℕ → Phil
-    p ptr = record  init-Phil { ptr = ptr ; left = left ; right = right }  
-    c1 :  List Context → Context
-    c1 [] =  init-context
-    c1 (c2 ∷ ct) =  c2
-
 test-newdata : bt Data
 test-newdata = new-data  init-context ( λ ptr → D_AtomicNat (a ptr) ) $ λ c n → Context.memory c where
     a : ℕ → AtomicNat