:: Towards the construction of a model of Mizar concepts
:: by Grzegorz Bancerek
::
:: Copyright (c) 2008-2021 Association of Mizar Users

theorem Th1: :: ABCMIZ_1:1
for x being set
for f being Function holds f . x c= Union f
proof end;

theorem :: ABCMIZ_1:2
for x being set
for f being Function st Union f = {} holds
f . x = {} by ;

theorem Th3: :: ABCMIZ_1:3
for f being Function
for x, y being object st f = [x,y] holds
x = y
proof end;

theorem Th4: :: ABCMIZ_1:4
for X, Y being set holds (id X) .: Y c= Y
proof end;

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
proof end;

registration
let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;
cluster -> non pair for Element of Union the Sorts of (Free (S,X));
coherence
for b1 being Element of (Free (S,X)) holds not b1 is pair
proof end;
end;

theorem Th6: :: ABCMIZ_1:6
for x, y, z being set st x in {z} * & y in {z} * & card x = card y holds
x = y
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;

registration
let S be non void Signature;
let X be V9() ManySortedSet of S;
cluster -> DTree-yielding for FinSequence of Union the Sorts of (Free (S,X));
coherence
for b1 being FinSequence of (Free (S,X)) holds b1 is DTree-yielding
proof end;
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 () & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> ))) ) )
proof end;

definition
let A be set ;
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
for b1, b2 being set st A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) & A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) holds
b1 = b2
proof end;
existence
ex b1 being set st
( A c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
proof end;
projectivity
for b1, b2 being set st b2 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b2 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) holds
( b1 c= b1 & ( for x, y being set st [x,y] in b1 holds
x c= b1 ) & ( for B being set st b1 c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b1 c= B ) )
;
end;

:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :
for A, b2 being set holds
( b2 = varcl A iff ( A c= b2 & ( for x, y being set st [x,y] in b2 holds
x c= b2 ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b2 c= B ) ) );

theorem Th8: :: ABCMIZ_1:8
proof end;

theorem Th9: :: ABCMIZ_1:9
for A, B being set st A c= B holds
varcl A c= varcl B
proof end;

theorem Th10: :: ABCMIZ_1:10
for A being set holds varcl () = union { () where a is Element of A : verum }
proof end;

scheme :: ABCMIZ_1:sch 1
Sch14{ F1() -> set , F2( set ) -> set , P1[ set ] } :
varcl (union { F2(z) where z is Element of F1() : P1[z] } ) = union { (varcl F2(z)) where z is Element of F1() : P1[z] }
proof end;

theorem Th11: :: ABCMIZ_1:11
for X, Y being set holds varcl (X \/ Y) = () \/ ()
proof end;

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
proof end;

theorem Th13: :: ABCMIZ_1:13
for X, Y being set holds varcl (() /\ ()) = () /\ ()
proof end;

registration
let A be empty set ;
coherence
varcl A is empty
by Th8;
end;

deffunc H1( set , set ) -> set = { [(),j] where A is Subset of \$2, j is Element of NAT : A is finite } ;

definition
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) = { [(),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) );
existence
ex b1 being set ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )
proof end;
uniqueness
for b1, b2 being set st ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st
( b2 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :
for b1 being set holds
( b1 = Vars iff ex V being ManySortedSet of NAT st
( b1 = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) );

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) = { [(),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
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) = { [(),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
proof end;

theorem Th16: :: ABCMIZ_1:16
{ [{},i] where i is Element of NAT : verum } c= Vars
proof end;

theorem Th17: :: ABCMIZ_1:17
for A being finite Subset of Vars
for i being Nat holds [(),i] in Vars
proof end;

theorem Th18: :: ABCMIZ_1:18
Vars = { [(),j] where A is Subset of Vars, j is Element of NAT : A is finite }
proof end;

theorem Th19: :: ABCMIZ_1:19
proof end;

theorem Th20: :: ABCMIZ_1:20
for X being set st the_rank_of X is finite holds
X is finite
proof end;

theorem Th21: :: ABCMIZ_1:21
for X being set holds the_rank_of () = the_rank_of X
proof end;

theorem Th22: :: ABCMIZ_1:22
for X being finite Subset of () holds X in Rank omega
proof end;

theorem Th23: :: ABCMIZ_1:23
proof end;

theorem Th24: :: ABCMIZ_1:24
for A being finite Subset of Vars holds varcl A is finite Subset of Vars
proof end;

registration
cluster Vars -> non empty ;
correctness
coherence
not Vars is empty
;
proof end;
end;

definition end;

registration
let x be variable;
cluster vars x -> finite for set ;
coherence
for b1 being set st b1 = x 1 holds
b1 is finite
proof end;
end;

notation
let x be variable;
synonym vars x for x 1 ;
end;

definition
let x be variable;
:: original: vars
redefine func vars x -> Subset of Vars;
coherence
vars x is Subset of Vars
proof end;
end;

theorem :: ABCMIZ_1:25
for i being Nat holds [{},i] in Vars
proof end;

theorem Th26: :: ABCMIZ_1:26
for j being Element of NAT
for A being Subset of Vars holds varcl {[(),j]} = () \/ {[(),j]}
proof end;

theorem Th27: :: ABCMIZ_1:27
for x being variable holds varcl {x} = (vars x) \/ {x}
proof end;

theorem :: ABCMIZ_1:28
for i being Nat
for x being variable holds [((vars x) \/ {x}),i] in Vars
proof end;

notation
let R be Relation;
let A be set ;
synonym R dom A for R | A;
end;

definition
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
ex b1 being FinSequenceSet of Vars st
for p being FinSequence of Vars holds
( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) 1 c= rng (p dom i) ) ) )
proof end;
correctness
uniqueness
for b1, b2 being FinSequenceSet of Vars st ( for p being FinSequence of Vars holds
( p in b1 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 b2 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
b1 = b2
;
proof end;
end;

:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :
for b1 being FinSequenceSet of Vars holds
( b1 = QuasiLoci iff for p being FinSequence of Vars holds
( p in b1 iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) 1 c= rng (p dom i) ) ) ) );

