# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597458498 -32400
# Node ID b8b3eaf0dd61c14e7d0d460dd1fccd0f246429f9
# Parent  4b131e351170ed7abc41321d088a968f005f3b20
...

diff -r 4b131e351170 -r b8b3eaf0dd61 clausal.agda
--- a/clausal.agda	Sat Aug 15 11:03:32 2020 +0900
+++ b/clausal.agda	Sat Aug 15 11:28:18 2020 +0900
@@ -47,8 +47,10 @@
 {-# TERMINATING #-} 
 skolem  : List Const → List Func → (sbst : Expr  → Var →  Expr  → Expr  ) → Statement → Statement
 skolem cl fl sbst s = skolemv1 ( λ s cl fl vr → s ) s cl fl []  where
-   skolemv1 : (Statement → List Const → List Func → List Var → Statement ) → Statement → List Const → List Func → List Var → Statement
+   skolemv1 : (Statement → List Const → List Func → List Var → Statement )
+             → Statement → List Const → List Func → List Var → Statement
    skolemv1 next (All x => s )   cl fl vl              = skolemv1 next s cl fl ( x ∷ vl) 
+   -- all existentical quantifiers are replaced by constants or funcions
    skolemv1 next (Exist x => s ) [] fl []              = skolemv1 next s [] fl [] 
    skolemv1 next (Exist x => s ) (sk ∷ cl ) fl []      = skolemv1 next (subst-prop s sbst x (Expr.const sk)) cl fl [] 
    skolemv1 next (Exist x => s ) cl [] (v ∷ t)         = skolemv1 next s cl [] (v ∷ t)
@@ -58,12 +60,13 @@
       mkarg v (v1 ∷ t )  = var v , mkarg v1 t
    skolemv1 next (s /\ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s /\ s₁) ) s₁ ) s 
    skolemv1 next (s \/ s₁)                             = skolemv1 ( λ s → skolemv1 (λ s₁ → next (s \/ s₁) ) s₁ ) s 
-   skolemv1 next s cl fl vl                            = next s cl fl vl 
+   skolemv1 next                                       = next 
 
 -- remove universal quantifiers
 univout  : Statement → Statement
 univout (s /\ s₁) = univout s /\ univout s₁
 univout (s \/ s₁) = univout s \/ univout s₁
+univout (All x => s ) = s
 univout x = x
 
 -- move disjunctions inside