>PhoX> Sort term.
Sort term defined
>PhoX> Cst f : term  term.
f : term  term
>PhoX> Cst zero : term.
zero : term
>PhoX> def Im A y = x (A x  f x = y).
Im = \A,y x:A  f x = y
                                   : (term  prop)  term  prop
>PhoX> def ker x = f x = zero.
ker = \x (f x = zero) : term  prop
>PhoX> def inclus A B = x (A x  B x).
inclus = \A,B x:A  B x
                                    : ('a  prop)  ('a  prop)  prop
>PhoX> Cst plus : term  term  term.
plus : term  term  term
>PhoX> Cst moins : term  term  term.
moins : term  term  term
>PhoX> def Plus A B x = y,z (A y  B z  x = (plus y z)).

Plus = \A,B,x y,z (A y  B z  x = plus y z)
 : (term  prop)  (term  prop)  term  prop
>PhoX> (* On a supposé, implicitement, que les ensembles de termes sont des espaces vectoriels et que f est une application linéaire. Les lemmes ci-dessous expriment les propriétés des espaces vectoriels (resp. des applications linéaires) dont on a besoin dans la preuve faite. Ils pourraient être prouvés sans difficulté à partir des axiomes d'espace vectoriel et de la définition d'une application linéaire. On a préféré ici se concentrer sur l'essentiel et on les admettra donc*)

>PhoX> claim lemme1 x,y (f x = f y  ker (moins y x)).

lemme1 = x,y (f x = f y  ker (moins y x)) : theorem
>PhoX> claim lemme2 x,y,z plus x (plus z (moins y x))=plus y z.

lemme2 = x,y,z plus x (plus z (moins y x)) = plus y z :
theorem
>PhoX> claim lemme3 x,y (ker x  ker y  ker (plus x y)).

lemme3 = x,y (ker x  ker y  ker (plus x y)) :
theorem
>PhoX> claim lemme4 y,a,b (plus a b = y  ker b  f a = f y).

lemme4 = y,a,b (plus a b = y  ker b  f a = f y) :
theorem
>PhoX> claim lemme5 A,B a (A a  Plus A B a).
lemme5 =
                                            A,B a:A  Plus A B a :
                                            theorem
>PhoX> goal A,B ((inclus (Im A) (Im B)) (inclus (Plus A ker) (Plus B ker))).
Here is the goal:
goal 1/1
    A,B (inclus (Im A) (Im B)  inclus (Plus A ker) (Plus B ker))

%PhoX% intro 6.
2 goals created.

goal 2/2
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
    Plus B ker x

%PhoX% elim H0.
1 goal created.

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z (A y  ker z  x = plus y z)
    Plus B ker x

%PhoX% elim H1.
1 goal created.

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H2 := A y  ker z  x = plus y z
    Plus B ker x

%PhoX% lefts H2.
1 goal created.

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Plus B ker x

%PhoX% use Im B (f y).
2 goals created.

goal 2/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
    Plus B ker x

%PhoX% elim G.
1 goal created.

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0  f x0 = f y
    Plus B ker x

%PhoX% intro 2.
1 goal created.

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0  f x0 = f y
    B ?1  ker ?2  x = plus ?1 ?2

%PhoX% instance ?1 x0.
Here are the goals:
goal 3/3
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 2/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0  f x0 = f y
    B x0  ker ?2  x = plus x0 ?2

%PhoX% instance ?2 plus z (moins y x0).
Here are the goals:
goal 3/3
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 2/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0  f x0 = f y
    B x0  ker (plus z (moins y x0))  x = plus x0 (plus z (moins y x0))

%PhoX% left H5.
1 goal created.

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    B x0  ker (plus z (moins y x0))  x = plus x0 (plus z (moins y x0))

%PhoX% intros.
3 goals created.

goal 3/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    x = plus x0 (plus z (moins y x0))

goal 2/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    ker (plus z (moins y x0))

goal 1/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    B x0

%PhoX% axiom H5.
0 goal created.

goal 4/4
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 3/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 2/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    x = plus x0 (plus z (moins y x0))

goal 1/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    ker (plus z (moins y x0))

%PhoX% use ker (moins y x0).
2 goals created.

goal 2/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    ker (moins y x0)

goal 1/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := ker (moins y x0)
    ker (plus z (moins y x0))

%PhoX% elim lemme3.
1 goal created.

goal 1/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := ker (moins y x0)
    ker z  ker (moins y x0)

%PhoX% intro.
2 goals created.

goal 2/6
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := ker (moins y x0)
    ker (moins y x0)

goal 1/6
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := ker (moins y x0)
    ker z

%PhoX% axiom H4.
0 goal created.

goal 5/5
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 4/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 3/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    x = plus x0 (plus z (moins y x0))

goal 2/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    ker (moins y x0)

goal 1/5
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := ker (moins y x0)
    ker (moins y x0)

%PhoX% axiom G0.
0 goal created.

goal 4/4
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 3/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 2/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    x = plus x0 (plus z (moins y x0))

goal 1/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    ker (moins y x0)

%PhoX% elim lemme1.
1 goal created.

goal 1/4
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    f x0 = f y

%PhoX% axiom H6.
0 goal created.

goal 3/3
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 2/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
    x = plus x0 (plus z (moins y x0))

%PhoX% apply -1 x0 -2 y -3 z lemme2.
1 goal created.

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
G := Im B (f y)
H5 := B x0
H6 := f x0 = f y
G0 := plus x0 (plus z (moins y x0)) = plus y z
    x = plus x0 (plus z (moins y x0))

%PhoX% intro.
0 goal created.

goal 2/2
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im B (f y)

%PhoX% elim H.
1 goal created.

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    Im A (f y)

%PhoX% intro.
1 goal created.

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    A ?3  f ?3 = f y

%PhoX% intro.
2 goals created.

goal 2/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    f ?3 = f y

goal 1/3
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    A ?3

%PhoX% axiom H2.
0 goal created.

goal 2/2
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

goal 1/2
H := inclus (Im A) (Im B)
H0 := Plus A ker x
H1 := z0 (A y  ker z0  x = plus y z0)
H3 := x = plus y z
H2 := A y
H4 := ker z
    f y = f y

%PhoX% intro.
0 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := Im A x
    Im B x

%PhoX% left H0.
1 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0  f x0 = x
    Im B x

%PhoX% left H0.
1 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    Im B x

%PhoX% use Plus B ker x0.
2 goals created.

goal 2/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    Plus B ker x0

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
G := Plus B ker x0
    Im B x

%PhoX% left G.
1 goal created.

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H2 := z (B x1  ker z  x0 = plus x1 z)
    Im B x

%PhoX% lefts H2.
1 goal created.

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H2 := B x1  ker z  x0 = plus x1 z
    Im B x

%PhoX% lefts H2.
1 goal created.

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
    Im B x

%PhoX% intro .
1 goal created.

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
    B ?4  f ?4 = x

%PhoX% intro.
2 goals created.

goal 2/3
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
    f ?4 = x

goal 1/3
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
    B ?4

%PhoX% axiom H2.
0 goal created.

goal 2/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    Plus B ker x0

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
    f x1 = x

%PhoX% apply -4 H3 -5 H4 lemme4.
1 goal created.

goal 1/2
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
H3 := x0 = plus x1 z
H2 := B x1
H4 := ker z
G := f x1 = f (plus x1 z)
    f x1 = x

%PhoX% intro.
0 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    Plus B ker x0

%PhoX% elim H.
1 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    Plus A ker x0

%PhoX% elim lemme5.
1 goal created.

goal 1/1
H := inclus (Plus A ker) (Plus B ker)
H0 := A x0
H1 := f x0 = x
    A x0

%PhoX% axiom H0.
0 goal created.

%PhoX% save th.
Building proof ....
Typing proof ....
Verifying proof ....
Saving proof ....
th = A,B (inclus (Im A) (Im B)  inclus (Plus A ker) (Plus B ker))
 : theorem

bye