theorem Th29: :: ABCMIZ_1:29
proof end;

registration
cluster QuasiLoci -> non empty ;
correctness
coherence
not QuasiLoci is empty
;
by Th29;
end;

definition end;

registration
coherence
for b1 being quasi-loci holds b1 is one-to-one
by Def3;
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 ) )
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 ) )
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 )
proof end;

theorem :: ABCMIZ_1:33
for l being quasi-loci holds varcl (rng l) = rng l
proof end;

theorem Th34: :: ABCMIZ_1:34
for x being variable holds
( <*x*> is quasi-loci iff vars x = {} )
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} ) )
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} ) )
proof end;

definition
let l be quasi-loci;
:: original: "
redefine func l " -> PartFunc of Vars,NAT;
coherence
l " is PartFunc of Vars,NAT
proof end;
end;

definition
func a_Type -> set equals :: ABCMIZ_1:def 4
0 ;
coherence
0 is set
;
func an_Adj -> set equals :: ABCMIZ_1:def 5
1;
coherence
1 is set
;
func a_Term -> set equals :: ABCMIZ_1:def 6
2;
coherence
2 is set
;
func * -> set equals :: ABCMIZ_1:def 7
0 ;
coherence
0 is set
;
func non_op -> set equals :: ABCMIZ_1:def 8
1;
coherence
1 is set
;
end;

:: deftheorem defines a_Type ABCMIZ_1:def 4 :

:: deftheorem defines an_Adj ABCMIZ_1:def 5 :

:: deftheorem defines a_Term ABCMIZ_1:def 6 :
a_Term = 2;

:: deftheorem defines * ABCMIZ_1:def 7 :
* = 0 ;

:: deftheorem defines non_op ABCMIZ_1:def 8 :
non_op = 1;

definition
let C be Signature;
attr C is constructor means :Def9: :: ABCMIZ_1:def 9
( the carrier of C = & c= the carrier' of C & the Arity of C . * = & the Arity of C . non_op = & 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 * ) );
end;

:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
for C being Signature holds
( C is constructor iff ( the carrier of C = & c= the carrier' of C & the Arity of C . * = & the Arity of C . non_op = & 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 * ) ) );

registration
cluster V265() constructor -> non empty non void for ManySortedSign ;
coherence
for b1 being Signature st b1 is constructor holds
( not b1 is empty & not b1 is void )
;
end;

definition
func MinConstrSign -> strict Signature means :Def10: :: ABCMIZ_1:def 10
( it is constructor & the carrier' of it = );
existence
ex b1 being strict Signature st
( b1 is constructor & the carrier' of b1 = )
proof end;
correctness
uniqueness
for b1, b2 being strict Signature st b1 is constructor & the carrier' of b1 = & b2 is constructor & the carrier' of b2 = holds
b1 = b2
;
proof end;
end;

:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :
for b1 being strict Signature holds
( b1 = MinConstrSign iff ( b1 is constructor & the carrier' of b1 = ) );

registration
coherence by Def10;
end;

registration
existence
ex b1 being Signature st
( b1 is constructor & b1 is strict )
proof end;
end;

definition end;

:: theorem ::?
:: for C being ConstructorSignature holds the carrier of C = 3
:: by CONSTRSIGN,YELLOW11:1;
definition
let C be ConstructorSignature;
let o be OperSymbol of C;
attr o is constructor means :Def11: :: ABCMIZ_1:def 11
( o <> * & o <> non_op );
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 ) );

theorem :: ABCMIZ_1:37
for S being ConstructorSignature
for o being OperSymbol of S st o is constructor holds
the_arity_of o = (len ()) |-> a_Term
proof end;

definition
let C be non empty non void Signature;
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 = {} );
end;

:: 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 = {} ) );

definition
let C be ConstructorSignature;
A1: the carrier of C = by Def9;
func a_Type C -> SortSymbol of C equals :: ABCMIZ_1:def 13
a_Type ;
coherence
a_Type is SortSymbol of C
by ;
func an_Adj C -> SortSymbol of C equals :: ABCMIZ_1:def 14
coherence
by ;
func a_Term C -> SortSymbol of C equals :: ABCMIZ_1:def 15
a_Term ;
coherence
a_Term is SortSymbol of C
by ;
A2: c= the carrier' of C by Def9;
A3: * in by TARSKI:def 2;
A4: non_op in by TARSKI:def 2;
func non_op C -> OperSymbol of C equals :: ABCMIZ_1:def 16
non_op ;
coherence
non_op is OperSymbol of C
by A2, A4;
func ast C -> OperSymbol of C equals :: ABCMIZ_1:def 17
* ;
coherence
* is OperSymbol of C
by A2, A3;
end;

:: deftheorem defines a_Type ABCMIZ_1:def 13 :
for C being ConstructorSignature holds a_Type C = a_Type ;

:: deftheorem defines an_Adj ABCMIZ_1:def 14 :

:: deftheorem defines a_Term ABCMIZ_1:def 15 :
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 ;

:: deftheorem defines ast ABCMIZ_1:def 17 :
for C being ConstructorSignature holds ast C = * ;

theorem :: ABCMIZ_1:38
for C being ConstructorSignature holds
( the_arity_of () = <*()*> & the_result_sort_of () = an_Adj C & the_arity_of (ast C) = <*(),()*> & the_result_sort_of (ast C) = a_Type C ) by Def9;

definition
correctness
coherence ;
;
correctness
coherence ;
;
correctness
coherence ;
;
end;

:: deftheorem defines Modes ABCMIZ_1:def 18 :

:: deftheorem defines Attrs ABCMIZ_1:def 19 :

:: deftheorem defines Funcs ABCMIZ_1:def 20 :

registration
cluster Modes -> non empty ;
coherence
not Modes is empty
;
cluster Attrs -> non empty ;
coherence
not Attrs is empty
;
cluster Funcs -> non empty ;
coherence
not Funcs is empty
;
end;

definition
func Constructors -> non empty set equals :: ABCMIZ_1:def 21
() \/ Funcs;
coherence
() \/ Funcs is non empty set
;
end;

:: deftheorem defines Constructors ABCMIZ_1:def 21 :

theorem :: ABCMIZ_1:39
proof end;

definition
let x be Element of ;
:: original: vars
redefine func x 1 -> quasi-loci;
coherence by MCART_1:10;
:: original: the_base_of
redefine func x 2 -> Element of NAT ;
coherence by MCART_1:10;
end;

notation
let c be Element of Constructors ;
synonym kind_of c for c 1 ;
end;

definition
let c be Element of Constructors ;
:: original: vars
redefine func kind_of c -> Element of ;
coherence
proof end;
:: original: the_base_of
redefine func c 2 -> Element of ;
coherence
proof end;
end;

definition
let c be Element of Constructors ;
func loci_of c -> quasi-loci equals :: ABCMIZ_1:def 22
(c 2) 1 ;
coherence
(c 2) 1 is quasi-loci
;
func index_of c -> Nat equals :: ABCMIZ_1:def 23
(c 2) 2 ;
coherence
(c 2) 2 is Nat
;
end;

:: deftheorem defines loci_of ABCMIZ_1:def 22 :
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 ;

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 ) )
proof end;

definition
func MaxConstrSign -> strict ConstructorSignature means :Def24: :: ABCMIZ_1:def 24
( the carrier' of it = \/ 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
ex b1 being strict ConstructorSignature st
( the carrier' of b1 = \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds
( the ResultSort of b1 . o = o 1 & card ( the Arity of b1 . o) = card ((o 2) 1) ) ) )
proof end;
uniqueness
for b1, b2 being strict ConstructorSignature st the carrier' of b1 = \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds
( the ResultSort of b1 . o = o 1 & card ( the Arity of b1 . o) = card ((o 2) 1) ) ) & the carrier' of b2 = \/ Constructors & ( for o being OperSymbol of b2 st o is constructor holds
( the ResultSort of b2 . o = o 1 & card ( the Arity of b2 . o) = card ((o 2) 1) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
for b1 being strict ConstructorSignature holds
( b1 = MaxConstrSign iff ( the carrier' of b1 = \/ Constructors & ( for o being OperSymbol of b1 st o is constructor holds
( the ResultSort of b1 . o = o 1 & card ( the Arity of b1 . o) = card ((o 2) 1) ) ) ) );

registration
correctness
coherence ;
proof end;
correctness
proof end;
end;

registration
correctness
existence
ex b1 being ConstructorSignature st
( b1 is initialized & b1 is strict )
;
proof end;
end;

registration
let C be initialized ConstructorSignature;
cluster constructor for Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st b1 is constructor
proof end;
end;

definition
let C be ConstructorSignature;
A1: the carrier of C = 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
for b1, b2 being ManySortedSet of the carrier of C st b1 . a_Type = {} & b1 . an_Adj = {} & b1 . a_Term = Vars & b2 . a_Type = {} & b2 . an_Adj = {} & b2 . a_Term = Vars holds
b1 = b2
proof end;
existence
ex b1 being ManySortedSet of the carrier of C st
( b1 . a_Type = {} & b1 . an_Adj = {} & b1 . a_Term = Vars )
proof end;
end;

:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :
for C being ConstructorSignature
for b2 being ManySortedSet of the carrier of C holds
( b2 = MSVars C iff ( b2 . a_Type = {} & b2 . an_Adj = {} & b2 . a_Term = Vars ) );

:: 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;
registration
let C be ConstructorSignature;
cluster MSVars C -> V9() ;
coherence
not MSVars C is empty-yielding
proof end;
end;

registration
let C be initialized ConstructorSignature;
cluster Free (C,()) -> non-empty ;
correctness
coherence
Free (C,()) is non-empty
;
proof end;
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));
attr t is ground means :: ABCMIZ_1:def 26
Union () = {} ;
attr t is compound means :Def27: :: ABCMIZ_1:def 27
t . {} in [: the carrier' of S,{ the carrier of S}:];
end;

:: 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 () = {} );

:: 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}:] );

definition
let C be initialized ConstructorSignature;
mode expression of C is Element of (Free (C,()));
end;

definition
let C be initialized ConstructorSignature;
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,())) . s;
existence
ex b1 being expression of C st b1 in the Sorts of (Free (C,())) . s
proof end;
end;

:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :
for C being initialized ConstructorSignature
for s being SortSymbol of C
for b3 being expression of C holds
( b3 is expression of C,s iff b3 in the Sorts of (Free (C,())) . s );

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,())) . s )
proof end;

definition
let C be initialized ConstructorSignature;
let c be constructor OperSymbol of C;
assume A1: len () = 0 ;
func c term -> expression of C equals :: ABCMIZ_1:def 29
[c, the carrier of C] -tree {};
coherence
[c, the carrier of C] -tree {} is expression of C
proof end;
end;

:: deftheorem defines term ABCMIZ_1:def 29 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C st len () = 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 () = 1 holds
for a being expression of C st ex s being SortSymbol of C st
( s = () . 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 () = 1 ;
let e be expression of C;
assume A2: ex s being SortSymbol of C st
( s = () . 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*> is expression of C
by A1, A2, Th42;
end;

:: deftheorem Def30 defines term ABCMIZ_1:def 30 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len () = 1 holds
for e being expression of C st ex s being SortSymbol of C st
( s = () . 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
( () term a is expression of C, an_Adj 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 () term a = () term b holds
a = b
proof end;

registration
let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;
cluster () term a -> compound ;
coherence
() term a is compound
proof end;
end;

registration
let C be initialized ConstructorSignature;
cluster non pair non empty Relation-like Function-like finite DecoratedTree-like compound for Element of Union the Sorts of (Free (C,()));
existence
ex b1 being expression of C st b1 is compound
proof end;
end;

theorem Th45: :: ABCMIZ_1:45
for C being initialized ConstructorSignature
for o being OperSymbol of C st len () = 2 holds
for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = () . 1 & s2 = () . 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 () = 2 ;
let e1, e2 be expression of C;
assume A2: ex s1, s2 being SortSymbol of C st
( s1 = () . 1 & s2 = () . 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*> is expression of C
by A1, A2, Th45;
end;

:: deftheorem Def31 defines term ABCMIZ_1:def 31 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len () = 2 holds
for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = () . 1 & s2 = () . 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*> )
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 )
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;
cluster (ast C) term (a,t) -> compound ;
coherence
(ast C) term (a,t) is compound
proof end;
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 ;
mode OperSymbol of s -> OperSymbol of S means :: ABCMIZ_1:def 32
the_result_sort_of it = s;
existence
ex b1 being OperSymbol of S st the_result_sort_of b1 = s
by A1;
end;

:: 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 b3 being OperSymbol of S holds
( b3 is OperSymbol of s iff the_result_sort_of b3 = s );

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
proof end;
:: original: ast
redefine func ast C -> OperSymbol of a_Type C;
coherence
ast C is OperSymbol of a_Type C
proof end;
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
proof end;

definition
let C be initialized ConstructorSignature;
A1: the Sorts of (Free (C,())) . () c= Union the Sorts of (Free (C,()))
proof end;
func QuasiTerms C -> Subset of (Free (C,())) equals :: ABCMIZ_1:def 33
the Sorts of (Free (C,())) . ();
coherence
the Sorts of (Free (C,())) . () is Subset of (Free (C,()))
by A1;
end;

:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :
for C being initialized ConstructorSignature holds QuasiTerms C = the Sorts of (Free (C,())) . ();

registration
let C be initialized ConstructorSignature;
coherence
( not QuasiTerms C is empty & QuasiTerms C is constituted-DTrees )
;
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;

definition
let x be variable;
let C be initialized ConstructorSignature;
func x -term C -> quasi-term of C equals :: ABCMIZ_1:def 34
root-tree [x,a_Term];
coherence
root-tree [x,a_Term] is quasi-term of C
proof end;
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];

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
proof end;

registration
let x be variable;
let C be initialized ConstructorSignature;
cluster x -term C -> non compound ;
coherence
not x -term C is compound
proof end;
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 () & p in () * ) )
proof end;

definition
let C be initialized ConstructorSignature;
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C;
assume A1: len p = len () ;
A2: p in () * 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 is compound expression of C
proof end;
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 () 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 () 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 () & e = c -trm p ) or ex a being expression of C, an_Adj C st e = () 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 () holds
c -trm p <> () 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 () 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 () 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 = () 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)
proof end;

definition
let C be initialized ConstructorSignature;
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 | if ex a9 being expression of C, an_Adj C st a = () term a9
otherwise () term a;
coherence
( ( ex a9 being expression of C, an_Adj C st a = () term a9 implies a | is expression of C, an_Adj C ) & ( ( for a9 being expression of C, an_Adj C holds not a = () term a9 ) implies () term a is expression of C, an_Adj C ) )
proof end;
consistency
for b1 being expression of C, an_Adj C holds verum
;
end;

:: 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 = () term a9 implies Non a = a | ) & ( ( for a9 being expression of C, an_Adj C holds not a = () term a9 ) implies Non a = () term a ) );

definition
let C be initialized ConstructorSignature;
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 = () term a9;
end;

:: 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 = () term a9 );

registration
let C be initialized ConstructorSignature;
existence
ex b1 being expression of C, an_Adj C st b1 is positive
proof end;
end;

theorem Th59: :: ABCMIZ_1:59
for C being initialized ConstructorSignature
for a being positive expression of C, an_Adj C holds Non a = () term a
proof end;

definition
let C be initialized ConstructorSignature;
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 = () term a9 );
end;

:: 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 = () term a9 ) );

registration
let C be initialized ConstructorSignature;
let a be positive expression of C, an_Adj C;
cluster Non a -> non positive negative ;
coherence
( Non a is negative & not Non a is positive )
proof end;
end;

registration
let C be initialized ConstructorSignature;
existence
ex b1 being expression of C, an_Adj C st
( b1 is negative & not b1 is positive )
proof end;
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 = () 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 = () 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 () 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
proof end;
end;

definition
let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;
attr a is regular means :Def39: :: ABCMIZ_1:def 39
( a is positive or a is negative );
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 ) );

registration
let C be initialized ConstructorSignature;
cluster positive -> non negative regular for expression of C, an_Adj C;
coherence
for b1 being expression of C, an_Adj C st b1 is positive holds
( b1 is regular & not b1 is negative )
;
cluster negative -> non positive regular for expression of C, an_Adj C;
coherence
for b1 being expression of C, an_Adj C st b1 is negative holds
( b1 is regular & not b1 is positive )
;
end;

registration
let C be initialized ConstructorSignature;
existence
ex b1 being expression of C, an_Adj C st b1 is regular
proof end;
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,()))
proof end;
func QuasiAdjs C -> Subset of (Free (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 } is Subset of (Free (C,()))
by A1;
end;

:: 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 } ;

registration
let C be initialized ConstructorSignature;
coherence
( not QuasiAdjs C is empty & QuasiAdjs C is constituted-DTrees )
proof end;
end;

definition end;

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 )
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;

registration
let C be initialized ConstructorSignature;
cluster non positive regular -> negative for expression of C, an_Adj C;
coherence
for b1 being quasi-adjective of C st not b1 is positive holds
b1 is negative
by Def39;
cluster non negative regular -> positive for expression of C, an_Adj C;
coherence
for b1 being quasi-adjective of C st not b1 is negative holds
b1 is positive
;
end;

registration
let C be initialized ConstructorSignature;
existence
ex b1 being quasi-adjective of C st b1 is positive
proof end;
existence
ex b1 being quasi-adjective of C st b1 is negative
proof end;
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 () & 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 () 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
proof end;
end;

theorem Th67: :: ABCMIZ_1:67
for C being initialized ConstructorSignature
for a being quasi-adjective of C holds Non (Non a) = a
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
proof end;

theorem :: ABCMIZ_1:69
for C being initialized ConstructorSignature
for a being quasi-adjective of C holds Non a <> a
proof end;

definition
let C be initialized ConstructorSignature;
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);
end;

:: 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) );

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 )
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 )
proof end;

registration
let C be initialized ConstructorSignature;
existence
ex b1 being expression of C, a_Type C st b1 is pure
proof end;
end;

definition
let C be initialized ConstructorSignature;
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 () : t is pure } ;
coherence
{ [A,t] where t is expression of C, a_Type C, A is finite Subset of () : t is pure } is set
;
end;

:: 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 () : t is pure } ;

registration
let C be initialized ConstructorSignature;
cluster QuasiTypes C -> non empty ;
coherence
not QuasiTypes C is empty
proof end;
end;

definition
let C be initialized ConstructorSignature;
mode quasi-type of C -> set means :Def43: :: ABCMIZ_1:def 43
it in QuasiTypes C;
existence
ex b1 being set st b1 in QuasiTypes C
proof end;
end;

:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :
for C being initialized ConstructorSignature
for b2 being set holds
( b2 is quasi-type of C iff b2 in QuasiTypes C );

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 () 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 () & y is pure expression of C, a_Type C ) )
proof end;

registration
let C be initialized ConstructorSignature;
cluster -> pair for quasi-type of C;
coherence
for b1 being quasi-type of C holds b1 is pair
proof end;
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 () & 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 () holds
m -trm p is pure expression of C, a_Type C
proof end;

theorem :: ABCMIZ_1:76
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;

notation
let C be initialized ConstructorSignature;
let A be finite Subset of ();
let q be pure expression of C, a_Type C;
synonym A ast q for [C,A];
end;

definition
let C be initialized ConstructorSignature;
let A be finite Subset of ();
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;

registration
let C be initialized ConstructorSignature;
let T be quasi-type of C;
cluster vars T -> finite for set ;
coherence
for b1 being set st b1 = T 1 holds
b1 is finite
proof end;
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;

definition
let C be initialized ConstructorSignature;
let T be quasi-type of C;
:: original: vars
redefine func adjs T -> Subset of ();
coherence
vars T is Subset of ()
proof end;
:: original: the_base_of
redefine func the_base_of T -> pure expression of C, a_Type C;
coherence
proof end;
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 () 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 ()
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 () ;

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
proof end;

definition
let C be initialized ConstructorSignature;
let T be quasi-type of C;
let a be quasi-adjective of C;
func a ast T -> quasi-type of C equals :: ABCMIZ_1:def 44
coherence
[({a} \/ (adjs T)),()] is quasi-type of C
proof end;
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)),()];

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 ) ;

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
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) by XBOOLE_1:4;

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;
cluster () . s -> finite ;
coherence
() . s is finite
proof end;
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));
cluster () . s -> finite ;
coherence
() . s is finite
proof end;
end;

definition
let S be non void Signature;
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;
uniqueness
for b1, b2 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st ( for t being Element of (Free (S,X)) holds b1 . t = () . s ) & ( for t being Element of (Free (S,X)) holds b2 . t = () . s ) holds
b1 = b2
proof end;
existence
ex b1 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st
for t being Element of (Free (S,X)) holds b1 . t = () . s
proof end;
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 b4 being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds
( b4 = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b4 . t = () . s );

definition
let C be initialized ConstructorSignature;
let e be expression of C;
func variables_in e -> Subset of Vars equals :: ABCMIZ_1:def 46
() . ();
coherence
() . () is Subset of Vars
proof end;
end;

:: deftheorem defines variables_in ABCMIZ_1:def 46 :
for C being initialized ConstructorSignature
for e being expression of C holds variables_in e = () . ();

registration
let C be initialized ConstructorSignature;
let e be expression of C;
coherence ;
end;

definition
let C be initialized ConstructorSignature;
let e be expression of C;
func vars e -> finite Subset of Vars equals :: ABCMIZ_1:def 47
varcl ();
coherence by Th24;
end;

:: deftheorem defines vars ABCMIZ_1:def 47 :
for C being initialized ConstructorSignature
for e being expression of C holds vars e = varcl ();

theorem :: ABCMIZ_1:85
for C being initialized ConstructorSignature
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;

theorem :: ABCMIZ_1:87
for C being initialized ConstructorSignature
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 { () 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 }
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 () holds
variables_in (c -trm p) = union { () 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 () 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 {}) = EmptyMS 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
proof end;

theorem Th94: :: ABCMIZ_1:94
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds variables_in (() 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 (() 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)
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)) = () \/ ()
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)
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
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;

definition
let C be initialized ConstructorSignature;
let T be quasi-type of C;
func variables_in T -> Subset of Vars equals :: ABCMIZ_1:def 48
(union ((((),()) variables_in) .: (adjs T))) \/ ();
coherence
(union ((((),()) variables_in) .: (adjs T))) \/ () is Subset of Vars
proof end;
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 ((((),()) variables_in) .: (adjs T))) \/ ();

registration
let C be initialized ConstructorSignature;
let T be quasi-type of C;
coherence
proof end;
end;

definition
let C be initialized ConstructorSignature;
let T be quasi-type of C;
func vars T -> finite Subset of Vars equals :: ABCMIZ_1:def 49
varcl ();
coherence by Th24;
end;

:: deftheorem defines vars ABCMIZ_1:def 49 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds vars T = varcl ();

theorem :: ABCMIZ_1:101
for C being initialized ConstructorSignature
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) = () \/ ()
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)
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 () holds variables_in (A ast q) = (union { () where a is quasi-adjective of C : a in A } ) \/ ()
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 () 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 (({} ()) 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 = {} )
proof end;

definition
let C be initialized ConstructorSignature;
let T be quasi-type of C;
attr T is ground means :Def50: :: ABCMIZ_1:def 50
variables_in T = {} ;
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 = {} );

registration
let C be initialized ConstructorSignature;
existence
ex b1 being expression of C, a_Type C st
( b1 is ground & b1 is pure )
proof end;
existence
ex b1 being quasi-adjective of C st b1 is ground
proof end;
end;

theorem Th108: :: ABCMIZ_1:108
for C being initialized ConstructorSignature
for t being ground pure expression of C, a_Type C holds ({} ()) ast t is ground
proof end;

registration
let C be initialized ConstructorSignature;
let t be ground pure expression of C, a_Type C;
cluster t ast -> ground for quasi-type of C;
coherence
for b1 being quasi-type of C st b1 = ({} ()) ast t holds
b1 is ground
by Th108;
end;

registration
let C be initialized ConstructorSignature;
cluster pair non empty ground for quasi-type of C;
existence
ex b1 being quasi-type of C st b1 is ground
proof end;
end;

registration
let C be initialized ConstructorSignature;
let T be ground quasi-type of C;
let a be ground quasi-adjective of C;
cluster a ast T -> ground ;
coherence
a ast T is ground
proof end;
end;

:: Type widening is smooth iff
:: vars-function is sup-semilattice homomorphism from widening sup-semilattice
:: into VarPoset
definition
func VarPoset -> non empty strict Poset equals :: ABCMIZ_1:def 51
(InclPoset { () where A is finite Subset of Vars : verum } ) opp ;
coherence
(InclPoset { () where A is finite Subset of Vars : verum } ) opp is non empty strict Poset
proof end;
end;

:: deftheorem defines VarPoset ABCMIZ_1:def 51 :
VarPoset = (InclPoset { () where A is finite Subset of Vars : verum } ) opp ;

theorem Th109: :: ABCMIZ_1:109
for x, y being Element of VarPoset holds
( x <= y iff y c= x )
proof end;

:: registration
:: let V1,V2 be Element of VarPoset;
:: identify V1 <= V2 with V2 c= V1;
:: compatibility by Th22;
:: end;
theorem Th110: :: ABCMIZ_1:110
for x being set holds
( x is Element of VarPoset iff ( x is finite Subset of Vars & varcl x = x ) )
proof end;

registration
coherence
proof end;
end;

theorem Th111: :: ABCMIZ_1:111
for V1, V2 being Element of VarPoset holds
( V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2 )
proof end;

registration
let V1, V2 be Element of VarPoset;
identify V1 "\/" V2 with V1 /\ V2;
compatibility
V1 "\/" V2 = V1 /\ V2
by Th111;
identify V1 "/\" V2 with V1 \/ V2;
compatibility
V1 "/\" V2 = V1 \/ V2
by Th111;
end;

theorem Th112: :: ABCMIZ_1:112
for X being non empty Subset of VarPoset holds
( ex_sup_of X, VarPoset & sup X = meet X )
proof end;

registration
coherence
proof end;
end;

theorem :: ABCMIZ_1:113
proof end;

definition
let C be initialized ConstructorSignature;
func vars-function C -> Function of (), the carrier of VarPoset means :: ABCMIZ_1:def 52
for T being quasi-type of C holds it . T = vars T;
uniqueness
for b1, b2 being Function of (), the carrier of VarPoset st ( for T being quasi-type of C holds b1 . T = vars T ) & ( for T being quasi-type of C holds b2 . T = vars T ) holds
b1 = b2
proof end;
existence
ex b1 being Function of (), the carrier of VarPoset st
for T being quasi-type of C holds b1 . T = vars T
proof end;
end;

:: deftheorem defines vars-function ABCMIZ_1:def 52 :
for C being initialized ConstructorSignature
for b2 being Function of (), the carrier of VarPoset holds
( b2 = vars-function C iff for T being quasi-type of C holds b2 . T = vars T );

definition
let L be non empty Poset;
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 = () | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) );
end;

:: 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 = () | 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;
cluster RelStr(# {T},(id {T}) #) -> smooth ;
coherence
RelStr(# {T},(id {T}) #) is smooth
proof end;
end;

scheme :: ABCMIZ_1:sch 2
StructInd{ F1() -> initialized ConstructorSignature, P1[ set ], F2() -> expression of F1() } :
P1[F2()]
provided
A1: for x being variable holds P1[x -term F1()] and
A2: for c being constructor OperSymbol of F1()
for p being FinSequence of QuasiTerms F1() st len p = len () & ( for t being quasi-term of F1() st t in rng p holds
P1[t] ) holds
P1[c -trm p] and
A3: for a being expression of F1(), an_Adj F1() st P1[a] holds
P1[(non_op F1()) term a] and
A4: for a being expression of F1(), an_Adj F1() st P1[a] holds
for t being expression of F1(), a_Type F1() st P1[t] holds
P1[(ast F1()) term (a,t)]
proof end;

definition
let S be ManySortedSign ;
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;
attr X is with_missing_variables means :: ABCMIZ_1:def 55
X " c= rng the ResultSort of S;
end;

:: 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 );

:: deftheorem 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 );

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 )
proof end;

