--- a/automaton-in-agda/src/induction-ex.agda	Fri Jan 21 12:31:34 2022 +0900
+++ b/automaton-in-agda/src/induction-ex.agda	Sun Jan 23 11:15:01 2022 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --guardedness #-}
+{-# OPTIONS --guardedness --sized-types #-}
 module induction-ex where
 
 open import Relation.Binary.PropositionalEquality
@@ -80,10 +80,11 @@
 ν ∅   = false
 δ ∅ _ = ∅
 
-∅' :  {i : Size } { A : Set }  → Lang i A
-∅' {i} {A}  = record { ν = false ; δ = lemma3 } where
-    lemma3 : {j : Size< i} → A → Lang j A
-    lemma3 {j} _ = {!!}
+-- record syntax does not recognize sized data
+-- ∅' :  {i : Size } { A : Set }  → Lang i A
+-- ∅' {i} {A}  = record { ν = false ; δ = lemma3 } where
+--     lemma3 : {j : Size< i} → A → Lang j A
+--     lemma3 {j} _ = ∅'
 
 ∅l : {A : Set } → language {A}
 ∅l _ = false

--- a/automaton-in-agda/src/libbijection.agda	Fri Jan 21 12:31:34 2022 +0900
+++ b/automaton-in-agda/src/libbijection.agda	Sun Jan 23 11:15:01 2022 +0900
@@ -58,6 +58,15 @@
   }
 
 
+open import bijection 
+bij-Setoid :  {n : Level} → Setoid (Level.suc n) n
+bij-Setoid {n}  = record {
+      Carrier = Set n
+    ; _≈_ = Bijection
+    ; isEquivalence = bijIsEquivalence  -- record { sym = bi-sym _ _ ; refl = bid _ ; trans = bi-trans _ _ _ }
+  }
+
+
 libBijection :  {n m : Level} (R : Set n) (S : Set m) → Bijection R S  → Bijection1 (≡-Setoid R) (≡-Setoid S)
 libBijection R S b = record {
      to = record { _⟨$⟩_   = λ x → fun→ b x ; cong = λ i=j → cong (fun→ b) i=j }

--- a/automaton-in-agda/src/temporal-logic.agda	Fri Jan 21 12:31:34 2022 +0900
+++ b/automaton-in-agda/src/temporal-logic.agda	Sun Jan 23 11:15:01 2022 +0900
@@ -33,7 +33,7 @@
 M1 σ i (s x) = σ i x ≡ true
 M1 σ i (○ x) = M1 σ (suc i) x  
 M1 σ i (□ p) = (j : ℕ) → i ≤ j → M1  σ j p
-M1 σ i (⋄ p) = ¬ ( M1 σ i (t-not p) )
+M1 σ i (⋄ p) = ¬ ( M1 σ i (□ (t-not p) ))
 M1 σ i (p U q) = ¬ ( ( j : ℕ) → i ≤ j → ¬ (M1 σ j q ∧ (( k : ℕ) → i ≤ k → k < j → M1 σ j p )) )
 M1 σ i (t-not p) = ¬ ( M1 σ i p )
 M1 σ i (p t\/ p₁) = M1 σ i p ∧ M1 σ i p₁ 
@@ -54,7 +54,7 @@
 MI : { V : Set } → (ℕ → V → Bool) → (i j : ℕ) → i ≤ j  →  LITL V  → Set
 MI σ i j lt (iv x) = σ i x ≡ true
 MI σ i j lt (i○ x) with <-cmp i j
-... | tri< a ¬b ¬c = MI σ (suc i) j {!!} x
+... | tri< a ¬b ¬c = MI σ (suc i) j a x
 ... | tri≈ ¬a b ¬c = ⊤
 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> lt c)
 MI σ i j lt (p & q) = ¬ ( ( k : ℕ) → (i<k : i ≤ k) → (k<j : k ≤ j) → ¬ ( MI σ i k i<k p ∧ MI σ k j k<j p))
@@ -91,6 +91,7 @@
 MQ {V} val dec (p b/\ p₁) = MQ val dec p /\ MQ val dec p₁ 
 
 data QPTL ( V : Set )  : Set where
+    qt :  Bool → QPTL V
     qs :  V → QPTL V
     q○ :  QPTL V → QPTL V
     q□ :  QPTL V → QPTL V
@@ -100,3 +101,29 @@
     _q\/_ :  QPTL V → QPTL  V → QPTL  V
     _q/\_ :  QPTL V → QPTL  V → QPTL  V
 
+{-# TERMINATING #-}
+SQP1 : { V : Set } → ((x y : V) → Dec ( x ≡ y))   → QPTL V → V  → Bool → QPTL V
+SQP1 {V} dec (qt x) v t = qt x
+SQP1 {V} dec (qs x) v t with dec x v
+... | yes _  = qt t
+... | no  _  = qs x
+SQP1 {V} dec (q-exists x p) v t = SQP1 dec (SQP1 dec p x true) v t q\/  SQP1 dec (SQP1 dec p x false) v t
+SQP1 {V} dec (q○ p) v t = q○ p
+SQP1 {V} dec (q□ p) v t = SQP1 {V} dec p v t q/\ q□ p
+SQP1 {V} dec (q⋄ p) v t = q-not ( SQP1 dec (q□ (q-not p)) v t)
+SQP1 {V} dec (q-not p) v t = q-not ( SQP1 dec p v t )
+SQP1 {V} dec (p q\/ p₁) v t = SQP1 {V} dec  p v t q\/ SQP1 {V} dec  p₁ v t 
+SQP1 {V} dec (p q/\ p₁) v t = SQP1 {V} dec  p v t q/\ SQP1 {V} dec  p₁ v t 
+
+{-# TERMINATING #-}
+MQPTL : { V : Set } → (ℕ → V → Bool) → ℕ → ((x y : V) → Dec ( x ≡ y))     →  QPTL V  → Set
+MQPTL σ i dec (qt x) = x ≡ true
+MQPTL σ i dec (qs x) = σ i x ≡ true
+MQPTL σ i dec (q○ x) = MQPTL σ (suc i) dec x  
+MQPTL σ i dec (q□ p) = (j : ℕ) → i ≤ j → MQPTL  σ j dec p
+MQPTL σ i dec (q⋄ p) = ¬ ( MQPTL σ i dec (q□ (q-not p) ))
+MQPTL σ i dec (q-not p) = ¬ ( MQPTL σ i dec p )
+MQPTL σ i dec (q-exists x p) = MQPTL σ i dec ( SQP1 dec p x true q\/  (SQP1 dec p x false)) 
+MQPTL σ i dec (p q\/ p₁) = MQPTL σ i dec p ∧ MQPTL σ i dec p₁ 
+MQPTL σ i dec (p q/\ p₁) = MQPTL σ i dec p ∨ MQPTL σ i dec p₁ 
+