--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/example2.agda	Thu Aug 13 18:44:09 2020 +0900
@@ -0,0 +1,72 @@
+module example2 where
+open import Data.List hiding (all ; and ; or )
+open import Data.Maybe 
+open import Data.Bool hiding ( not )
+
+data Const : Set where
+      anakin : Const
+      luke : Const
+      leia : Const
+
+data Var : Set where
+      X : Var
+      Y : Var
+      Z : Var
+
+data Func : Set where
+      f : Func
+
+data Pred : Set where
+      father : Pred
+      brother : Pred
+
+open import Logic Const Func Var Pred 
+
+_⇒_ : Statement → Statement → Statement 
+x ⇒ y = ( ¬ x ) \/ y
+
+ex1 : Statement
+ex1 = All X => All Y => (( Exist Z => ( ( predx father ( var X , var Z ) /\  predx father (var Y , var Z ) ))) ⇒ predx brother ( var X , var Y) )
+
+subst-expr :  Expr  → Var → Expr → Expr 
+subst-expr  (var X) X v = v
+subst-expr  (var Y) Y v = v
+subst-expr  (var Z) Z v = v
+subst-expr  (func f₁ e) xv v = func f₁ ( subst-expr e xv v ) 
+subst-expr  (e , e1) xv v = ( subst-expr e xv v ) , ( subst-expr e1 xv v )
+subst-expr  x _ v = x
+
+amap : (px :  Pred ) → Bool 
+amap px = false
+pmap : (px :  Pred ) → Expr → Bool 
+pmap father ( const leia , const anakin ) = true
+pmap father ( const luke , const anakin ) = true
+pmap brother ( const leia , const luke) = true
+pmap px _ = false
+
+-- we only try simple constant, it may contains arbitrary complex functional value
+all0   :  List Expr
+all0 =  const anakin ∷ const luke ∷ const leia ∷ []
+
+test003 : Bool 
+test003 = M amap pmap all0 subst-expr (
+     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+
+--
+-- Valid Proposition true on any interpretation
+--
+pmap1 : (px :  Pred ) → Expr → Bool 
+pmap1 father ( const leia , const anakin ) = true
+pmap1 father ( const luke , const anakin ) = true
+pmap1 brother ( const leia , const luke) = false
+pmap1 px _ = false
+
+test006 : Bool 
+test006 = M amap pmap1 all0 subst-expr (
+     ( ex1 /\ ( predx father ( const leia , const anakin ) /\ predx father ( const luke , const anakin ) )) ⇒ predx brother ( const leia , const luke) )
+
+test004 : Bool 
+test004 = M amap pmap all0 subst-expr ( ex1  )
+
+test005 : Bool 
+test005 = M amap pmap all0 subst-expr (   All X => All Y => ( predx father ( var X , const anakin ) /\  predx father (var Y , const anakin ) ))