registration
coherence
proof end;
let C be ConstructorSignature;
coherence
proof end;
end;

registration
let S be ManySortedSign ;
coherence
for b1 being ManySortedSet of the carrier of S st b1 is V8() holds
b1 is with_missing_variables
proof end;
end;

registration
let S be ManySortedSign ;
existence
ex b1 being ManySortedSet of the carrier of S st b1 is with_missing_variables
proof end;
end;

registration
existence
ex b1 being ConstructorSignature st
( b1 is initialized & b1 is with_an_operation_for_each_sort & b1 is strict )
proof end;
end;

registration
let C be with_an_operation_for_each_sort ManySortedSign ;
coherence
for b1 being ManySortedSet of the carrier of C holds b1 is with_missing_variables
proof end;
end;

definition
let G be non empty DTConstrStr ;
:: original: Terminals
redefine func Terminals G -> Subset of G;
coherence
Terminals G is Subset of G
proof end;
:: original: NonTerminals
redefine func NonTerminals G -> Subset of G;
coherence
NonTerminals G is Subset of G
proof end;
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 /\ () 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
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
proof end;

theorem Th118: :: ABCMIZ_1:118
for S being set
for X, Y being ManySortedSet of S st X c= Y holds
Union () c= Union ()
proof end;

theorem :: ABCMIZ_1:119
for S being non void Signature
for X, Y being ManySortedSet of the carrier of S st X c= Y holds
the carrier of () c= the carrier of () by ;

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 () = [: the carrier' of S,{ the carrier of S}:] & Terminals () = Union () )
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 () c= Terminals () & the Rules of () c= the Rules of () & TS () c= TS () )
proof end;

theorem Th122: :: ABCMIZ_1:122
for C being initialized ConstructorSignature
for t being set holds
( t in Terminals (DTConMSA ()) iff ex x being variable st t = [x,()] )
proof end;

theorem Th123: :: ABCMIZ_1:123
for C being initialized ConstructorSignature
for t being set holds
( t in NonTerminals (DTConMSA ()) iff ( t = [(ast C), the carrier of C] or t = [(), 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 --> ))
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 --> )) st t in Union the Sorts of (Free (S,X)) holds
t in the Sorts of (Free (S,X)) . ()
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
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 ()
for g2 being Symbol of ()
for p1 being FinSequence of the carrier of ()
for p2 being FinSequence of the carrier of () 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 ()
proof end;

definition
let S be non void Signature;
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
ex b1 being UnOp of (Union the Sorts of (Free (S,X))) st
for s being SortSymbol of S holds b1 .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s
proof end;
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 b3 being UnOp of (Union the Sorts of (Free (S,X))) holds
( b3 is term-transformation of S,X iff for s being SortSymbol of S holds b3 .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s );

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 )
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 )
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;
attr t is substitution means :: ABCMIZ_1:def 57
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;
end;

:: 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 );

scheme :: ABCMIZ_1:sch 3
StructDef{ F1() -> initialized ConstructorSignature, F2( set ) -> expression of F1(), F3( set ) -> expression of F1(), F4( set , set ) -> expression of F1(), F5( set , set ) -> expression of F1() } :
ex f being term-transformation of F1(), MSVars F1() st
( ( for x being variable holds f . (x -term F1()) = F2(x) ) & ( for c being constructor OperSymbol of F1()
for p, q being FinSequence of QuasiTerms F1() st len p = len () & q = f * p holds
f . (c -trm p) = F4(c,q) ) & ( for a being expression of F1(), an_Adj F1() holds f . ((non_op F1()) term a) = F3((f . a)) ) & ( for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds f . ((ast F1()) term (a,t)) = F5((f . a),(f . t)) ) )
provided
A1: for x being variable holds F2(x) is quasi-term of F1() and
A2: for c being constructor OperSymbol of F1()
for p being FinSequence of QuasiTerms F1() st len p = len () holds
F4(c,p) is expression of F1(), the_result_sort_of c and
A3: for a being expression of F1(), an_Adj F1() holds F3(a) is expression of F1(), an_Adj F1() and
A4: for a being expression of F1(), an_Adj F1()
for t being expression of F1(), a_Type F1() holds F5(a,t) is expression of F1(), a_Type F1()
proof end;

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;

definition end;

definition
let C be initialized ConstructorSignature;
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;
end;

:: 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 );

notation
let C be initialized ConstructorSignature;
let f be valuation of C;
antonym relevant f for irrelevant ;
end;

registration
let C be initialized ConstructorSignature;
coherence
for b1 being valuation of C st b1 is empty holds
b1 is irrelevant
;
end;

registration
let C be initialized ConstructorSignature;
existence
ex b1 being valuation of C st b1 is empty
proof end;
end;

definition
let C be initialized ConstructorSignature;
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 } is valuation of C
proof end;
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 } ;

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 ) )
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 )
proof end;
end;

registration
let C be initialized ConstructorSignature;
let X be empty Subset of Vars;
cluster C idval X -> empty ;
coherence
C idval X is empty
proof end;
end;

