Commit 69b4bd15 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Dershowitz examples

parent e798bd91
A : Type.
e : A.
def slash : A -> A -> A.
def backslash : A -> A -> A.
def dot : A -> A -> A.
[x] backslash x x --> e.
[x] slash x x --> e.
[x] dot e x --> x.
[x] dot x e --> x.
[x] backslash e x --> x.
[x] slash x e --> x.
[x,y] dot x (backslash x y) --> y.
[x,y] dot (slash y x) x --> y.
[x,y] backslash x (dot x y) --> y.
[x,y] backslash (dot y x) x --> y.
[x,y] slash x (backslash y x) --> y.
[x,y] backslash (slash x y) x --> y.
fun : Type.
plus : fun -> fun -> fun.
mult : fun -> fun -> fun.
minus : fun -> fun -> fun.
id : fun.
0 : fun.
1 : fun.
opp : fun -> fun.
div : fun -> fun -> fun.
ln : fun -> fun.
power : fun -> fun -> fun.
def D : fun -> fun.
[] D id --> 1.
[] D 0 --> 0.
[] D 1 --> 1.
[x,y] D (plus x y) --> plus (D x) (D y).
[x,y] D (mult x y) --> plus (mult y (D x)) (mult x (D y)).
[x,y] D (minus x y) --> minus (D x) (D y).
[x] D (opp x) --> opp (D x).
[x,y] D (div x y) --> minus (div (D x) y) (mult x (div (D y) (mult y y))).
[x] D (ln x) --> div (D x) x.
[x,y] D (power x y) --> plus (mult y (mult (power x (minus y 1)) (D x))) (mult (power x y) (mult (ln x) (D y))).
Group : Type.
1 : Group.
def dot : Group -> Group -> Group.
def inv : Group -> Group.
[x] dot 1 x --> x.
[x] dot x 1 --> x.
[x] dot (inv x) x --> 1.
[x] dot x (inv x) --> 1.
[] inv 1 --> 1.
[x] inv (inv x) --> 1.
[x,y] dot (inv x) (dot x y) --> y.
[x,y] dot x (dot (inv x) y) --> y.
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> g (f x).
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> g (f x).
[x] g (g x) --> f x.
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (f x) --> f (g (f x)).
A : Type.
def f : A -> A.
def g : A -> A.
[x] f (g x) --> g (g (f x)).
[x] f (g x) --> g (g (g x)).
Dutch : Type.
def w : Dutch -> Dutch.
def r : Dutch -> Dutch.
def b : Dutch -> Dutch.
[x] w (r x) --> r (w x).
[x] b (r x) --> r (b x).
[x] b (w x) --> w (b x).
fun : Type.
plus : fun -> fun -> fun.
mult : fun -> fun -> fun.
minus : fun -> fun -> fun.
id : fun.
0 : fun.
1 : fun.
def D : fun -> fun.
[] D id --> 1.
[] D 0 --> 0.
[] D 1 --> 1.
[x,y] D (plus x y) --> plus (D x) (D y).
[x,y] D (mult x y) --> plus (mult y (D x)) (mult x (D y)).
[x,y] D (minus x y) --> minus (D x) (D y).
A : Type.
def dot : A -> A -> A.
[x,y,z] dot (dot x y) z --> dot x (dot y z).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment