:: by Grzegorz Bancerek

::

:: Received April 21, 2008

:: Copyright (c) 2008-2012 Association of Mizar Users

begin

theorem :: ABCMIZ_1:2

theorem Th5: :: ABCMIZ_1:5

for S being non void Signature

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds not t is pair

for X being V8() ManySortedSet of the carrier of S

for t being Term of S,X holds not t is pair

proof end;

registration

let S be non void Signature;

let X be V9() ManySortedSet of the carrier of S;

coherence

for b_{1} being Element of (Free (S,X)) holds not b_{1} is pair

end;
let X be V9() ManySortedSet of the carrier of S;

coherence

for b

proof end;

definition

let S be non void Signature;

let A be MSAlgebra over S;

mode Subset of A is Subset of (Union the Sorts of A);

mode FinSequence of A is FinSequence of Union the Sorts of A;

end;
let A be MSAlgebra over S;

mode Subset of A is Subset of (Union the Sorts of A);

mode FinSequence of A is FinSequence of Union the Sorts of A;

registration

let S be non void Signature;

let X be V9() ManySortedSet of S;

coherence

for b_{1} being FinSequence of (Free (S,X)) holds b_{1} is DTree-yielding

end;
let X be V9() ManySortedSet of S;

coherence

for b

proof end;

theorem Th7: :: ABCMIZ_1:7

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( ex s being SortSymbol of S ex v being set st

( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st

( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) ) )

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( ex s being SortSymbol of S ex v being set st

( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st

( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X \/ ( the carrier of S --> {0}))) ) )

proof end;

definition

let A be set ;

for b_{1}, b_{2} being set st A c= b_{1} & ( for x, y being set st [x,y] in b_{1} holds

x c= b_{1} ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{1} c= B ) & A c= b_{2} & ( for x, y being set st [x,y] in b_{2} holds

x c= b_{2} ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{2} c= B ) holds

b_{1} = b_{2}

ex b_{1} being set st

( A c= b_{1} & ( for x, y being set st [x,y] in b_{1} holds

x c= b_{1} ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{1} c= B ) )

for b_{1} being set

for b_{2} being set st b_{2} c= b_{1} & ( for x, y being set st [x,y] in b_{1} holds

x c= b_{1} ) & ( for B being set st b_{2} c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{1} c= B ) holds

( b_{1} c= b_{1} & ( for x, y being set st [x,y] in b_{1} holds

x c= b_{1} ) & ( for B being set st b_{1} c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{1} c= B ) )
;

end;
func varcl A -> set means :Def1: :: ABCMIZ_1:def 1

( A c= it & ( for x, y being set st [x,y] in it holds

x c= it ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

it c= B ) );

uniqueness ( A c= it & ( for x, y being set st [x,y] in it holds

x c= it ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

it c= B ) );

for b

x c= b

x c= B ) holds

b

x c= b

x c= B ) holds

b

b

proof end;

existence ex b

( A c= b

x c= b

x c= B ) holds

b

proof end;

projectivity for b

for b

x c= b

x c= B ) holds

b

( b

x c= b

x c= B ) holds

b

:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :

for A being set

for b_{2} being set holds

( b_{2} = varcl A iff ( A c= b_{2} & ( for x, y being set st [x,y] in b_{2} holds

x c= b_{2} ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds

x c= B ) holds

b_{2} c= B ) ) );

for A being set

for b

( b

x c= b

x c= B ) holds

b

theorem Th12: :: ABCMIZ_1:12

for A being non empty set st ( for a being Element of A holds varcl a = a ) holds

varcl (meet A) = meet A

varcl (meet A) = meet A

proof end;

registration
end;

deffunc H

definition

ex b_{1} being set ex V being ManySortedSet of NAT st

( b_{1} = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )

for b_{1}, b_{2} being set st ex V being ManySortedSet of NAT st

( b_{1} = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st

( b_{2} = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds

b_{1} = b_{2}
end;

func Vars -> set means :Def2: :: ABCMIZ_1:def 2

ex V being ManySortedSet of NAT st

( it = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) );

existence ex V being ManySortedSet of NAT st

( it = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :

for b_{1} being set holds

( b_{1} = Vars iff ex V being ManySortedSet of NAT st

( b_{1} = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) );

for b

( b

( b

theorem Th14: :: ABCMIZ_1:14

for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds

for i, j being Element of NAT st i <= j holds

V . i c= V . j

for i, j being Element of NAT st i <= j holds

V . i c= V . j

proof end;

theorem Th15: :: ABCMIZ_1:15

for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds

for A being finite Subset of Vars ex i being Element of NAT st A c= V . i

for A being finite Subset of Vars ex i being Element of NAT st A c= V . i

proof end;

definition

let x be variable;

:: original: vars

redefine func vars x -> Subset of Vars;

coherence

vars x is Subset of Vars

end;
:: original: vars

redefine func vars x -> Subset of Vars;

coherence

vars x is Subset of Vars

proof end;

theorem Th26: :: ABCMIZ_1:26

for j being Element of NAT

for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}

for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}

proof end;

begin

definition

ex b_{1} being FinSequenceSet of Vars st

for p being FinSequence of Vars holds

( p in b_{1} iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) )

uniqueness

for b_{1}, b_{2} being FinSequenceSet of Vars st ( for p being FinSequence of Vars holds

( p in b_{1} iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) ) ) & ( for p being FinSequence of Vars holds

( p in b_{2} iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) ) ) holds

b_{1} = b_{2};

end;

func QuasiLoci -> FinSequenceSet of Vars means :Def3: :: ABCMIZ_1:def 3

for p being FinSequence of Vars holds

( p in it iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) );

existence for p being FinSequence of Vars holds

( p in it iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) );

ex b

for p being FinSequence of Vars holds

( p in b

(p . i) `1 c= rng (p dom i) ) ) )

proof end;

correctness uniqueness

for b

( p in b

(p . i) `1 c= rng (p dom i) ) ) ) ) & ( for p being FinSequence of Vars holds

( p in b

(p . i) `1 c= rng (p dom i) ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :

for b_{1} being FinSequenceSet of Vars holds

( b_{1} = QuasiLoci iff for p being FinSequence of Vars holds

( p in b_{1} iff ( p is one-to-one & ( for i being Nat st i in dom p holds

(p . i) `1 c= rng (p dom i) ) ) ) );

for b

( b

( p in b

(p . i) `1 c= rng (p dom i) ) ) ) );

registration
end;

theorem Th30: :: ABCMIZ_1:30

for l being one-to-one FinSequence of Vars holds

( l is quasi-loci iff for i being Nat

for x being variable st i in dom l & x = l . i holds

for y being variable st y in vars x holds

ex j being Nat st

( j in dom l & j < i & y = l . j ) )

( l is quasi-loci iff for i being Nat

for x being variable st i in dom l & x = l . i holds

for y being variable st y in vars x holds

ex j being Nat st

( j in dom l & j < i & y = l . j ) )

proof end;

theorem Th31: :: ABCMIZ_1:31

for l being quasi-loci

for x being variable holds

( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )

for x being variable holds

( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )

proof end;

theorem Th32: :: ABCMIZ_1:32

for p, q being FinSequence st p ^ q is quasi-loci holds

( p is quasi-loci & q is FinSequence of Vars )

( p is quasi-loci & q is FinSequence of Vars )

proof end;

theorem Th35: :: ABCMIZ_1:35

for x, y being variable holds

( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) )

( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) )

proof end;

theorem :: ABCMIZ_1:36

for x, y, z being variable holds

( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) )

( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) )

proof end;

definition

let l be quasi-loci;

:: original: "

redefine func l " -> PartFunc of Vars,NAT;

coherence

l " is PartFunc of Vars,NAT

end;
:: original: "

redefine func l " -> PartFunc of Vars,NAT;

coherence

l " is PartFunc of Vars,NAT

proof end;

begin

definition

coherence

0 is set ;

coherence

1 is set ;

coherence

2 is set ;

coherence

0 is set ;

coherence

1 is set ;

end;
0 is set ;

coherence

1 is set ;

coherence

2 is set ;

coherence

0 is set ;

coherence

1 is set ;

definition

let C be Signature;

end;
attr C is constructor means :Def9: :: ABCMIZ_1:def 9

( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds

the Arity of C . o in {a_Term} * ) );

( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds

the Arity of C . o in {a_Term} * ) );

:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :

for C being Signature holds

( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds

the Arity of C . o in {a_Term} * ) ) );

for C being Signature holds

( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds

the Arity of C . o in {a_Term} * ) ) );

registration

coherence

for b_{1} being Signature st b_{1} is constructor holds

( not b_{1} is empty & not b_{1} is void )

end;
for b

( not b

proof end;

definition

ex b_{1} being strict Signature st

( b_{1} is constructor & the carrier' of b_{1} = {*,non_op} )

uniqueness

for b_{1}, b_{2} being strict Signature st b_{1} is constructor & the carrier' of b_{1} = {*,non_op} & b_{2} is constructor & the carrier' of b_{2} = {*,non_op} holds

b_{1} = b_{2};

end;

func MinConstrSign -> strict Signature means :Def10: :: ABCMIZ_1:def 10

( it is constructor & the carrier' of it = {*,non_op} );

existence ( it is constructor & the carrier' of it = {*,non_op} );

ex b

( b

proof end;

correctness uniqueness

for b

b

proof end;

:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :

for b_{1} being strict Signature holds

( b_{1} = MinConstrSign iff ( b_{1} is constructor & the carrier' of b_{1} = {*,non_op} ) );

for b

( b

registration
end;

registration
end;

:: deftheorem Def11 defines constructor ABCMIZ_1:def 11 :

for C being ConstructorSignature

for o being OperSymbol of C holds

( o is constructor iff ( o <> * & o <> non_op ) );

for C being ConstructorSignature

for o being OperSymbol of C holds

( o is constructor iff ( o <> * & o <> non_op ) );

theorem :: ABCMIZ_1:37

for S being ConstructorSignature

for o being OperSymbol of S st o is constructor holds

the_arity_of o = (len (the_arity_of o)) |-> a_Term

for o being OperSymbol of S st o is constructor holds

the_arity_of o = (len (the_arity_of o)) |-> a_Term

proof end;

definition

let C be non empty non void Signature;

end;
attr C is initialized means :Def12: :: ABCMIZ_1:def 12

ex m, a being OperSymbol of C st

( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} );

ex m, a being OperSymbol of C st

( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} );

:: deftheorem Def12 defines initialized ABCMIZ_1:def 12 :

for C being non empty non void Signature holds

( C is initialized iff ex m, a being OperSymbol of C st

( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) );

for C being non empty non void Signature holds

( C is initialized iff ex m, a being OperSymbol of C st

( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) );

definition

let C be ConstructorSignature;

A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

coherence

a_Type is SortSymbol of C by A1, ENUMSET1:def 1;

coherence

an_Adj is SortSymbol of C by A1, ENUMSET1:def 1;

coherence

a_Term is SortSymbol of C by A1, ENUMSET1:def 1;

A2: {*,non_op} c= the carrier' of C by Def9;

A3: * in {*,non_op} by TARSKI:def 2;

A4: non_op in {*,non_op} by TARSKI:def 2;

coherence

non_op is OperSymbol of C by A2, A4;

coherence

* is OperSymbol of C by A2, A3;

end;
A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

coherence

a_Type is SortSymbol of C by A1, ENUMSET1:def 1;

coherence

an_Adj is SortSymbol of C by A1, ENUMSET1:def 1;

coherence

a_Term is SortSymbol of C by A1, ENUMSET1:def 1;

A2: {*,non_op} c= the carrier' of C by Def9;

A3: * in {*,non_op} by TARSKI:def 2;

A4: non_op in {*,non_op} by TARSKI:def 2;

coherence

non_op is OperSymbol of C by A2, A4;

coherence

* is OperSymbol of C by A2, A3;

:: deftheorem defines a_Type ABCMIZ_1:def 13 :

for C being ConstructorSignature holds a_Type C = a_Type ;

for C being ConstructorSignature holds a_Type C = a_Type ;

:: deftheorem defines an_Adj ABCMIZ_1:def 14 :

for C being ConstructorSignature holds an_Adj C = an_Adj ;

for C being ConstructorSignature holds an_Adj C = an_Adj ;

:: deftheorem defines a_Term ABCMIZ_1:def 15 :

for C being ConstructorSignature holds a_Term C = a_Term ;

for C being ConstructorSignature holds a_Term C = a_Term ;

:: deftheorem defines non_op ABCMIZ_1:def 16 :

for C being ConstructorSignature holds non_op C = non_op ;

for C being ConstructorSignature holds non_op C = non_op ;

theorem :: ABCMIZ_1:38

for C being ConstructorSignature holds

( the_arity_of (non_op C) = <*(an_Adj C)*> & the_result_sort_of (non_op C) = an_Adj C & the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_result_sort_of (ast C) = a_Type C ) by Def9;

( the_arity_of (non_op C) = <*(an_Adj C)*> & the_result_sort_of (non_op C) = an_Adj C & the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_result_sort_of (ast C) = a_Type C ) by Def9;

definition

correctness

coherence

[:{a_Type},[:QuasiLoci,NAT:]:] is set ;

;

correctness

coherence

[:{an_Adj},[:QuasiLoci,NAT:]:] is set ;

;

correctness

coherence

[:{a_Term},[:QuasiLoci,NAT:]:] is set ;

;

end;
coherence

[:{a_Type},[:QuasiLoci,NAT:]:] is set ;

;

correctness

coherence

[:{an_Adj},[:QuasiLoci,NAT:]:] is set ;

;

correctness

coherence

[:{a_Term},[:QuasiLoci,NAT:]:] is set ;

;

registration
end;

definition

let x be Element of [:QuasiLoci,NAT:];

:: original: vars

redefine func x `1 -> quasi-loci;

coherence

vars x is quasi-loci by MCART_1:10;

:: original: the_base_of

redefine func x `2 -> Element of NAT ;

coherence

the_base_of is Element of NAT by MCART_1:10;

end;
:: original: vars

redefine func x `1 -> quasi-loci;

coherence

vars x is quasi-loci by MCART_1:10;

:: original: the_base_of

redefine func x `2 -> Element of NAT ;

coherence

the_base_of is Element of NAT by MCART_1:10;

definition

let c be Element of Constructors ;

:: original: vars

redefine func kind_of c -> Element of {a_Type,an_Adj,a_Term};

coherence

vars c is Element of {a_Type,an_Adj,a_Term}

redefine func c `2 -> Element of [:QuasiLoci,NAT:];

coherence

the_base_of is Element of [:QuasiLoci,NAT:]

end;
:: original: vars

redefine func kind_of c -> Element of {a_Type,an_Adj,a_Term};

coherence

vars c is Element of {a_Type,an_Adj,a_Term}

proof end;

:: original: the_base_ofredefine func c `2 -> Element of [:QuasiLoci,NAT:];

coherence

the_base_of is Element of [:QuasiLoci,NAT:]

proof end;

definition
end;

:: deftheorem defines loci_of ABCMIZ_1:def 22 :

for c being Element of Constructors holds loci_of c = (c `2) `1 ;

for c being Element of Constructors holds loci_of c = (c `2) `1 ;

:: deftheorem defines index_of ABCMIZ_1:def 23 :

for c being Element of Constructors holds index_of c = (c `2) `2 ;

for c being Element of Constructors holds index_of c = (c `2) `2 ;

theorem :: ABCMIZ_1:40

for c being Element of Constructors holds

( ( kind_of c = a_Type implies c in Modes ) & ( c in Modes implies kind_of c = a_Type ) & ( kind_of c = an_Adj implies c in Attrs ) & ( c in Attrs implies kind_of c = an_Adj ) & ( kind_of c = a_Term implies c in Funcs ) & ( c in Funcs implies kind_of c = a_Term ) )

( ( kind_of c = a_Type implies c in Modes ) & ( c in Modes implies kind_of c = a_Type ) & ( kind_of c = an_Adj implies c in Attrs ) & ( c in Attrs implies kind_of c = an_Adj ) & ( kind_of c = a_Term implies c in Funcs ) & ( c in Funcs implies kind_of c = a_Term ) )

proof end;

definition

ex b_{1} being strict ConstructorSignature st

( the carrier' of b_{1} = {*,non_op} \/ Constructors & ( for o being OperSymbol of b_{1} st o is constructor holds

( the ResultSort of b_{1} . o = o `1 & card ( the Arity of b_{1} . o) = card ((o `2) `1) ) ) )

for b_{1}, b_{2} being strict ConstructorSignature st the carrier' of b_{1} = {*,non_op} \/ Constructors & ( for o being OperSymbol of b_{1} st o is constructor holds

( the ResultSort of b_{1} . o = o `1 & card ( the Arity of b_{1} . o) = card ((o `2) `1) ) ) & the carrier' of b_{2} = {*,non_op} \/ Constructors & ( for o being OperSymbol of b_{2} st o is constructor holds

( the ResultSort of b_{2} . o = o `1 & card ( the Arity of b_{2} . o) = card ((o `2) `1) ) ) holds

b_{1} = b_{2}
end;

func MaxConstrSign -> strict ConstructorSignature means :Def24: :: ABCMIZ_1:def 24

( the carrier' of it = {*,non_op} \/ Constructors & ( for o being OperSymbol of it st o is constructor holds

( the ResultSort of it . o = o `1 & card ( the Arity of it . o) = card ((o `2) `1) ) ) );

existence ( the carrier' of it = {*,non_op} \/ Constructors & ( for o being OperSymbol of it st o is constructor holds

( the ResultSort of it . o = o `1 & card ( the Arity of it . o) = card ((o `2) `1) ) ) );

ex b

( the carrier' of b

( the ResultSort of b

proof end;

uniqueness for b

( the ResultSort of b

( the ResultSort of b

b

proof end;

:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :

for b_{1} being strict ConstructorSignature holds

( b_{1} = MaxConstrSign iff ( the carrier' of b_{1} = {*,non_op} \/ Constructors & ( for o being OperSymbol of b_{1} st o is constructor holds

( the ResultSort of b_{1} . o = o `1 & card ( the Arity of b_{1} . o) = card ((o `2) `1) ) ) ) );

for b

( b

( the ResultSort of b

registration

correctness

coherence

not MinConstrSign is initialized ;

coherence

MaxConstrSign is initialized ;

end;
coherence

not MinConstrSign is initialized ;

proof end;

correctness coherence

MaxConstrSign is initialized ;

proof end;

registration

correctness

existence

ex b_{1} being ConstructorSignature st

( b_{1} is initialized & b_{1} is strict );

end;
existence

ex b

( b

proof end;

registration

let C be initialized ConstructorSignature;

existence

ex b_{1} being OperSymbol of C st b_{1} is constructor

end;
existence

ex b

proof end;

begin

definition

let C be ConstructorSignature;

A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

for b_{1}, b_{2} being ManySortedSet of the carrier of C st b_{1} . a_Type = {} & b_{1} . an_Adj = {} & b_{1} . a_Term = Vars & b_{2} . a_Type = {} & b_{2} . an_Adj = {} & b_{2} . a_Term = Vars holds

b_{1} = b_{2}

ex b_{1} being ManySortedSet of the carrier of C st

( b_{1} . a_Type = {} & b_{1} . an_Adj = {} & b_{1} . a_Term = Vars )

end;
A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

func MSVars C -> ManySortedSet of the carrier of C means :Def25: :: ABCMIZ_1:def 25

( it . a_Type = {} & it . an_Adj = {} & it . a_Term = Vars );

uniqueness ( it . a_Type = {} & it . an_Adj = {} & it . a_Term = Vars );

for b

b

proof end;

existence ex b

( b

proof end;

:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :

for C being ConstructorSignature

for b_{2} being ManySortedSet of the carrier of C holds

( b_{2} = MSVars C iff ( b_{2} . a_Type = {} & b_{2} . an_Adj = {} & b_{2} . a_Term = Vars ) );

for C being ConstructorSignature

for b

( b

:: theorem

:: for C being ConstructorSignature

:: for x being variable holds

:: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11;

:: for C being ConstructorSignature

:: for x being variable holds

:: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11;

registration
end;

registration

let C be initialized ConstructorSignature;

correctness

coherence

Free (C,(MSVars C)) is non-empty ;

end;
correctness

coherence

Free (C,(MSVars C)) is non-empty ;

proof end;

definition

let S be non void Signature;

let X be V9() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

end;
let X be V9() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

:: deftheorem defines ground ABCMIZ_1:def 26 :

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( t is ground iff Union (S variables_in t) = {} );

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( t is ground iff Union (S variables_in t) = {} );

:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( t is compound iff t . {} in [: the carrier' of S,{ the carrier of S}:] );

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for t being Element of (Free (S,X)) holds

( t is compound iff t . {} in [: the carrier' of S,{ the carrier of S}:] );

definition
end;

definition

let C be initialized ConstructorSignature;

let s be SortSymbol of C;

ex b_{1} being expression of C st b_{1} in the Sorts of (Free (C,(MSVars C))) . s

end;
let s be SortSymbol of C;

mode expression of C,s -> expression of C means :Def28: :: ABCMIZ_1:def 28

it in the Sorts of (Free (C,(MSVars C))) . s;

existence it in the Sorts of (Free (C,(MSVars C))) . s;

ex b

proof end;

:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :

for C being initialized ConstructorSignature

for s being SortSymbol of C

for b_{3} being expression of C holds

( b_{3} is expression of C,s iff b_{3} in the Sorts of (Free (C,(MSVars C))) . s );

for C being initialized ConstructorSignature

for s being SortSymbol of C

for b

( b

theorem Th41: :: ABCMIZ_1:41

for z being set

for C being initialized ConstructorSignature

for s being SortSymbol of C holds

( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )

for C being initialized ConstructorSignature

for s being SortSymbol of C holds

( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )

proof end;

definition

let C be initialized ConstructorSignature;

let c be constructor OperSymbol of C;

assume A1: len (the_arity_of c) = 0 ;

coherence

[c, the carrier of C] -tree {} is expression of C

end;
let c be constructor OperSymbol of C;

assume A1: len (the_arity_of c) = 0 ;

coherence

[c, the carrier of C] -tree {} is expression of C

proof end;

:: deftheorem defines term ABCMIZ_1:def 29 :

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds

c term = [c, the carrier of C] -tree {};

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds

c term = [c, the carrier of C] -tree {};

theorem Th42: :: ABCMIZ_1:42

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 1 holds

for a being expression of C st ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & a is expression of C,s ) holds

[o, the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o

for o being OperSymbol of C st len (the_arity_of o) = 1 holds

for a being expression of C st ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & a is expression of C,s ) holds

[o, the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o

proof end;

definition

let C be initialized ConstructorSignature;

let o be OperSymbol of C;

assume A1: len (the_arity_of o) = 1 ;

let e be expression of C;

assume A2: ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & e is expression of C,s ) ;

[o, the carrier of C] -tree <*e*> is expression of C by A1, A2, Th42;

end;
let o be OperSymbol of C;

assume A1: len (the_arity_of o) = 1 ;

let e be expression of C;

assume A2: ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & e is expression of C,s ) ;

func o term e -> expression of C equals :Def30: :: ABCMIZ_1:def 30

[o, the carrier of C] -tree <*e*>;

coherence [o, the carrier of C] -tree <*e*>;

[o, the carrier of C] -tree <*e*> is expression of C by A1, A2, Th42;

:: deftheorem Def30 defines term ABCMIZ_1:def 30 :

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 1 holds

for e being expression of C st ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & e is expression of C,s ) holds

o term e = [o, the carrier of C] -tree <*e*>;

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 1 holds

for e being expression of C st ex s being SortSymbol of C st

( s = (the_arity_of o) . 1 & e is expression of C,s ) holds

o term e = [o, the carrier of C] -tree <*e*>;

theorem Th43: :: ABCMIZ_1:43

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> )

for a being expression of C, an_Adj C holds

( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> )

proof end;

theorem Th44: :: ABCMIZ_1:44

for C being initialized ConstructorSignature

for a, b being expression of C, an_Adj C st (non_op C) term a = (non_op C) term b holds

a = b

for a, b being expression of C, an_Adj C st (non_op C) term a = (non_op C) term b holds

a = b

proof end;

registration

let C be initialized ConstructorSignature;

let a be expression of C, an_Adj C;

coherence

(non_op C) term a is compound

end;
let a be expression of C, an_Adj C;

coherence

(non_op C) term a is compound

proof end;

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C st b_{1} is compound

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like compound for Element of Union the Sorts of (Free (C,(MSVars C)));

existence ex b

proof end;

theorem Th45: :: ABCMIZ_1:45

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 2 holds

for a, b being expression of C st ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds

[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o

for o being OperSymbol of C st len (the_arity_of o) = 2 holds

for a, b being expression of C st ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds

[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o

proof end;

definition

let C be initialized ConstructorSignature;

let o be OperSymbol of C;

assume A1: len (the_arity_of o) = 2 ;

let e1, e2 be expression of C;

assume A2: ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) ;

[o, the carrier of C] -tree <*e1,e2*> is expression of C by A1, A2, Th45;

end;
let o be OperSymbol of C;

assume A1: len (the_arity_of o) = 2 ;

let e1, e2 be expression of C;

assume A2: ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) ;

func o term (e1,e2) -> expression of C equals :Def31: :: ABCMIZ_1:def 31

[o, the carrier of C] -tree <*e1,e2*>;

coherence [o, the carrier of C] -tree <*e1,e2*>;

[o, the carrier of C] -tree <*e1,e2*> is expression of C by A1, A2, Th45;

:: deftheorem Def31 defines term ABCMIZ_1:def 31 :

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 2 holds

for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds

o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>;

for C being initialized ConstructorSignature

for o being OperSymbol of C st len (the_arity_of o) = 2 holds

for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st

( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds

o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>;

theorem Th46: :: ABCMIZ_1:46

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds

( (ast C) term (a,t) is expression of C, a_Type C & (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> )

for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds

( (ast C) term (a,t) is expression of C, a_Type C & (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> )

proof end;

theorem :: ABCMIZ_1:47

for C being initialized ConstructorSignature

for a, b being expression of C, an_Adj C

for t1, t2 being expression of C, a_Type C st (ast C) term (a,t1) = (ast C) term (b,t2) holds

( a = b & t1 = t2 )

for a, b being expression of C, an_Adj C

for t1, t2 being expression of C, a_Type C st (ast C) term (a,t1) = (ast C) term (b,t2) holds

( a = b & t1 = t2 )

proof end;

registration

let C be initialized ConstructorSignature;

let a be expression of C, an_Adj C;

let t be expression of C, a_Type C;

coherence

(ast C) term (a,t) is compound

end;
let a be expression of C, an_Adj C;

let t be expression of C, a_Type C;

coherence

(ast C) term (a,t) is compound

proof end;

definition

let S be non void Signature;

let s be SortSymbol of S;

assume A1: ex o being OperSymbol of S st the_result_sort_of o = s ;

existence

ex b_{1} being OperSymbol of S st the_result_sort_of b_{1} = s
by A1;

end;
let s be SortSymbol of S;

assume A1: ex o being OperSymbol of S st the_result_sort_of o = s ;

existence

ex b

:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :

for S being non void Signature

for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds

for b_{3} being OperSymbol of S holds

( b_{3} is OperSymbol of s iff the_result_sort_of b_{3} = s );

for S being non void Signature

for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds

for b

( b

definition

let C be ConstructorSignature;

:: original: non_op

redefine func non_op C -> OperSymbol of an_Adj C;

coherence

non_op C is OperSymbol of an_Adj C

redefine func ast C -> OperSymbol of a_Type C;

coherence

ast C is OperSymbol of a_Type C

end;
:: original: non_op

redefine func non_op C -> OperSymbol of an_Adj C;

coherence

non_op C is OperSymbol of an_Adj C

proof end;

:: original: astredefine func ast C -> OperSymbol of a_Type C;

coherence

ast C is OperSymbol of a_Type C

proof end;

theorem Th48: :: ABCMIZ_1:48

for C being initialized ConstructorSignature

for s1, s2 being SortSymbol of C st s1 <> s2 holds

for t1 being expression of C,s1

for t2 being expression of C,s2 holds t1 <> t2

for s1, s2 being SortSymbol of C st s1 <> s2 holds

for t1 being expression of C,s1

for t2 being expression of C,s2 holds t1 <> t2

proof end;

begin

definition

let C be initialized ConstructorSignature;

A1: the Sorts of (Free (C,(MSVars C))) . (a_Term C) c= Union the Sorts of (Free (C,(MSVars C)))

the Sorts of (Free (C,(MSVars C))) . (a_Term C) is Subset of (Free (C,(MSVars C))) by A1;

end;
A1: the Sorts of (Free (C,(MSVars C))) . (a_Term C) c= Union the Sorts of (Free (C,(MSVars C)))

proof end;

func QuasiTerms C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 33

the Sorts of (Free (C,(MSVars C))) . (a_Term C);

coherence the Sorts of (Free (C,(MSVars C))) . (a_Term C);

the Sorts of (Free (C,(MSVars C))) . (a_Term C) is Subset of (Free (C,(MSVars C))) by A1;

:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :

for C being initialized ConstructorSignature holds QuasiTerms C = the Sorts of (Free (C,(MSVars C))) . (a_Term C);

for C being initialized ConstructorSignature holds QuasiTerms C = the Sorts of (Free (C,(MSVars C))) . (a_Term C);

registration

let C be initialized ConstructorSignature;

coherence

( not QuasiTerms C is empty & QuasiTerms C is constituted-DTrees )

end;
coherence

( not QuasiTerms C is empty & QuasiTerms C is constituted-DTrees )

proof end;

definition
end;

theorem :: ABCMIZ_1:49

for z being set

for C being initialized ConstructorSignature holds

( z is quasi-term of C iff z in QuasiTerms C ) by Th41;

for C being initialized ConstructorSignature holds

( z is quasi-term of C iff z in QuasiTerms C ) by Th41;

definition

let x be variable;

let C be initialized ConstructorSignature;

coherence

root-tree [x,a_Term] is quasi-term of C

end;
let C be initialized ConstructorSignature;

coherence

root-tree [x,a_Term] is quasi-term of C

proof end;

:: deftheorem defines -term ABCMIZ_1:def 34 :

for x being variable

for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term];

for x being variable

for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term];

theorem Th50: :: ABCMIZ_1:50

for x1, x2 being variable

for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds

x1 = x2

for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds

x1 = x2

proof end;

registration

let x be variable;

let C be initialized ConstructorSignature;

coherence

not x -term C is compound

end;
let C be initialized ConstructorSignature;

coherence

not x -term C is compound

proof end;

theorem Th51: :: ABCMIZ_1:51

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being DTree-yielding FinSequence holds

( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )

for c being constructor OperSymbol of C

for p being DTree-yielding FinSequence holds

( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )

proof end;

definition

let C be initialized ConstructorSignature;

let c be constructor OperSymbol of C;

let p be FinSequence of QuasiTerms C;

assume B1: len p = len (the_arity_of c) ;

A1: p in (QuasiTerms C) * by FINSEQ_1:def 11;

[c, the carrier of C] -tree p is compound expression of C

end;
let c be constructor OperSymbol of C;

let p be FinSequence of QuasiTerms C;

assume B1: len p = len (the_arity_of c) ;

A1: p in (QuasiTerms C) * by FINSEQ_1:def 11;

func c -trm p -> compound expression of C equals :Def35: :: ABCMIZ_1:def 35

[c, the carrier of C] -tree p;

coherence [c, the carrier of C] -tree p;

[c, the carrier of C] -tree p is compound expression of C

proof end;

:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p = [c, the carrier of C] -tree p;

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p = [c, the carrier of C] -tree p;

theorem Th52: :: ABCMIZ_1:52

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p is expression of C, the_result_sort_of c

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p is expression of C, the_result_sort_of c

proof end;

theorem Th53: :: ABCMIZ_1:53

for C being initialized ConstructorSignature

for e being expression of C holds

( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) )

for e being expression of C holds

( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) )

proof end;

theorem Th54: :: ABCMIZ_1:54

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for a being expression of C, an_Adj C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p <> (non_op C) term a

for c being constructor OperSymbol of C

for a being expression of C, an_Adj C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p <> (non_op C) term a

proof end;

theorem Th55: :: ABCMIZ_1:55

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for a being expression of C, an_Adj C

for t being expression of C, a_Type C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p <> (ast C) term (a,t)

for c being constructor OperSymbol of C

for a being expression of C, an_Adj C

for t being expression of C, a_Type C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

c -trm p <> (ast C) term (a,t)

proof end;

theorem :: ABCMIZ_1:56

for C being initialized ConstructorSignature

for a, b being expression of C, an_Adj C

for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term (b,t)

for a, b being expression of C, an_Adj C

for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term (b,t)

proof end;

theorem Th57: :: ABCMIZ_1:57

for C being initialized ConstructorSignature

for e being expression of C st e . {} = [non_op, the carrier of C] holds

ex a being expression of C, an_Adj C st e = (non_op C) term a

for e being expression of C st e . {} = [non_op, the carrier of C] holds

ex a being expression of C, an_Adj C st e = (non_op C) term a

proof end;

theorem Th58: :: ABCMIZ_1:58

for C being initialized ConstructorSignature

for e being expression of C st e . {} = [*, the carrier of C] holds

ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

for e being expression of C st e . {} = [*, the carrier of C] holds

ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

proof end;

begin

definition

let C be initialized ConstructorSignature;

let a be expression of C, an_Adj C;

( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies a | <*0*> is expression of C, an_Adj C ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C ) )

for b_{1} being expression of C, an_Adj C holds verum
;

end;
let a be expression of C, an_Adj C;

func Non a -> expression of C, an_Adj C equals :Def36: :: ABCMIZ_1:def 36

a | <*0*> if ex a9 being expression of C, an_Adj C st a = (non_op C) term a9

otherwise (non_op C) term a;

coherence a | <*0*> if ex a9 being expression of C, an_Adj C st a = (non_op C) term a9

otherwise (non_op C) term a;

( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies a | <*0*> is expression of C, an_Adj C ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C ) )

proof end;

consistency for b

:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) );

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) );

definition

let C be initialized ConstructorSignature;

let a be expression of C, an_Adj C;

end;
let a be expression of C, an_Adj C;

attr a is positive means :Def37: :: ABCMIZ_1:def 37

for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9;

for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9;

:: deftheorem Def37 defines positive ABCMIZ_1:def 37 :

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is positive iff for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 );

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is positive iff for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 );

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C, an_Adj C st b_{1} is positive

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive for expression of C, an_Adj C;

existence ex b

proof end;

theorem Th59: :: ABCMIZ_1:59

for C being initialized ConstructorSignature

for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a

for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a

proof end;

definition

let C be initialized ConstructorSignature;

let a be expression of C, an_Adj C;

end;
let a be expression of C, an_Adj C;

attr a is negative means :Def38: :: ABCMIZ_1:def 38

ex a9 being expression of C, an_Adj C st

( a9 is positive & a = (non_op C) term a9 );

ex a9 being expression of C, an_Adj C st

( a9 is positive & a = (non_op C) term a9 );

:: deftheorem Def38 defines negative ABCMIZ_1:def 38 :

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is negative iff ex a9 being expression of C, an_Adj C st

( a9 is positive & a = (non_op C) term a9 ) );

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is negative iff ex a9 being expression of C, an_Adj C st

( a9 is positive & a = (non_op C) term a9 ) );

registration

let C be initialized ConstructorSignature;

let a be positive expression of C, an_Adj C;

coherence

( Non a is negative & not Non a is positive )

end;
let a be positive expression of C, an_Adj C;

coherence

( Non a is negative & not Non a is positive )

proof end;

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C, an_Adj C st

( b_{1} is negative & not b_{1} is positive )

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like non positive negative for expression of C, an_Adj C;

existence ex b

( b

proof end;

theorem Th60: :: ABCMIZ_1:60

for C being initialized ConstructorSignature

for a being non positive expression of C, an_Adj C ex a9 being expression of C, an_Adj C st

( a = (non_op C) term a9 & Non a = a9 )

for a being non positive expression of C, an_Adj C ex a9 being expression of C, an_Adj C st

( a = (non_op C) term a9 & Non a = a9 )

proof end;

theorem Th61: :: ABCMIZ_1:61

for C being initialized ConstructorSignature

for a being negative expression of C, an_Adj C ex a9 being positive expression of C, an_Adj C st

( a = (non_op C) term a9 & Non a = a9 )

for a being negative expression of C, an_Adj C ex a9 being positive expression of C, an_Adj C st

( a = (non_op C) term a9 & Non a = a9 )

proof end;

theorem Th62: :: ABCMIZ_1:62

for C being initialized ConstructorSignature

for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a

for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a

proof end;

registration

let C be initialized ConstructorSignature;

let a be negative expression of C, an_Adj C;

coherence

Non a is positive

end;
let a be negative expression of C, an_Adj C;

coherence

Non a is positive

proof end;

:: deftheorem Def39 defines regular ABCMIZ_1:def 39 :

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is regular iff ( a is positive or a is negative ) );

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds

( a is regular iff ( a is positive or a is negative ) );

registration

let C be initialized ConstructorSignature;

coherence

for b_{1} being expression of C, an_Adj C st b_{1} is positive holds

( b_{1} is regular & not b_{1} is negative )

for b_{1} being expression of C, an_Adj C st b_{1} is negative holds

( b_{1} is regular & not b_{1} is positive )
by Def39;

end;
coherence

for b

( b

proof end;

coherence for b

( b

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C, an_Adj C st b_{1} is regular

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like regular for expression of C, an_Adj C;

existence ex b

proof end;

definition

let C be initialized ConstructorSignature;

set X = { a where a is expression of C, an_Adj C : a is regular } ;

A1: { a where a is expression of C, an_Adj C : a is regular } c= Union the Sorts of (Free (C,(MSVars C)))

{ a where a is expression of C, an_Adj C : a is regular } is Subset of (Free (C,(MSVars C))) by A1;

end;
set X = { a where a is expression of C, an_Adj C : a is regular } ;

A1: { a where a is expression of C, an_Adj C : a is regular } c= Union the Sorts of (Free (C,(MSVars C)))

proof end;

func QuasiAdjs C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 40

{ a where a is expression of C, an_Adj C : a is regular } ;

coherence { a where a is expression of C, an_Adj C : a is regular } ;

{ a where a is expression of C, an_Adj C : a is regular } is Subset of (Free (C,(MSVars C))) by A1;

:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :

for C being initialized ConstructorSignature holds QuasiAdjs C = { a where a is expression of C, an_Adj C : a is regular } ;

for C being initialized ConstructorSignature holds QuasiAdjs C = { a where a is expression of C, an_Adj C : a is regular } ;

registration

let C be initialized ConstructorSignature;

coherence

( not QuasiAdjs C is empty & QuasiAdjs C is constituted-DTrees )

end;
coherence

( not QuasiAdjs C is empty & QuasiAdjs C is constituted-DTrees )

proof end;

definition

let C be initialized ConstructorSignature;

mode quasi-adjective of C is regular expression of C, an_Adj C;

end;
mode quasi-adjective of C is regular expression of C, an_Adj C;

theorem Th63: :: ABCMIZ_1:63

for z being set

for C being initialized ConstructorSignature holds

( z is quasi-adjective of C iff z in QuasiAdjs C )

for C being initialized ConstructorSignature holds

( z is quasi-adjective of C iff z in QuasiAdjs C )

proof end;

theorem :: ABCMIZ_1:64

for z being set

for C being initialized ConstructorSignature holds

( z is quasi-adjective of C iff ( z is positive expression of C, an_Adj C or z is negative expression of C, an_Adj C ) ) by Def39;

for C being initialized ConstructorSignature holds

( z is quasi-adjective of C iff ( z is positive expression of C, an_Adj C or z is negative expression of C, an_Adj C ) ) by Def39;

registration

let C be initialized ConstructorSignature;

coherence

for b_{1} being quasi-adjective of C st not b_{1} is positive holds

b_{1} is negative
by Def39;

coherence

for b_{1} being quasi-adjective of C st not b_{1} is negative holds

b_{1} is positive
;

end;
coherence

for b

b

coherence

for b

b

registration

let C be initialized ConstructorSignature;

ex b_{1} being quasi-adjective of C st b_{1} is positive

ex b_{1} being quasi-adjective of C st b_{1} is negative

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive regular for expression of C, an_Adj C;

existence ex b

proof end;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like negative regular for expression of C, an_Adj C;

existence ex b

proof end;

theorem Th65: :: ABCMIZ_1:65

for C being initialized ConstructorSignature

for a being positive quasi-adjective of C ex v being constructor OperSymbol of C st

( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of v) & a = v -trm p ) )

for a being positive quasi-adjective of C ex v being constructor OperSymbol of C st

( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of v) & a = v -trm p ) )

proof end;

theorem Th66: :: ABCMIZ_1:66

for C being initialized ConstructorSignature

for p being FinSequence of QuasiTerms C

for v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C & len p = len (the_arity_of v) holds

v -trm p is positive quasi-adjective of C

for p being FinSequence of QuasiTerms C

for v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C & len p = len (the_arity_of v) holds

v -trm p is positive quasi-adjective of C

proof end;

registration

let C be initialized ConstructorSignature;

let a be quasi-adjective of C;

coherence

Non a is regular

end;
let a be quasi-adjective of C;

coherence

Non a is regular

proof end;

theorem :: ABCMIZ_1:68

for C being initialized ConstructorSignature

for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds

a1 = a2

for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds

a1 = a2

proof end;

begin

definition

let C be initialized ConstructorSignature;

let q be expression of C, a_Type C;

end;
let q be expression of C, a_Type C;

attr q is pure means :Def41: :: ABCMIZ_1:def 41

for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds not q = (ast C) term (a,t);

for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds not q = (ast C) term (a,t);

:: deftheorem Def41 defines pure ABCMIZ_1:def 41 :

for C being initialized ConstructorSignature

for q being expression of C, a_Type C holds

( q is pure iff for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds not q = (ast C) term (a,t) );

for C being initialized ConstructorSignature

for q being expression of C, a_Type C holds

( q is pure iff for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds not q = (ast C) term (a,t) );

theorem Th70: :: ABCMIZ_1:70

for C being initialized ConstructorSignature

for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} holds

ex t being expression of C, a_Type C st

( t = root-tree [m, the carrier of C] & t is pure )

for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} holds

ex t being expression of C, a_Type C st

( t = root-tree [m, the carrier of C] & t is pure )

proof end;

theorem Th71: :: ABCMIZ_1:71

for C being initialized ConstructorSignature

for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} holds

ex a being expression of C, an_Adj C st

( a = root-tree [v, the carrier of C] & a is positive )

for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} holds

ex a being expression of C, an_Adj C st

( a = root-tree [v, the carrier of C] & a is positive )

proof end;

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C, a_Type C st b_{1} is pure

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like pure for expression of C, a_Type C;

existence ex b

proof end;

definition

let C be initialized ConstructorSignature;

{ [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } is set ;

end;
func QuasiTypes C -> set equals :: ABCMIZ_1:def 42

{ [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

coherence { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

{ [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } is set ;

:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :

for C being initialized ConstructorSignature holds QuasiTypes C = { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

for C being initialized ConstructorSignature holds QuasiTypes C = { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

registration
end;

definition

let C be initialized ConstructorSignature;

existence

ex b_{1} being set st b_{1} in QuasiTypes C

end;
existence

ex b

proof end;

:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :

for C being initialized ConstructorSignature

for b_{2} being set holds

( b_{2} is quasi-type of C iff b_{2} in QuasiTypes C );

for C being initialized ConstructorSignature

for b

( b

theorem Th72: :: ABCMIZ_1:72

for z being set

for C being initialized ConstructorSignature holds

( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )

for C being initialized ConstructorSignature holds

( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )

proof end;

theorem Th73: :: ABCMIZ_1:73

for x, y being set

for C being initialized ConstructorSignature holds

( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) )

for C being initialized ConstructorSignature holds

( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) )

proof end;

registration

let C be initialized ConstructorSignature;

coherence

for b_{1} being quasi-type of C holds b_{1} is pair

end;
coherence

for b

proof end;

theorem Th74: :: ABCMIZ_1:74

for C being initialized ConstructorSignature

for q being pure expression of C, a_Type C ex m being constructor OperSymbol of C st

( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of m) & q = m -trm p ) )

for q being pure expression of C, a_Type C ex m being constructor OperSymbol of C st

( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st

( len p = len (the_arity_of m) & q = m -trm p ) )

proof end;

theorem Th75: :: ABCMIZ_1:75

for C being initialized ConstructorSignature

for p being FinSequence of QuasiTerms C

for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds

m -trm p is pure expression of C, a_Type C

for p being FinSequence of QuasiTerms C

for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds

m -trm p is pure expression of C, a_Type C

proof end;

theorem :: ABCMIZ_1:76

for C being initialized ConstructorSignature holds

( QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )

( QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )

proof end;

theorem :: ABCMIZ_1:77

for C being initialized ConstructorSignature

for e being set holds

( ( e is quasi-term of C implies not e is quasi-adjective of C ) & ( e is quasi-term of C implies not e is quasi-type of C ) & ( e is quasi-type of C implies not e is quasi-adjective of C ) ) by Th48;

for e being set holds

( ( e is quasi-term of C implies not e is quasi-adjective of C ) & ( e is quasi-term of C implies not e is quasi-type of C ) & ( e is quasi-type of C implies not e is quasi-adjective of C ) ) by Th48;

notation

let C be initialized ConstructorSignature;

let A be finite Subset of (QuasiAdjs C);

let q be pure expression of C, a_Type C;

synonym A ast q for [C,A];

end;
let A be finite Subset of (QuasiAdjs C);

let q be pure expression of C, a_Type C;

synonym A ast q for [C,A];

definition

let C be initialized ConstructorSignature;

let A be finite Subset of (QuasiAdjs C);

let q be pure expression of C, a_Type C;

:: original: ast

redefine func A ast q -> quasi-type of C;

coherence

q ast is quasi-type of C by Th73;

end;
let A be finite Subset of (QuasiAdjs C);

let q be pure expression of C, a_Type C;

:: original: ast

redefine func A ast q -> quasi-type of C;

coherence

q ast is quasi-type of C by Th73;

registration

let C be initialized ConstructorSignature;

let T be quasi-type of C;

coherence

T `1 is finite

end;
let T be quasi-type of C;

coherence

T `1 is finite

proof end;

notation

let C be initialized ConstructorSignature;

let T be quasi-type of C;

synonym adjs T for C `1 ;

synonym the_base_of T for C `2 ;

end;
let T be quasi-type of C;

synonym adjs T for C `1 ;

synonym the_base_of T for C `2 ;

definition

let C be initialized ConstructorSignature;

let T be quasi-type of C;

:: original: vars

redefine func adjs T -> Subset of (QuasiAdjs C);

coherence

vars T is Subset of (QuasiAdjs C)

redefine func the_base_of T -> pure expression of C, a_Type C;

coherence

the_base_of is pure expression of C, a_Type C

end;
let T be quasi-type of C;

:: original: vars

redefine func adjs T -> Subset of (QuasiAdjs C);

coherence

vars T is Subset of (QuasiAdjs C)

proof end;

:: original: the_base_ofredefine func the_base_of T -> pure expression of C, a_Type C;

coherence

the_base_of is pure expression of C, a_Type C

proof end;

theorem :: ABCMIZ_1:78

for C being initialized ConstructorSignature

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds

( adjs (A ast q) = A & the_base_of (A ast q) = q ) ;

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds

( adjs (A ast q) = A & the_base_of (A ast q) = q ) ;

theorem :: ABCMIZ_1:79

for C being initialized ConstructorSignature

for A1, A2 being finite Subset of (QuasiAdjs C)

for q1, q2 being pure expression of C, a_Type C st A1 ast q1 = A2 ast q2 holds

( A1 = A2 & q1 = q2 ) by XTUPLE_0:1;

for A1, A2 being finite Subset of (QuasiAdjs C)

for q1, q2 being pure expression of C, a_Type C st A1 ast q1 = A2 ast q2 holds

( A1 = A2 & q1 = q2 ) by XTUPLE_0:1;

theorem Th80: :: ABCMIZ_1:80

for C being initialized ConstructorSignature

for T being quasi-type of C holds T = (adjs T) ast (the_base_of T)

for T being quasi-type of C holds T = (adjs T) ast (the_base_of T)

proof end;

theorem :: ABCMIZ_1:81

for C being initialized ConstructorSignature

for T1, T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds

T1 = T2

for T1, T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds

T1 = T2

proof end;

definition

let C be initialized ConstructorSignature;

let T be quasi-type of C;

let a be quasi-adjective of C;

coherence

[({a} \/ (adjs T)),(the_base_of T)] is quasi-type of C

end;
let T be quasi-type of C;

let a be quasi-adjective of C;

coherence

[({a} \/ (adjs T)),(the_base_of T)] is quasi-type of C

proof end;

:: deftheorem defines ast ABCMIZ_1:def 44 :

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds a ast T = [({a} \/ (adjs T)),(the_base_of T)];

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds a ast T = [({a} \/ (adjs T)),(the_base_of T)];

theorem :: ABCMIZ_1:82

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds

( adjs (a ast T) = {a} \/ (adjs T) & the_base_of (a ast T) = the_base_of T ) by MCART_1:7;

for T being quasi-type of C

for a being quasi-adjective of C holds

( adjs (a ast T) = {a} \/ (adjs T) & the_base_of (a ast T) = the_base_of T ) by MCART_1:7;

theorem :: ABCMIZ_1:83

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds a ast (a ast T) = a ast T

for T being quasi-type of C

for a being quasi-adjective of C holds a ast (a ast T) = a ast T

proof end;

theorem :: ABCMIZ_1:84

for C being initialized ConstructorSignature

for T being quasi-type of C

for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T)

for T being quasi-type of C

for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T)

proof end;

begin

registration

let S be non void Signature;

let s be SortSymbol of S;

let X be V8() ManySortedSet of the carrier of S;

let t be Term of S,X;

coherence

(variables_in t) . s is finite

end;
let s be SortSymbol of S;

let X be V8() ManySortedSet of the carrier of S;

let t be Term of S,X;

coherence

(variables_in t) . s is finite

proof end;

registration

let S be non void Signature;

let s be SortSymbol of S;

let X be V9() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

coherence

(S variables_in t) . s is finite

end;
let s be SortSymbol of S;

let X be V9() ManySortedSet of the carrier of S;

let t be Element of (Free (S,X));

coherence

(S variables_in t) . s is finite

proof end;

definition

let S be non void Signature;

let X be V9() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

for b_{1}, b_{2} being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st ( for t being Element of (Free (S,X)) holds b_{1} . t = (S variables_in t) . s ) & ( for t being Element of (Free (S,X)) holds b_{2} . t = (S variables_in t) . s ) holds

b_{1} = b_{2}

ex b_{1} being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st

for t being Element of (Free (S,X)) holds b_{1} . t = (S variables_in t) . s

end;
let X be V9() ManySortedSet of the carrier of S;

let s be SortSymbol of S;

func (X,s) variables_in -> Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) means :Def45: :: ABCMIZ_1:def 45

for t being Element of (Free (S,X)) holds it . t = (S variables_in t) . s;

uniqueness for t being Element of (Free (S,X)) holds it . t = (S variables_in t) . s;

for b

b

proof end;

existence ex b

for t being Element of (Free (S,X)) holds b

proof end;

:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b_{4} being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds

( b_{4} = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b_{4} . t = (S variables_in t) . s );

for S being non void Signature

for X being V9() ManySortedSet of the carrier of S

for s being SortSymbol of S

for b

( b

definition

let C be initialized ConstructorSignature;

let e be expression of C;

coherence

(C variables_in e) . (a_Term C) is Subset of Vars

end;
let e be expression of C;

coherence

(C variables_in e) . (a_Term C) is Subset of Vars

proof end;

:: deftheorem defines variables_in ABCMIZ_1:def 46 :

for C being initialized ConstructorSignature

for e being expression of C holds variables_in e = (C variables_in e) . (a_Term C);

for C being initialized ConstructorSignature

for e being expression of C holds variables_in e = (C variables_in e) . (a_Term C);

registration

let C be initialized ConstructorSignature;

let e be expression of C;

coherence

variables_in e is finite ;

end;
let e be expression of C;

coherence

variables_in e is finite ;

definition

let C be initialized ConstructorSignature;

let e be expression of C;

coherence

varcl (variables_in e) is finite Subset of Vars by Th24;

end;
let e be expression of C;

coherence

varcl (variables_in e) is finite Subset of Vars by Th24;

:: deftheorem defines vars ABCMIZ_1:def 47 :

for C being initialized ConstructorSignature

for e being expression of C holds vars e = varcl (variables_in e);

for C being initialized ConstructorSignature

for e being expression of C holds vars e = varcl (variables_in e);

theorem :: ABCMIZ_1:85

for C being initialized ConstructorSignature

for e being expression of C holds varcl (vars e) = vars e ;

for e being expression of C holds varcl (vars e) = vars e ;

theorem :: ABCMIZ_1:86

for C being initialized ConstructorSignature

for x being variable holds variables_in (x -term C) = {x} by MSAFREE3:10;

for x being variable holds variables_in (x -term C) = {x} by MSAFREE3:10;

theorem :: ABCMIZ_1:87

for C being initialized ConstructorSignature

for x being variable holds vars (x -term C) = {x} \/ (vars x)

for x being variable holds vars (x -term C) = {x} \/ (vars x)

proof end;

theorem Th88: :: ABCMIZ_1:88

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for e being expression of C

for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds

variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }

for c being constructor OperSymbol of C

for e being expression of C

for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds

variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }

proof end;

theorem Th89: :: ABCMIZ_1:89

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for e being expression of C

for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds

vars e = union { (vars t) where t is quasi-term of C : t in rng p }

for c being constructor OperSymbol of C

for e being expression of C

for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds

vars e = union { (vars t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:90

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:91

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

vars (c -trm p) = union { (vars t) where t is quasi-term of C : t in rng p }

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds

vars (c -trm p) = union { (vars t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:92

for S being ManySortedSign

for o being set holds S variables_in ([o, the carrier of S] -tree {}) = [[0]] the carrier of S

for o being set holds S variables_in ([o, the carrier of S] -tree {}) = [[0]] the carrier of S

proof end;

theorem Th93: :: ABCMIZ_1:93

for S being ManySortedSign

for o being set

for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t

for o being set

for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t

proof end;

theorem Th94: :: ABCMIZ_1:94

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a

for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a

proof end;

theorem :: ABCMIZ_1:95

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds vars ((non_op C) term a) = vars a by Th94;

for a being expression of C, an_Adj C holds vars ((non_op C) term a) = vars a by Th94;

theorem Th96: :: ABCMIZ_1:96

for S being ManySortedSign

for o being set

for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) \/ (S variables_in t2)

for o being set

for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) \/ (S variables_in t2)

proof end;

theorem Th97: :: ABCMIZ_1:97

for C being initialized ConstructorSignature

for t being expression of C, a_Type C

for a being expression of C, an_Adj C holds variables_in ((ast C) term (a,t)) = (variables_in a) \/ (variables_in t)

for t being expression of C, a_Type C

for a being expression of C, an_Adj C holds variables_in ((ast C) term (a,t)) = (variables_in a) \/ (variables_in t)

proof end;

theorem :: ABCMIZ_1:98

for C being initialized ConstructorSignature

for t being expression of C, a_Type C

for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t)

for t being expression of C, a_Type C

for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t)

proof end;

theorem Th99: :: ABCMIZ_1:99

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds variables_in (Non a) = variables_in a

for a being expression of C, an_Adj C holds variables_in (Non a) = variables_in a

proof end;

theorem :: ABCMIZ_1:100

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C holds vars (Non a) = vars a by Th99;

for a being expression of C, an_Adj C holds vars (Non a) = vars a by Th99;

definition

let C be initialized ConstructorSignature;

let T be quasi-type of C;

(union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)) is Subset of Vars

end;
let T be quasi-type of C;

func variables_in T -> Subset of Vars equals :: ABCMIZ_1:def 48

(union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

coherence (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

(union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)) is Subset of Vars

proof end;

:: deftheorem defines variables_in ABCMIZ_1:def 48 :

for C being initialized ConstructorSignature

for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

for C being initialized ConstructorSignature

for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

registration

let C be initialized ConstructorSignature;

let T be quasi-type of C;

coherence

variables_in T is finite

end;
let T be quasi-type of C;

coherence

variables_in T is finite

proof end;

definition

let C be initialized ConstructorSignature;

let T be quasi-type of C;

coherence

varcl (variables_in T) is finite Subset of Vars by Th24;

end;
let T be quasi-type of C;

coherence

varcl (variables_in T) is finite Subset of Vars by Th24;

:: deftheorem defines vars ABCMIZ_1:def 49 :

for C being initialized ConstructorSignature

for T being quasi-type of C holds vars T = varcl (variables_in T);

for C being initialized ConstructorSignature

for T being quasi-type of C holds vars T = varcl (variables_in T);

theorem :: ABCMIZ_1:101

for C being initialized ConstructorSignature

for T being quasi-type of C holds varcl (vars T) = vars T ;

for T being quasi-type of C holds varcl (vars T) = vars T ;

theorem Th102: :: ABCMIZ_1:102

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T)

for T being quasi-type of C

for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T)

proof end;

theorem :: ABCMIZ_1:103

for C being initialized ConstructorSignature

for T being quasi-type of C

for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T)

for T being quasi-type of C

for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T)

proof end;

theorem Th104: :: ABCMIZ_1:104

for C being initialized ConstructorSignature

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)

proof end;

theorem :: ABCMIZ_1:105

for C being initialized ConstructorSignature

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)

for q being pure expression of C, a_Type C

for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)

proof end;

theorem Th106: :: ABCMIZ_1:106

for C being initialized ConstructorSignature

for q being pure expression of C, a_Type C holds variables_in (({} (QuasiAdjs C)) ast q) = variables_in q

for q being pure expression of C, a_Type C holds variables_in (({} (QuasiAdjs C)) ast q) = variables_in q

proof end;

theorem Th107: :: ABCMIZ_1:107

for C being initialized ConstructorSignature

for e being expression of C holds

( e is ground iff variables_in e = {} )

for e being expression of C holds

( e is ground iff variables_in e = {} )

proof end;

:: deftheorem Def50 defines ground ABCMIZ_1:def 50 :

for C being initialized ConstructorSignature

for T being quasi-type of C holds

( T is ground iff variables_in T = {} );

for C being initialized ConstructorSignature

for T being quasi-type of C holds

( T is ground iff variables_in T = {} );

registration

let C be initialized ConstructorSignature;

ex b_{1} being expression of C, a_Type C st

( b_{1} is ground & b_{1} is pure )

ex b_{1} being quasi-adjective of C st b_{1} is ground

end;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground pure for expression of C, a_Type C;

existence ex b

( b

proof end;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground regular for expression of C, an_Adj C;

existence ex b

proof end;

theorem Th108: :: ABCMIZ_1:108

for C being initialized ConstructorSignature

for t being ground pure expression of C, a_Type C holds ({} (QuasiAdjs C)) ast t is ground

for t being ground pure expression of C, a_Type C holds ({} (QuasiAdjs C)) ast t is ground

proof end;

registration

let C be initialized ConstructorSignature;

let t be ground pure expression of C, a_Type C;

coherence

for b_{1} being quasi-type of C st b_{1} = ({} (QuasiAdjs C)) ast t holds

b_{1} is ground
by Th108;

end;
let t be ground pure expression of C, a_Type C;

coherence

for b

b

registration

let C be initialized ConstructorSignature;

existence

ex b_{1} being quasi-type of C st b_{1} is ground

end;
existence

ex b

proof end;

registration

let C be initialized ConstructorSignature;

let T be ground quasi-type of C;

let a be ground quasi-adjective of C;

coherence

a ast T is ground

end;
let T be ground quasi-type of C;

let a be ground quasi-adjective of C;

coherence

a ast T is ground

proof end;

begin

:: Type widening is smooth iff

:: vars-function is sup-semilattice homomorphism from widening sup-semilattice

:: into VarPoset

:: vars-function is sup-semilattice homomorphism from widening sup-semilattice

:: into VarPoset

definition

(InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp is non empty strict Poset
end;

func VarPoset -> non empty strict Poset equals :: ABCMIZ_1:def 51

(InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;

coherence (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;

(InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp is non empty strict Poset

proof end;

:: deftheorem defines VarPoset ABCMIZ_1:def 51 :

VarPoset = (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;

VarPoset = (InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;

:: registration

:: let V1,V2 be Element of VarPoset;

:: identify V1 <= V2 with V2 c= V1;

:: compatibility by Th22;

:: end;

:: let V1,V2 be Element of VarPoset;

:: identify V1 <= V2 with V2 c= V1;

:: compatibility by Th22;

:: end;

registration

let V1, V2 be Element of VarPoset;

compatibility

V1 "\/" V2 = V1 /\ V2 by Th111;

compatibility

V1 "/\" V2 = V1 \/ V2 by Th111;

end;
compatibility

V1 "\/" V2 = V1 /\ V2 by Th111;

compatibility

V1 "/\" V2 = V1 \/ V2 by Th111;

registration
end;

definition

let C be initialized ConstructorSignature;

for b_{1}, b_{2} being Function of (QuasiTypes C), the carrier of VarPoset st ( for T being quasi-type of C holds b_{1} . T = vars T ) & ( for T being quasi-type of C holds b_{2} . T = vars T ) holds

b_{1} = b_{2}

ex b_{1} being Function of (QuasiTypes C), the carrier of VarPoset st

for T being quasi-type of C holds b_{1} . T = vars T

end;
func vars-function C -> Function of (QuasiTypes C), the carrier of VarPoset means :: ABCMIZ_1:def 52

for T being quasi-type of C holds it . T = vars T;

uniqueness for T being quasi-type of C holds it . T = vars T;

for b

b

proof end;

existence ex b

for T being quasi-type of C holds b

proof end;

:: deftheorem defines vars-function ABCMIZ_1:def 52 :

for C being initialized ConstructorSignature

for b_{2} being Function of (QuasiTypes C), the carrier of VarPoset holds

( b_{2} = vars-function C iff for T being quasi-type of C holds b_{2} . T = vars T );

for C being initialized ConstructorSignature

for b

( b

definition

let L be non empty Poset;

end;
attr L is smooth means :: ABCMIZ_1:def 53

ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st

( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) );

ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st

( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) );

:: deftheorem defines smooth ABCMIZ_1:def 53 :

for L being non empty Poset holds

( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st

( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) );

for L being non empty Poset holds

( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st

( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) );

registration

let C be initialized ConstructorSignature;

let T be ground quasi-type of C;

coherence

RelStr(# {T},(id {T}) #) is smooth

end;
let T be ground quasi-type of C;

coherence

RelStr(# {T},(id {T}) #) is smooth

proof end;

begin

scheme :: ABCMIZ_1:sch 2

StructInd{ F_{1}() -> initialized ConstructorSignature, P_{1}[ set ], F_{2}() -> expression of F_{1}() } :

provided

StructInd{ F

provided

A1:
for x being variable holds P_{1}[x -term F_{1}()]
and

A2: for c being constructor OperSymbol of F_{1}()

for p being FinSequence of QuasiTerms F_{1}() st len p = len (the_arity_of c) & ( for t being quasi-term of F_{1}() st t in rng p holds

P_{1}[t] ) holds

P_{1}[c -trm p]
and

A3: for a being expression of F_{1}(), an_Adj F_{1}() st P_{1}[a] holds

P_{1}[(non_op F_{1}()) term a]
and

A4: for a being expression of F_{1}(), an_Adj F_{1}() st P_{1}[a] holds

for t being expression of F_{1}(), a_Type F_{1}() st P_{1}[t] holds

P_{1}[(ast F_{1}()) term (a,t)]

A2: for c being constructor OperSymbol of F

for p being FinSequence of QuasiTerms F

P

P

A3: for a being expression of F

P

A4: for a being expression of F

for t being expression of F

P

proof end;

definition

let S be ManySortedSign ;

end;
attr S is with_an_operation_for_each_sort means :Def54: :: ABCMIZ_1:def 54

the carrier of S c= rng the ResultSort of S;

let X be ManySortedSet of the carrier of S;the carrier of S c= rng the ResultSort of S;

attr X is with_missing_variables means :Def55: :: ABCMIZ_1:def 55

X " {{}} c= rng the ResultSort of S;

X " {{}} c= rng the ResultSort of S;

:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :

for S being ManySortedSign holds

( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S );

for S being ManySortedSign holds

( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S );

:: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def 55 :

for S being ManySortedSign

for X being ManySortedSet of the carrier of S holds

( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S );

for S being ManySortedSign

for X being ManySortedSet of the carrier of S holds

( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S );

theorem Th114: :: ABCMIZ_1:114

for S being non void Signature

for X being ManySortedSet of the carrier of S holds

( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds

ex o being OperSymbol of S st the_result_sort_of o = s )

for X being ManySortedSet of the carrier of S holds

( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds

ex o being OperSymbol of S st the_result_sort_of o = s )

proof end;

registration

coherence

MaxConstrSign is with_an_operation_for_each_sort

coherence

MSVars C is with_missing_variables

end;
MaxConstrSign is with_an_operation_for_each_sort

proof end;

let C be ConstructorSignature;coherence

MSVars C is with_missing_variables

proof end;

registration

let S be ManySortedSign ;

for b_{1} being ManySortedSet of the carrier of S st b_{1} is V8() holds

b_{1} is with_missing_variables

end;
cluster Relation-like V8() the carrier of S -defined Function-like total -> with_missing_variables for set ;

coherence for b

b

proof end;

registration

let S be ManySortedSign ;

ex b_{1} being ManySortedSet of the carrier of S st b_{1} is with_missing_variables

end;
cluster Relation-like the carrier of S -defined Function-like total with_missing_variables for set ;

existence ex b

proof end;

registration

ex b_{1} being ConstructorSignature st

( b_{1} is initialized & b_{1} is with_an_operation_for_each_sort & b_{1} is strict )
end;

cluster non empty non void V58() strict V259() constructor initialized with_an_operation_for_each_sort for ManySortedSign ;

existence ex b

( b

proof end;

registration

let C be with_an_operation_for_each_sort ManySortedSign ;

for b_{1} being ManySortedSet of the carrier of C holds b_{1} is with_missing_variables

end;
cluster Relation-like the carrier of C -defined Function-like total -> with_missing_variables for set ;

coherence for b

proof end;

definition

let G be non empty DTConstrStr ;

:: original: Terminals

redefine func Terminals G -> Subset of G;

coherence

Terminals G is Subset of G

redefine func NonTerminals G -> Subset of G;

coherence

NonTerminals G is Subset of G

end;
:: original: Terminals

redefine func Terminals G -> Subset of G;

coherence

Terminals G is Subset of G

proof end;

:: original: NonTerminalsredefine func NonTerminals G -> Subset of G;

coherence

NonTerminals G is Subset of G

proof end;

theorem Th115: :: ABCMIZ_1:115

for D1, D2 being non empty DTConstrStr st the Rules of D1 c= the Rules of D2 holds

( NonTerminals D1 c= NonTerminals D2 & the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) )

( NonTerminals D1 c= NonTerminals D2 & the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) )

proof end;

theorem Th116: :: ABCMIZ_1:116

for D1, D2 being non empty DTConstrStr st Terminals D1 c= Terminals D2 & the Rules of D1 c= the Rules of D2 holds

TS D1 c= TS D2

TS D1 c= TS D2

proof end;

theorem Th117: :: ABCMIZ_1:117

for S being ManySortedSign

for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds

Y is with_missing_variables

for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds

Y is with_missing_variables

proof end;

theorem Th118: :: ABCMIZ_1:118

for S being set

for X, Y being ManySortedSet of S st X c= Y holds

Union (coprod X) c= Union (coprod Y)

for X, Y being ManySortedSet of S st X c= Y holds

Union (coprod X) c= Union (coprod Y)

proof end;

theorem :: ABCMIZ_1:119

theorem Th120: :: ABCMIZ_1:120

for S being non void Signature

for X being ManySortedSet of the carrier of S st X is with_missing_variables holds

( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )

for X being ManySortedSet of the carrier of S st X is with_missing_variables holds

( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )

proof end;

theorem :: ABCMIZ_1:121

for S being non void Signature

for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds

( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )

for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds

( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )

proof end;

theorem Th122: :: ABCMIZ_1:122

for C being initialized ConstructorSignature

for t being set holds

( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )

for t being set holds

( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )

proof end;

theorem Th123: :: ABCMIZ_1:123

for C being initialized ConstructorSignature

for t being set holds

( t in NonTerminals (DTConMSA (MSVars C)) iff ( t = [(ast C), the carrier of C] or t = [(non_op C), the carrier of C] or ex c being constructor OperSymbol of C st t = [c, the carrier of C] ) )

for t being set holds

( t in NonTerminals (DTConMSA (MSVars C)) iff ( t = [(ast C), the carrier of C] or t = [(non_op C), the carrier of C] or ex c being constructor OperSymbol of C st t = [c, the carrier of C] ) )

proof end;

theorem Th124: :: ABCMIZ_1:124

for S being non void Signature

for X being with_missing_variables ManySortedSet of the carrier of S

for t being set st t in Union the Sorts of (Free (S,X)) holds

t is Term of S,(X \/ ( the carrier of S --> {0}))

for X being with_missing_variables ManySortedSet of the carrier of S

for t being set st t in Union the Sorts of (Free (S,X)) holds

t is Term of S,(X \/ ( the carrier of S --> {0}))

proof end;

theorem :: ABCMIZ_1:125

for S being non void Signature

for X being with_missing_variables ManySortedSet of the carrier of S

for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds

t in the Sorts of (Free (S,X)) . (the_sort_of t)

for X being with_missing_variables ManySortedSet of the carrier of S

for t being Term of S,(X \/ ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds

t in the Sorts of (Free (S,X)) . (the_sort_of t)

proof end;

theorem :: ABCMIZ_1:126

for G being non empty DTConstrStr

for s being Element of G

for p being FinSequence st s ==> p holds

p is FinSequence of the carrier of G

for s being Element of G

for p being FinSequence st s ==> p holds

p is FinSequence of the carrier of G

proof end;

theorem Th127: :: ABCMIZ_1:127

for S being non void Signature

for X, Y being ManySortedSet of the carrier of S

for g1 being Symbol of (DTConMSA X)

for g2 being Symbol of (DTConMSA Y)

for p1 being FinSequence of the carrier of (DTConMSA X)

for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds

g2 ==> p2

for X, Y being ManySortedSet of the carrier of S

for g1 being Symbol of (DTConMSA X)

for g2 being Symbol of (DTConMSA Y)

for p1 being FinSequence of the carrier of (DTConMSA X)

for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds

g2 ==> p2

proof end;

theorem Th128: :: ABCMIZ_1:128

for S being non void Signature

for X being with_missing_variables ManySortedSet of the carrier of S holds Union the Sorts of (Free (S,X)) = TS (DTConMSA X)

for X being with_missing_variables ManySortedSet of the carrier of S holds Union the Sorts of (Free (S,X)) = TS (DTConMSA X)

proof end;

definition

let S be non void Signature;

let X be ManySortedSet of the carrier of S;

ex b_{1} being UnOp of (Union the Sorts of (Free (S,X))) st

for s being SortSymbol of S holds b_{1} .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s

end;
let X be ManySortedSet of the carrier of S;

mode term-transformation of S,X -> UnOp of (Union the Sorts of (Free (S,X))) means :Def56: :: ABCMIZ_1:def 56

for s being SortSymbol of S holds it .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s;

existence for s being SortSymbol of S holds it .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s;

ex b

for s being SortSymbol of S holds b

proof end;

:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :

for S being non void Signature

for X being ManySortedSet of the carrier of S

for b_{3} being UnOp of (Union the Sorts of (Free (S,X))) holds

( b_{3} is term-transformation of S,X iff for s being SortSymbol of S holds b_{3} .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s );

for S being non void Signature

for X being ManySortedSet of the carrier of S

for b

( b

theorem Th129: :: ABCMIZ_1:129

for S being non void Signature

for X being non empty ManySortedSet of the carrier of S

for f being UnOp of (Union the Sorts of (Free (S,X))) holds

( f is term-transformation of S,X iff for s being SortSymbol of S

for a being set st a in the Sorts of (Free (S,X)) . s holds

f . a in the Sorts of (Free (S,X)) . s )

for X being non empty ManySortedSet of the carrier of S

for f being UnOp of (Union the Sorts of (Free (S,X))) holds

( f is term-transformation of S,X iff for s being SortSymbol of S

for a being set st a in the Sorts of (Free (S,X)) . s holds

f . a in the Sorts of (Free (S,X)) . s )

proof end;

theorem Th130: :: ABCMIZ_1:130

for S being non void Signature

for X being non empty ManySortedSet of the carrier of S

for f being term-transformation of S,X

for s being SortSymbol of S

for p being FinSequence of the Sorts of (Free (S,X)) . s holds

( f * p is FinSequence of the Sorts of (Free (S,X)) . s & card (f * p) = len p )

for X being non empty ManySortedSet of the carrier of S

for f being term-transformation of S,X

for s being SortSymbol of S

for p being FinSequence of the Sorts of (Free (S,X)) . s holds

( f * p is FinSequence of the Sorts of (Free (S,X)) . s & card (f * p) = len p )

proof end;

definition

let S be non void Signature;

let X be ManySortedSet of the carrier of S;

let t be term-transformation of S,X;

end;
let X be ManySortedSet of the carrier of S;

let t be term-transformation of S,X;

:: deftheorem defines substitution ABCMIZ_1:def 57 :

for S being non void Signature

for X being ManySortedSet of the carrier of S

for t being term-transformation of S,X holds

( t is substitution iff for o being OperSymbol of S

for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds

t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q );

for S being non void Signature

for X being ManySortedSet of the carrier of S

for t being term-transformation of S,X holds

( t is substitution iff for o being OperSymbol of S

for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds

t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q );

scheme :: ABCMIZ_1:sch 3

StructDef{ F_{1}() -> initialized ConstructorSignature, F_{2}( set ) -> expression of F_{1}(), F_{3}( set ) -> expression of F_{1}(), F_{4}( set , set ) -> expression of F_{1}(), F_{5}( set , set ) -> expression of F_{1}() } :

StructDef{ F

ex f being term-transformation of F_{1}(), MSVars F_{1}() st

( ( for x being variable holds f . (x -term F_{1}()) = F_{2}(x) ) & ( for c being constructor OperSymbol of F_{1}()

for p, q being FinSequence of QuasiTerms F_{1}() st len p = len (the_arity_of c) & q = f * p holds

f . (c -trm p) = F_{4}(c,q) ) & ( for a being expression of F_{1}(), an_Adj F_{1}() holds f . ((non_op F_{1}()) term a) = F_{3}((f . a)) ) & ( for a being expression of F_{1}(), an_Adj F_{1}()

for t being expression of F_{1}(), a_Type F_{1}() holds f . ((ast F_{1}()) term (a,t)) = F_{5}((f . a),(f . t)) ) )

provided( ( for x being variable holds f . (x -term F

for p, q being FinSequence of QuasiTerms F

f . (c -trm p) = F

for t being expression of F

A1:
for x being variable holds F_{2}(x) is quasi-term of F_{1}()
and

A2: for c being constructor OperSymbol of F_{1}()

for p being FinSequence of QuasiTerms F_{1}() st len p = len (the_arity_of c) holds

F_{4}(c,p) is expression of F_{1}(), the_result_sort_of c
and

A3: for a being expression of F_{1}(), an_Adj F_{1}() holds F_{3}(a) is expression of F_{1}(), an_Adj F_{1}()
and

A4: for a being expression of F_{1}(), an_Adj F_{1}()

for t being expression of F_{1}(), a_Type F_{1}() holds F_{5}(a,t) is expression of F_{1}(), a_Type F_{1}()

A2: for c being constructor OperSymbol of F

for p being FinSequence of QuasiTerms F

F

A3: for a being expression of F

A4: for a being expression of F

for t being expression of F

proof end;

begin

definition

let A be set ;

let x, y be set ;

let a, b be Element of A;

:: original: IFIN

redefine func IFIN (x,y,a,b) -> Element of A;

coherence

IFIN (x,y,a,b) is Element of A by MATRIX_7:def 1;

end;
let x, y be set ;

let a, b be Element of A;

:: original: IFIN

redefine func IFIN (x,y,a,b) -> Element of A;

coherence

IFIN (x,y,a,b) is Element of A by MATRIX_7:def 1;

definition
end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

end;
let f be valuation of C;

attr f is irrelevant means :Def58: :: ABCMIZ_1:def 58

for x being variable st x in dom f holds

ex y being variable st f . x = y -term C;

for x being variable st x in dom f holds

ex y being variable st f . x = y -term C;

:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :

for C being initialized ConstructorSignature

for f being valuation of C holds

( f is irrelevant iff for x being variable st x in dom f holds

ex y being variable st f . x = y -term C );

for C being initialized ConstructorSignature

for f being valuation of C holds

( f is irrelevant iff for x being variable st x in dom f holds

ex y being variable st f . x = y -term C );

notation

let C be initialized ConstructorSignature;

let f be valuation of C;

antonym relevant f for irrelevant ;

end;
let f be valuation of C;

antonym relevant f for irrelevant ;

registration

let C be initialized ConstructorSignature;

coherence

for b_{1} being valuation of C st b_{1} is empty holds

b_{1} is irrelevant

end;
coherence

for b

b

proof end;

registration

let C be initialized ConstructorSignature;

ex b_{1} being valuation of C st b_{1} is empty

end;
cluster empty Relation-like Vars -defined QuasiTerms C -valued Function-like Function-yielding V115() for Element of bool [:Vars,(QuasiTerms C):];

existence ex b

proof end;

definition

let C be initialized ConstructorSignature;

let X be Subset of Vars;

{ [x,(x -term C)] where x is variable : x in X } is valuation of C

end;
let X be Subset of Vars;

func C idval X -> valuation of C equals :: ABCMIZ_1:def 59

{ [x,(x -term C)] where x is variable : x in X } ;

coherence { [x,(x -term C)] where x is variable : x in X } ;

{ [x,(x -term C)] where x is variable : x in X } is valuation of C

proof end;

:: deftheorem defines idval ABCMIZ_1:def 59 :

for C being initialized ConstructorSignature

for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ;

for C being initialized ConstructorSignature

for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ;

theorem Th131: :: ABCMIZ_1:131

for C being initialized ConstructorSignature

for X being Subset of Vars holds

( dom (C idval X) = X & ( for x being variable st x in X holds

(C idval X) . x = x -term C ) )

for X being Subset of Vars holds

( dom (C idval X) = X & ( for x being variable st x in X holds

(C idval X) . x = x -term C ) )

proof end;

registration

let C be initialized ConstructorSignature;

let X be Subset of Vars;

coherence

( C idval X is irrelevant & C idval X is one-to-one )

end;
let X be Subset of Vars;

coherence

( C idval X is irrelevant & C idval X is one-to-one )

proof end;

registration

let C be initialized ConstructorSignature;

let X be empty Subset of Vars;

coherence

C idval X is empty

end;
let X be empty Subset of Vars;

coherence

C idval X is empty

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

ex b_{1} being term-transformation of C, MSVars C st

( ( for x being variable holds

( ( x in dom f implies b_{1} . (x -term C) = f . x ) & ( not x in dom f implies b_{1} . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b_{1} * p holds

b_{1} . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b_{1} . ((non_op C) term a) = (non_op C) term (b_{1} . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds b_{1} . ((ast C) term (a,t)) = (ast C) term ((b_{1} . a),(b_{1} . t)) ) )

uniqueness

for b_{1}, b_{2} being term-transformation of C, MSVars C st ( for x being variable holds

( ( x in dom f implies b_{1} . (x -term C) = f . x ) & ( not x in dom f implies b_{1} . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b_{1} * p holds

b_{1} . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b_{1} . ((non_op C) term a) = (non_op C) term (b_{1} . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds b_{1} . ((ast C) term (a,t)) = (ast C) term ((b_{1} . a),(b_{1} . t)) ) & ( for x being variable holds

( ( x in dom f implies b_{2} . (x -term C) = f . x ) & ( not x in dom f implies b_{2} . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b_{2} * p holds

b_{2} . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b_{2} . ((non_op C) term a) = (non_op C) term (b_{2} . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds b_{2} . ((ast C) term (a,t)) = (ast C) term ((b_{2} . a),(b_{2} . t)) ) holds

b_{1} = b_{2};

end;
let f be valuation of C;

func f # -> term-transformation of C, MSVars C means :Def60: :: ABCMIZ_1:def 60

( ( for x being variable holds

( ( x in dom f implies it . (x -term C) = f . x ) & ( not x in dom f implies it . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = it * p holds

it . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds it . ((ast C) term (a,t)) = (ast C) term ((it . a),(it . t)) ) );

existence ( ( for x being variable holds

( ( x in dom f implies it . (x -term C) = f . x ) & ( not x in dom f implies it . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = it * p holds

it . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds it . ((ast C) term (a,t)) = (ast C) term ((it . a),(it . t)) ) );

ex b

( ( for x being variable holds

( ( x in dom f implies b

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b

b

for t being expression of C, a_Type C holds b

proof end;

correctness uniqueness

for b

( ( x in dom f implies b

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b

b

for t being expression of C, a_Type C holds b

( ( x in dom f implies b

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b

b

for t being expression of C, a_Type C holds b

b

proof end;

:: deftheorem Def60 defines # ABCMIZ_1:def 60 :

for C being initialized ConstructorSignature

for f being valuation of C

for b_{3} being term-transformation of C, MSVars C holds

( b_{3} = f # iff ( ( for x being variable holds

( ( x in dom f implies b_{3} . (x -term C) = f . x ) & ( not x in dom f implies b_{3} . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b_{3} * p holds

b_{3} . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b_{3} . ((non_op C) term a) = (non_op C) term (b_{3} . a) ) & ( for a being expression of C, an_Adj C

for t being expression of C, a_Type C holds b_{3} . ((ast C) term (a,t)) = (ast C) term ((b_{3} . a),(b_{3} . t)) ) ) );

for C being initialized ConstructorSignature

for f being valuation of C

for b

( b

( ( x in dom f implies b

for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b

b

for t being expression of C, a_Type C holds b

registration

let C be initialized ConstructorSignature;

let f be valuation of C;

coherence

f # is substitution

end;
let f be valuation of C;

coherence

f # is substitution

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let e be expression of C;

coherence

(f #) . e is expression of C ;

end;
let f be valuation of C;

let e be expression of C;

coherence

(f #) . e is expression of C ;

:: deftheorem defines at ABCMIZ_1:def 61 :

for C being initialized ConstructorSignature

for f being valuation of C

for e being expression of C holds e at f = (f #) . e;

for C being initialized ConstructorSignature

for f being valuation of C

for e being expression of C holds e at f = (f #) . e;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let p be FinSequence;

assume B1: rng p c= Union the Sorts of (Free (C,(MSVars C))) ;

coherence

(f #) * p is FinSequence

end;
let f be valuation of C;

let p be FinSequence;

assume B1: rng p c= Union the Sorts of (Free (C,(MSVars C))) ;

coherence

(f #) * p is FinSequence

proof end;

:: deftheorem Def62 defines at ABCMIZ_1:def 62 :

for C being initialized ConstructorSignature

for f being valuation of C

for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds

p at f = (f #) * p;

for C being initialized ConstructorSignature

for f being valuation of C

for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds

p at f = (f #) * p;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let p be FinSequence of QuasiTerms C;

p at f is FinSequence of QuasiTerms C

for b_{1} being FinSequence of QuasiTerms C holds

( b_{1} = p at f iff b_{1} = (f #) * p )

end;
let f be valuation of C;

let p be FinSequence of QuasiTerms C;

:: original: at

redefine func p at f -> FinSequence of QuasiTerms C equals :: ABCMIZ_1:def 63

(f #) * p;

coherence redefine func p at f -> FinSequence of QuasiTerms C equals :: ABCMIZ_1:def 63

(f #) * p;

p at f is FinSequence of QuasiTerms C

proof end;

compatibility for b

( b

proof end;

:: deftheorem defines at ABCMIZ_1:def 63 :

for C being initialized ConstructorSignature

for f being valuation of C

for p being FinSequence of QuasiTerms C holds p at f = (f #) * p;

for C being initialized ConstructorSignature

for f being valuation of C

for p being FinSequence of QuasiTerms C holds p at f = (f #) * p;

theorem :: ABCMIZ_1:132

theorem :: ABCMIZ_1:133

theorem :: ABCMIZ_1:134

for C being initialized ConstructorSignature

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C

for f being valuation of C st len p = len (the_arity_of c) holds

(c -trm p) at f = c -trm (p at f) by Def60;

for c being constructor OperSymbol of C

for p being FinSequence of QuasiTerms C

for f being valuation of C st len p = len (the_arity_of c) holds

(c -trm p) at f = c -trm (p at f) by Def60;

theorem :: ABCMIZ_1:135

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C

for f being valuation of C holds ((non_op C) term a) at f = (non_op C) term (a at f) by Def60;

for a being expression of C, an_Adj C

for f being valuation of C holds ((non_op C) term a) at f = (non_op C) term (a at f) by Def60;

theorem :: ABCMIZ_1:136

for C being initialized ConstructorSignature

for t being expression of C, a_Type C

for a being expression of C, an_Adj C

for f being valuation of C holds ((ast C) term (a,t)) at f = (ast C) term ((a at f),(t at f)) by Def60;

for t being expression of C, a_Type C

for a being expression of C, an_Adj C

for f being valuation of C holds ((ast C) term (a,t)) at f = (ast C) term ((a at f),(t at f)) by Def60;

theorem Th137: :: ABCMIZ_1:137

for C being initialized ConstructorSignature

for e being expression of C

for X being Subset of Vars holds e at (C idval X) = e

for e being expression of C

for X being Subset of Vars holds e at (C idval X) = e

proof end;

theorem :: ABCMIZ_1:138

for C being initialized ConstructorSignature

for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))

for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))

proof end;

theorem Th139: :: ABCMIZ_1:139

for C being initialized ConstructorSignature

for e being expression of C

for f being empty valuation of C holds e at f = e

for e being expression of C

for f being empty valuation of C holds e at f = e

proof end;

theorem :: ABCMIZ_1:140

for C being initialized ConstructorSignature

for f being empty valuation of C holds f # = id (Union the Sorts of (Free (C,(MSVars C))))

for f being empty valuation of C holds f # = id (Union the Sorts of (Free (C,(MSVars C))))

proof end;

:: theorem

:: for t being expression of C

:: for f1,f2 being valuation of C

:: holds (t at f1) at f2 = ((f2# )*(f1# )).t by FUNCT_2:21;

:: for t being expression of C

:: for f1,f2 being valuation of C

:: holds (t at f1) at f2 = ((f2# )*(f1# )).t by FUNCT_2:21;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let t be quasi-term of C;

:: original: at

redefine func t at f -> quasi-term of C;

coherence

t at f is quasi-term of C

end;
let f be valuation of C;

let t be quasi-term of C;

:: original: at

redefine func t at f -> quasi-term of C;

coherence

t at f is quasi-term of C

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let a be expression of C, an_Adj C;

:: original: at

redefine func a at f -> expression of C, an_Adj C;

coherence

a at f is expression of C, an_Adj C

end;
let f be valuation of C;

let a be expression of C, an_Adj C;

:: original: at

redefine func a at f -> expression of C, an_Adj C;

coherence

a at f is expression of C, an_Adj C

proof end;

registration

let C be initialized ConstructorSignature;

let f be valuation of C;

let a be positive expression of C, an_Adj C;

coherence

for b_{1} being expression of C, an_Adj C st b_{1} = a at f holds

b_{1} is positive

end;
let f be valuation of C;

let a be positive expression of C, an_Adj C;

coherence

for b

b

proof end;

registration

let C be initialized ConstructorSignature;

let f be valuation of C;

let a be negative expression of C, an_Adj C;

coherence

for b_{1} being expression of C, an_Adj C st b_{1} = a at f holds

b_{1} is negative

end;
let f be valuation of C;

let a be negative expression of C, an_Adj C;

coherence

for b

b

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let a be quasi-adjective of C;

:: original: at

redefine func a at f -> quasi-adjective of C;

coherence

a at f is quasi-adjective of C

end;
let f be valuation of C;

let a be quasi-adjective of C;

:: original: at

redefine func a at f -> quasi-adjective of C;

coherence

a at f is quasi-adjective of C

proof end;

theorem :: ABCMIZ_1:141

for C being initialized ConstructorSignature

for a being expression of C, an_Adj C

for f being valuation of C holds (Non a) at f = Non (a at f)

for a being expression of C, an_Adj C

for f being valuation of C holds (Non a) at f = Non (a at f)

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let t be expression of C, a_Type C;

:: original: at

redefine func t at f -> expression of C, a_Type C;

coherence

t at f is expression of C, a_Type C

end;
let f be valuation of C;

let t be expression of C, a_Type C;

:: original: at

redefine func t at f -> expression of C, a_Type C;

coherence

t at f is expression of C, a_Type C

proof end;

registration

let C be initialized ConstructorSignature;

let f be valuation of C;

let t be pure expression of C, a_Type C;

coherence

for b_{1} being expression of C, a_Type C st b_{1} = t at f holds

b_{1} is pure

end;
let f be valuation of C;

let t be pure expression of C, a_Type C;

coherence

for b

b

proof end;

theorem :: ABCMIZ_1:142

for C being initialized ConstructorSignature

for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st

for x, y being variable holds

( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )

for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st

for x, y being variable holds

( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )

proof end;

theorem :: ABCMIZ_1:143

for C being initialized ConstructorSignature

for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds

( y in dom g & g . y = x -term C ) ) holds

for e being expression of C st variables_in e c= dom f holds

(e at f) at g = e

for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds

( y in dom g & g . y = x -term C ) ) holds

for e being expression of C st variables_in e c= dom f holds

(e at f) at g = e

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let A be Subset of (QuasiAdjs C);

{ (a at f) where a is quasi-adjective of C : a in A } is Subset of (QuasiAdjs C)

end;
let f be valuation of C;

let A be Subset of (QuasiAdjs C);

func A at f -> Subset of (QuasiAdjs C) equals :: ABCMIZ_1:def 64

{ (a at f) where a is quasi-adjective of C : a in A } ;

coherence { (a at f) where a is quasi-adjective of C : a in A } ;

{ (a at f) where a is quasi-adjective of C : a in A } is Subset of (QuasiAdjs C)

proof end;

:: deftheorem defines at ABCMIZ_1:def 64 :

for C being initialized ConstructorSignature

for f being valuation of C

for A being Subset of (QuasiAdjs C) holds A at f = { (a at f) where a is quasi-adjective of C : a in A } ;

for C being initialized ConstructorSignature

for f being valuation of C

for A being Subset of (QuasiAdjs C) holds A at f = { (a at f) where a is quasi-adjective of C : a in A } ;

theorem Th144: :: ABCMIZ_1:144

for C being initialized ConstructorSignature

for f being valuation of C

for A being Subset of (QuasiAdjs C)

for a being quasi-adjective of C st A = {a} holds

A at f = {(a at f)}

for f being valuation of C

for A being Subset of (QuasiAdjs C)

for a being quasi-adjective of C st A = {a} holds

A at f = {(a at f)}

proof end;

theorem Th145: :: ABCMIZ_1:145

for C being initialized ConstructorSignature

for f being valuation of C

for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f)

for f being valuation of C

for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f)

proof end;

theorem :: ABCMIZ_1:146

for C being initialized ConstructorSignature

for f being valuation of C

for A, B being Subset of (QuasiAdjs C) st A c= B holds

A at f c= B at f

for f being valuation of C

for A, B being Subset of (QuasiAdjs C) st A c= B holds

A at f c= B at f

proof end;

registration

let C be initialized ConstructorSignature;

let f be valuation of C;

let A be finite Subset of (QuasiAdjs C);

coherence

A at f is finite

end;
let f be valuation of C;

let A be finite Subset of (QuasiAdjs C);

coherence

A at f is finite

proof end;

definition

let C be initialized ConstructorSignature;

let f be valuation of C;

let T be quasi-type of C;

coherence

((adjs T) at f) ast ((the_base_of T) at f) is quasi-type of C ;

end;
let f be valuation of C;

let T be quasi-type of C;

coherence

((adjs T) at f) ast ((the_base_of T) at f) is quasi-type of C ;

:: deftheorem defines at ABCMIZ_1:def 65 :

for C being initialized ConstructorSignature

for f being valuation of C

for T being quasi-type of C holds T at f = ((adjs T) at f) ast ((the_base_of T) at f);

for C being initialized ConstructorSignature

for f being valuation of C

for T being quasi-type of C holds T at f = ((adjs T) at f) ast ((the_base_of T) at f);

theorem :: ABCMIZ_1:147

for C being initialized ConstructorSignature

for f being valuation of C

for T being quasi-type of C holds

( adjs (T at f) = (adjs T) at f & the_base_of (T at f) = (the_base_of T) at f ) by MCART_1:7;

for f being valuation of C

for T being quasi-type of C holds

( adjs (T at f) = (adjs T) at f & the_base_of (T at f) = (the_base_of T) at f ) by MCART_1:7;

theorem :: ABCMIZ_1:148

for C being initialized ConstructorSignature

for f being valuation of C

for T being quasi-type of C

for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)

for f being valuation of C

for T being quasi-type of C

for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)

proof end;

definition

let C be initialized ConstructorSignature;

let f, g be valuation of C;

ex b_{1} being valuation of C st

( dom b_{1} = (dom f) \/ (dom g) & ( for x being variable st x in dom b_{1} holds

b_{1} . x = ((x -term C) at f) at g ) )

for b_{1}, b_{2} being valuation of C st dom b_{1} = (dom f) \/ (dom g) & ( for x being variable st x in dom b_{1} holds

b_{1} . x = ((x -term C) at f) at g ) & dom b_{2} = (dom f) \/ (dom g) & ( for x being variable st x in dom b_{2} holds

b_{2} . x = ((x -term C) at f) at g ) holds

b_{1} = b_{2}

end;
let f, g be valuation of C;

func f at g -> valuation of C means :Def66: :: ABCMIZ_1:def 66

( dom it = (dom f) \/ (dom g) & ( for x being variable st x in dom it holds

it . x = ((x -term C) at f) at g ) );

existence ( dom it = (dom f) \/ (dom g) & ( for x being variable st x in dom it holds

it . x = ((x -term C) at f) at g ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def66 defines at ABCMIZ_1:def 66 :

for C being initialized ConstructorSignature

for f, g, b_{4} being valuation of C holds

( b_{4} = f at g iff ( dom b_{4} = (dom f) \/ (dom g) & ( for x being variable st x in dom b_{4} holds

b_{4} . x = ((x -term C) at f) at g ) ) );

for C being initialized ConstructorSignature

for f, g, b

( b

b

registration

let C be initialized ConstructorSignature;

let f, g be irrelevant valuation of C;

coherence

f at g is irrelevant

end;
let f, g be irrelevant valuation of C;

coherence

f at g is irrelevant

proof end;

theorem Th149: :: ABCMIZ_1:149

for C being initialized ConstructorSignature

for e being expression of C

for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)

for e being expression of C

for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)

proof end;

theorem Th150: :: ABCMIZ_1:150

for C being initialized ConstructorSignature

for A being Subset of (QuasiAdjs C)

for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2)

for A being Subset of (QuasiAdjs C)

for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2)

proof end;

theorem :: ABCMIZ_1:151

for C being initialized ConstructorSignature

for T being quasi-type of C

for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)

for T being quasi-type of C

for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)

proof end;

:: for C being ConstructorSignature holds the carrier of C = 3

:: by CONSTRSIGN,YELLOW11:1;