definition
let C be initialized ConstructorSignature;
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 () & q = it * p holds
it . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds it . (() term a) = () 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
ex b1 being term-transformation of C, MSVars C st
( ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (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 () & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . (() term a) = () term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) )
proof end;
correctness
uniqueness
for b1, b2 being term-transformation of C, MSVars C st ( for x being variable holds
( ( x in dom f implies b1 . (x -term C) = f . x ) & ( not x in dom f implies b1 . (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 () & q = b1 * p holds
b1 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b1 . (() term a) = () term (b1 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b1 . ((ast C) term (a,t)) = (ast C) term ((b1 . a),(b1 . t)) ) & ( for x being variable holds
( ( x in dom f implies b2 . (x -term C) = f . x ) & ( not x in dom f implies b2 . (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 () & q = b2 * p holds
b2 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b2 . (() term a) = () term (b2 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b2 . ((ast C) term (a,t)) = (ast C) term ((b2 . a),(b2 . t)) ) holds
b1 = b2
;
proof end;
end;

:: deftheorem Def60 defines # ABCMIZ_1:def 60 :
for C being initialized ConstructorSignature
for f being valuation of C
for b3 being term-transformation of C, MSVars C holds
( b3 = f # iff ( ( for x being variable holds
( ( x in dom f implies b3 . (x -term C) = f . x ) & ( not x in dom f implies b3 . (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 () & q = b3 * p holds
b3 . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b3 . (() term a) = () term (b3 . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b3 . ((ast C) term (a,t)) = (ast C) term ((b3 . a),(b3 . t)) ) ) );

registration
let C be initialized ConstructorSignature;
let f be valuation of C;
coherence
proof end;
end;

definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let e be expression of C;
func e at f -> expression of C equals :: ABCMIZ_1:def 61
(f #) . e;
coherence
(f #) . e is expression of C
;
end;

:: 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;

definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let p be FinSequence;
assume A1: rng p c= Union the Sorts of (Free (C,())) ;
func p at f -> FinSequence equals :Def62: :: ABCMIZ_1:def 62
(f #) * p;
coherence
(f #) * p is FinSequence
proof end;
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,())) 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;
:: original: at
redefine func p at f -> FinSequence of QuasiTerms C equals :: ABCMIZ_1:def 63
(f #) * p;
coherence
p at f is FinSequence of QuasiTerms C
proof end;
compatibility
for b1 being FinSequence of QuasiTerms C holds
( b1 = p at f iff b1 = (f #) * p )
proof end;
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;

theorem :: ABCMIZ_1:132
for C being initialized ConstructorSignature
for f being valuation of C
for x being variable st not x in dom f holds
(x -term C) at f = x -term C by Def60;

theorem :: ABCMIZ_1:133
for C being initialized ConstructorSignature
for f being valuation of C
for x being variable st x in dom f holds
(x -term C) at f = f . x by Def60;

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 () 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 (() term a) at f = () 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;

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
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,())))
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
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,())))
proof end;

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
proof end;
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
proof end;
end;

registration
let C be initialized ConstructorSignature;
let f be valuation of C;
let a be positive expression of C, an_Adj C;
cluster a at f -> positive for expression of C, an_Adj C;
coherence
for b1 being expression of C, an_Adj C st b1 = a at f holds
b1 is positive
proof end;
end;

registration
let C be initialized ConstructorSignature;
let f be valuation of C;
let a be negative expression of C, an_Adj C;
cluster a at f -> negative for expression of C, an_Adj C;
coherence
for b1 being expression of C, an_Adj C st b1 = a at f holds
b1 is negative
proof end;
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
proof end;
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)
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
proof end;
end;

registration
let C be initialized ConstructorSignature;
let f be valuation of C;
let t be pure expression of C, a_Type C;
cluster t at f -> pure for expression of C, a_Type C;
coherence
for b1 being expression of C, a_Type C st b1 = t at f holds
b1 is pure
proof end;
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 ) )
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
proof end;

definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let A be Subset of ();
func A at f -> Subset of () 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 } is Subset of ()
proof end;
end;

:: deftheorem defines at ABCMIZ_1:def 64 :
for C being initialized ConstructorSignature
for f being valuation of C
for A being Subset of () 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 ()
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 () 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 () 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 ();
cluster A at f -> finite ;
coherence
A at f is finite
proof end;
end;

definition
let C be initialized ConstructorSignature;
let f be valuation of C;
let T be quasi-type of C;
func T at f -> quasi-type of C equals :: ABCMIZ_1:def 65
((adjs T) at f) ast (() at f);
coherence
((adjs T) at f) ast (() at f) is quasi-type of C
;
end;

:: 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 (() 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) = () at f ) ;

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)
proof end;

definition
let C be initialized ConstructorSignature;
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
ex b1 being valuation of C st
( dom b1 = (dom f) \/ (dom g) & ( for x being variable st x in dom b1 holds
b1 . x = ((x -term C) at f) at g ) )
proof end;
uniqueness
for b1, b2 being valuation of C st dom b1 = (dom f) \/ (dom g) & ( for x being variable st x in dom b1 holds
b1 . x = ((x -term C) at f) at g ) & dom b2 = (dom f) \/ (dom g) & ( for x being variable st x in dom b2 holds
b2 . x = ((x -term C) at f) at g ) holds
b1 = b2
proof end;
end;

:: deftheorem Def66 defines at ABCMIZ_1:def 66 :
for C being initialized ConstructorSignature
for f, g, b4 being valuation of C holds
( b4 = f at g iff ( dom b4 = (dom f) \/ (dom g) & ( for x being variable st x in dom b4 holds
b4 . x = ((x -term C) at f) at g ) ) );

registration
let C be initialized ConstructorSignature;
let f, g be irrelevant valuation of C;
cluster f at g -> irrelevant ;
coherence
f at g is irrelevant
proof end;
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)
proof end;

theorem Th150: :: ABCMIZ_1:150
for C being initialized ConstructorSignature
for A being Subset of ()
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)
proof end;