--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda/logic.agda.replaced	Fri Nov 05 15:19:08 2021 +0900
@@ -0,0 +1,152 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary hiding(_⇔_)
+open import Data.Empty
+
+
+data Bool : Set where
+    true : Bool
+    false : Bool
+
+record  _@$\wedge$@_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n @$\sqcup$@ m) where
+   case1 : A @$\rightarrow$@ A ∨ B
+   case2 : B @$\rightarrow$@ A ∨ B
+
+_⇔_ : {n m : Level } @$\rightarrow$@ ( A : Set n ) ( B : Set m )  @$\rightarrow$@ Set (n @$\sqcup$@ m)
+_⇔_ A B =  ( A @$\rightarrow$@ B ) @$\wedge$@ ( B @$\rightarrow$@ A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} @$\rightarrow$@ (A @$\rightarrow$@ B) @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ @$\neg$@ A
+contra-position {n} {m} {A} {B}  f @$\neg$@b a = @$\neg$@b ( f a )
+
+double-neg : {n  : Level } {A : Set n} @$\rightarrow$@ A @$\rightarrow$@ @$\neg$@ @$\neg$@ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} @$\rightarrow$@ @$\neg$@ @$\neg$@ @$\neg$@ A @$\rightarrow$@ @$\neg$@ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} @$\rightarrow$@  A @$\wedge$@ B  @$\rightarrow$@ @$\neg$@ ( (@$\neg$@ A ) ∨ (@$\neg$@ B ) )
+de-morgan {n} {A} {B} and (case1 @$\neg$@A) = @$\bot$@-elim ( @$\neg$@A ( _@$\wedge$@_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 @$\neg$@B) = @$\bot$@-elim ( @$\neg$@B ( _@$\wedge$@_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } @$\rightarrow$@  A ∨ B @$\rightarrow$@ @$\neg$@ A @$\rightarrow$@ B
+dont-or {A} {B} (case1 a) @$\neg$@A = @$\bot$@-elim ( @$\neg$@A a )
+dont-or {A} {B} (case2 b) @$\neg$@A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } @$\rightarrow$@  A ∨ B @$\rightarrow$@ @$\neg$@ B @$\rightarrow$@ A
+dont-orb {A} {B} (case2 b) @$\neg$@B = @$\bot$@-elim ( @$\neg$@B b )
+dont-orb {A} {B} (case1 a) @$\neg$@B = a
+
+
+
+infixr  130 _@$\wedge$@_
+infixr  140 _∨_
+infixr  150 _⇔_
+
+_@$\wedge$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool 
+true @$\wedge$@ true = true
+_ @$\wedge$@ _ = false
+
+_\/_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool 
+false \/ false = false
+_ \/ _ = true
+
+not_ : Bool @$\rightarrow$@ Bool 
+not true = false
+not false = true 
+
+_<=>_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool  
+true <=> true = true
+false <=> false = true
+_ <=> _ = false
+
+infixr  130 _\/_
+infixr  140 _@$\wedge$@_
+
+open import Relation.Binary.PropositionalEquality
+
+
+@$\equiv$@-Bool-func : {A B : Bool } @$\rightarrow$@ ( A @$\equiv$@ true @$\rightarrow$@ B @$\equiv$@ true ) @$\rightarrow$@ ( B @$\equiv$@ true @$\rightarrow$@ A @$\equiv$@ true ) @$\rightarrow$@ A @$\equiv$@ B
+@$\equiv$@-Bool-func {true} {true} a@$\rightarrow$@b b@$\rightarrow$@a = refl
+@$\equiv$@-Bool-func {false} {true} a@$\rightarrow$@b b@$\rightarrow$@a with b@$\rightarrow$@a refl
+... | ()
+@$\equiv$@-Bool-func {true} {false} a@$\rightarrow$@b b@$\rightarrow$@a with a@$\rightarrow$@b refl
+... | ()
+@$\equiv$@-Bool-func {false} {false} a@$\rightarrow$@b b@$\rightarrow$@a = refl
+
+bool-@$\equiv$@-? : (a b : Bool) @$\rightarrow$@ Dec ( a @$\equiv$@ b )
+bool-@$\equiv$@-? true true = yes refl
+bool-@$\equiv$@-? true false = no (@$\lambda$@ ())
+bool-@$\equiv$@-? false true = no (@$\lambda$@ ())
+bool-@$\equiv$@-? false false = yes refl
+
+@$\neg$@-bool-t : {a : Bool} @$\rightarrow$@  @$\neg$@ ( a @$\equiv$@ true ) @$\rightarrow$@ a @$\equiv$@ false
+@$\neg$@-bool-t {true} ne = @$\bot$@-elim ( ne refl )
+@$\neg$@-bool-t {false} ne = refl
+
+@$\neg$@-bool-f : {a : Bool} @$\rightarrow$@  @$\neg$@ ( a @$\equiv$@ false ) @$\rightarrow$@ a @$\equiv$@ true
+@$\neg$@-bool-f {true} ne = refl
+@$\neg$@-bool-f {false} ne = @$\bot$@-elim ( ne refl )
+
+@$\neg$@-bool : {a : Bool} @$\rightarrow$@  a @$\equiv$@ false  @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ @$\bot$@
+@$\neg$@-bool refl ()
+
+lemma-@$\wedge$@-0 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ @$\bot$@
+lemma-@$\wedge$@-0 {true} {true} refl ()
+lemma-@$\wedge$@-0 {true} {false} ()
+lemma-@$\wedge$@-0 {false} {true} ()
+lemma-@$\wedge$@-0 {false} {false} ()
+
+lemma-@$\wedge$@-1 : {a b : Bool} @$\rightarrow$@ a @$\wedge$@ b @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ @$\bot$@
+lemma-@$\wedge$@-1 {true} {true} refl ()
+lemma-@$\wedge$@-1 {true} {false} ()
+lemma-@$\wedge$@-1 {false} {true} ()
+lemma-@$\wedge$@-1 {false} {false} ()
+
+bool-and-tt : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true
+bool-and-tt refl refl = refl
+
+bool-@$\wedge$@@$\rightarrow$@tt-0 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ a @$\equiv$@ true 
+bool-@$\wedge$@@$\rightarrow$@tt-0 {true} {true} refl = refl
+bool-@$\wedge$@@$\rightarrow$@tt-0 {false} {_} ()
+
+bool-@$\wedge$@@$\rightarrow$@tt-1 : {a b : Bool} @$\rightarrow$@ ( a @$\wedge$@ b ) @$\equiv$@ true @$\rightarrow$@ b @$\equiv$@ true 
+bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {true} refl = refl
+bool-@$\wedge$@@$\rightarrow$@tt-1 {true} {false} ()
+bool-@$\wedge$@@$\rightarrow$@tt-1 {false} {false} ()
+
+bool-or-1 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ false @$\rightarrow$@ ( a \/ b ) @$\equiv$@ b 
+bool-or-1 {false} {true} refl = refl
+bool-or-1 {false} {false} refl = refl
+bool-or-2 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ false @$\rightarrow$@ (a \/ b ) @$\equiv$@ a 
+bool-or-2 {true} {false} refl = refl
+bool-or-2 {false} {false} refl = refl
+
+bool-or-3 : {a : Bool} @$\rightarrow$@ ( a \/ true ) @$\equiv$@ true 
+bool-or-3 {true} = refl
+bool-or-3 {false} = refl
+
+bool-or-31 : {a b : Bool} @$\rightarrow$@ b @$\equiv$@ true  @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true 
+bool-or-31 {true} {true} refl = refl
+bool-or-31 {false} {true} refl = refl
+
+bool-or-4 : {a : Bool} @$\rightarrow$@ ( true \/ a ) @$\equiv$@ true 
+bool-or-4 {true} = refl
+bool-or-4 {false} = refl
+
+bool-or-41 : {a b : Bool} @$\rightarrow$@ a @$\equiv$@ true  @$\rightarrow$@ ( a \/ b ) @$\equiv$@ true 
+bool-or-41 {true} {b} refl = refl
+
+bool-and-1 : {a b : Bool} @$\rightarrow$@  a @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
+bool-and-1 {false} {b} refl = refl
+bool-and-2 : {a b : Bool} @$\rightarrow$@  b @$\equiv$@ false @$\rightarrow$@ (a @$\wedge$@ b ) @$\equiv$@ false
+bool-and-2 {true} {false} refl = refl
+bool-and-2 {false} {false} refl = refl
+
+