:: A Model of Mizar Concepts -- Unification
:: by Grzegorz Bancerek
::
:: Received November 20, 2009
:: Copyright (c) 2009-2011 Association of Mizar Users


begin

theorem Th1: :: ABCMIZ_A:1
for x being pair set holds x = [(x `1),(x `2)]
proof end;

scheme :: ABCMIZ_A:sch 1
MinimalElement{ F1() -> non empty finite set , P1[ set , set ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() holds
not P1[y,x] ) )
provided
A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
not P1[y,x] and
A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds
P1[x,z]
proof end;

scheme :: ABCMIZ_A:sch 2
FiniteC{ F1() -> finite set , P1[ set ] } :
P1[F1()]
provided
A1: for A being Subset of F1() st ( for B being set st B c< A holds
P1[B] ) holds
P1[A]
proof end;

scheme :: ABCMIZ_A:sch 3
Numeration{ F1() -> finite set , P1[ set , set ] } :
ex s being one-to-one FinSequence st
( rng s = F1() & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j ) )
provided
A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
not P1[y,x] and
A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds
P1[x,z]
proof end;

theorem Th2: :: ABCMIZ_A:2
for x being variable holds varcl (vars x) = vars x
proof end;

theorem Th3: :: ABCMIZ_A:3
for C being initialized ConstructorSignature
for e being expression of C holds
( e is compound iff for x being Element of Vars holds not e = x -term C )
proof end;

begin

registration
cluster empty Relation-like Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like Element of QuasiLoci ;
existence
ex b1 being quasi-loci st b1 is empty by ABCMIZ_1:29;
end;

definition
let C be ConstructorSignature;
attr C is standardized means :Def1: :: ABCMIZ_A:def 1
 for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) );
end;

:: deftheorem Def1 defines standardized ABCMIZ_A:def 1 :
for C being ConstructorSignature holds
( C is standardized iff for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) );

theorem Th4: :: ABCMIZ_A:4
for C being ConstructorSignature st C is standardized holds
for o being OperSymbol of C holds
( o is constructor iff o in Constructors )
proof end;

registration
cluster MaxConstrSign -> standardized ;
coherence
MaxConstrSign is standardized
proof end;
end;

registration
cluster non empty non void strict V147() constructor initialized standardized ManySortedSign ;
existence
ex b1 being ConstructorSignature st
( b1 is initialized & b1 is standardized & b1 is strict )
proof end;
end;

definition
let C be initialized standardized ConstructorSignature;
let c be constructor OperSymbol of C;
func loci_of c -> quasi-loci equals :: ABCMIZ_A:def 2
(c `2) `1 ;
coherence
(c `2) `1 is quasi-loci
proof end;
end;

:: deftheorem defines loci_of ABCMIZ_A:def 2 :
for C being initialized standardized ConstructorSignature
for c being constructor OperSymbol of C holds loci_of c = (c `2) `1 ;

registration
let C be ConstructorSignature;
cluster V147() constructor Subsignature of C;
existence
ex b1 being Subsignature of C st b1 is constructor
proof end;
end;

registration
let C be initialized ConstructorSignature;
cluster non empty non void V147() constructor initialized Subsignature of C;
existence
ex b1 being constructor Subsignature of C st b1 is initialized
proof end;
end;

registration
let C be standardized ConstructorSignature;
cluster constructor -> constructor standardized Subsignature of C;
coherence
for b1 being constructor Subsignature of C holds b1 is standardized
proof end;
end;

theorem :: ABCMIZ_A:5
for S1, S2 being standardized ConstructorSignature st the carrier' of S1 = the carrier' of S2 holds
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
proof end;

theorem :: ABCMIZ_A:6
for C being ConstructorSignature holds
( C is standardized iff C is Subsignature of MaxConstrSign )
proof end;

registration
let C be initialized ConstructorSignature;
cluster non empty Relation-like Function-like finite DecoratedTree-like finite-branching non pair non compound expression of C, a_Term C;
existence
not for b1 being quasi-term of C holds b1 is compound
proof end;
end;

registration
cluster -> pair Element of Vars ;
coherence
for b1 being Element of Vars holds b1 is pair
proof end;
end;

theorem Th7: :: ABCMIZ_A:7
for x being Element of Vars st vars x is natural holds
vars x = 0
proof end;

theorem Th8: :: ABCMIZ_A:8
Vars misses Constructors
proof end;

theorem :: ABCMIZ_A:9
for x being Element of Vars holds
( x <> * & x <> non_op ) ;

theorem Th10: :: ABCMIZ_A:10
for C being standardized ConstructorSignature holds Vars misses the carrier' of C
proof end;

theorem Th11: :: ABCMIZ_A:11
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
proof end;

registration
let C be initialized standardized ConstructorSignature;
let e be expression of C;
cluster e . {} -> pair ;
coherence
e . {} is pair
proof end;
end;

theorem Th12: :: ABCMIZ_A:12
for C being initialized ConstructorSignature
for e being expression of C
for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
proof end;

theorem Th13: :: ABCMIZ_A:13
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
proof end;

theorem Th14: :: ABCMIZ_A:14
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
proof end;

theorem :: ABCMIZ_A:15
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
proof end;

theorem :: ABCMIZ_A:16
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
proof end;

theorem Th17: :: ABCMIZ_A:17
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Vars holds
ex x being Element of Vars st
( x = (e . {}) `1 & e = x -term C )
proof end;

theorem Th18: :: ABCMIZ_A:18
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 = * holds
ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
proof end;

theorem Th19: :: ABCMIZ_A:19
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 = non_op holds
ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
proof end;

theorem Th20: :: ABCMIZ_A:20
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
proof end;

theorem Th21: :: ABCMIZ_A:21
for C being initialized standardized ConstructorSignature
for t being quasi-term of C holds
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
proof end;

theorem Th22: :: ABCMIZ_A:22
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
proof end;

theorem :: ABCMIZ_A:23
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
proof end;

theorem Th24: :: ABCMIZ_A:24
for C being initialized standardized ConstructorSignature
for a being expression of C holds
( a is positive quasi-adjective of C iff ( (a . {}) `1 in Constructors & ((a . {}) `1) `1 = an_Adj ) )
proof end;

theorem :: ABCMIZ_A:25
for C being initialized standardized ConstructorSignature
for a being quasi-adjective of C holds
( a is negative iff (a . {}) `1 = non_op )
proof end;

theorem :: ABCMIZ_A:26
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
proof end;

begin

set MC = MaxConstrSign ;

definition
mode expression is expression of MaxConstrSign;
mode valuation is valuation of MaxConstrSign;
mode quasi-adjective is quasi-adjective of MaxConstrSign;
func QuasiAdjs -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 3
 QuasiAdjs MaxConstrSign;
coherence
QuasiAdjs MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;
mode quasi-term is quasi-term of MaxConstrSign;
func QuasiTerms -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 4
 QuasiTerms MaxConstrSign;
coherence
QuasiTerms MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;
mode quasi-type is quasi-type of MaxConstrSign ;
func QuasiTypes -> set equals :: ABCMIZ_A:def 5
 QuasiTypes MaxConstrSign;
coherence
QuasiTypes MaxConstrSign is set ;
end;

:: deftheorem defines QuasiAdjs ABCMIZ_A:def 3 :
QuasiAdjs = QuasiAdjs MaxConstrSign;

:: deftheorem defines QuasiTerms ABCMIZ_A:def 4 :
QuasiTerms = QuasiTerms MaxConstrSign;

:: deftheorem defines QuasiTypes ABCMIZ_A:def 5 :
QuasiTypes = QuasiTypes MaxConstrSign;

registration
cluster QuasiAdjs -> non empty ;
coherence
not QuasiAdjs is empty ;
cluster QuasiTerms -> non empty ;
coherence
not QuasiTerms is empty ;
cluster QuasiTypes -> non empty ;
coherence
not QuasiTypes is empty ;
end;

definition
:: original: Modes
redefine func Modes -> non empty Subset of Constructors;
coherence
Modes is non empty Subset of Constructors
proof end;
:: original: Attrs
redefine func Attrs -> non empty Subset of Constructors;
coherence
Attrs is non empty Subset of Constructors
proof end;
:: original: Funcs
redefine func Funcs -> non empty Subset of Constructors;
coherence
Funcs is non empty Subset of Constructors by XBOOLE_1:7;
end;

definition
func set-constr -> Element of Modes equals :: ABCMIZ_A:def 6
[a_Type,[{},0]];
coherence
[a_Type,[{},0]] is Element of Modes
proof end;
end;

:: deftheorem defines set-constr ABCMIZ_A:def 6 :
set-constr = [a_Type,[{},0]];

theorem :: ABCMIZ_A:27
( kind_of set-constr = a_Type & loci_of set-constr = {} & index_of set-constr = 0 )
proof end;

theorem Th28: :: ABCMIZ_A:28
Constructors = [:{a_Type,an_Adj,a_Term},[:QuasiLoci,NAT:]:]
proof end;

theorem Th29: :: ABCMIZ_A:29
for i being Nat
for l being quasi-loci holds
( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
proof end;

theorem Th30: :: ABCMIZ_A:30
for i being Nat ex l being quasi-loci st len l = i
proof end;

theorem Th31: :: ABCMIZ_A:31
for X being finite Subset of Vars ex l being quasi-loci st rng l = varcl X
proof end;

theorem Th32: :: ABCMIZ_A:32
for X, o being set
for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X holds
p is FinSequence of X
proof end;

definition
let C be initialized ConstructorSignature;
let e be expression of C;
mode subexpression of e -> expression of C means :: ABCMIZ_A:def 7
it in Subtrees e;
existence
ex b1 being expression of C st b1 in Subtrees e by TREES_9:12;
func constrs e -> set equals :: ABCMIZ_A:def 8
(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ;
coherence
(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } is set ;
func main-constr e -> set equals :Def9: :: ABCMIZ_A:def 9
(e . {}) `1 if e is compound
otherwise {} ;
correctness
coherence
( ( e is compound implies (e . {}) `1 is set ) & ( not e is compound implies {} is set ) );
consistency
for b1 being set holds verum;
;
func args e -> FinSequence of (Free (C,(MSVars C))) means :: ABCMIZ_A:def 10
e = (e . {}) -tree it;
existence
ex b1 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1
proof end;
uniqueness
for b1, b2 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 & e = (e . {}) -tree b2 holds
b1 = b2 by TREES_4:15;
end;

:: deftheorem defines subexpression ABCMIZ_A:def 7 :
for C being initialized ConstructorSignature
for e, b3 being expression of C holds
( b3 is subexpression of e iff b3 in Subtrees e );

:: deftheorem defines constrs ABCMIZ_A:def 8 :
for C being initialized ConstructorSignature
for e being expression of C holds constrs e = (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ;

:: deftheorem Def9 defines main-constr ABCMIZ_A:def 9 :
for C being initialized ConstructorSignature
for e being expression of C holds
( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) );

:: deftheorem defines args ABCMIZ_A:def 10 :
for C being initialized ConstructorSignature
for e being expression of C
for b3 being FinSequence of (Free (C,(MSVars C))) holds
( b3 = args e iff e = (e . {}) -tree b3 );

theorem Th33: :: ABCMIZ_A:33
for C being initialized ConstructorSignature
for e being expression of C holds e is subexpression of e
proof end;

theorem :: ABCMIZ_A:34
for x being variable
for C being initialized ConstructorSignature holds main-constr (x -term C) = {} by Def9;

theorem Th35: :: ABCMIZ_A: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
main-constr (c -trm p) = c
proof end;

definition
let C be initialized ConstructorSignature;
let e be expression of C;
attr e is constructor means :Def11: :: ABCMIZ_A:def 11
( e is compound & main-constr e is constructor OperSymbol of C );
end;

:: deftheorem Def11 defines constructor ABCMIZ_A:def 11 :
for C being initialized ConstructorSignature
for e being expression of C holds
( e is constructor iff ( e is compound & main-constr e is constructor OperSymbol of C ) );

registration
let C be initialized ConstructorSignature;
cluster constructor -> compound Element of Union the Sorts of (Free (C,(MSVars C)));
coherence
for b1 being expression of C st b1 is constructor holds
b1 is compound by Def11;
end;

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

registration
let C be initialized ConstructorSignature;
let e be constructor expression of C;
cluster non empty Relation-like Function-like finite DecoratedTree-like finite-branching non pair constructor subexpression of e;
existence
ex b1 being subexpression of e st b1 is constructor
proof end;
end;

registration
let S be non void Signature;
let X be V6() ManySortedSet of S;
let t be Element of (Free (S,X));
cluster proj2 t -> Relation-like ;
coherence
rng t is Relation-like
proof end;
end;

theorem :: ABCMIZ_A:36
for C being initialized ConstructorSignature
for e being constructor expression of C holds main-constr e in constrs e
proof end;

begin

definition
let C be non void Signature;
attr C is arity-rich means :Def12: :: ABCMIZ_A:def 12
 for n being Nat
for s being SortSymbol of C holds not { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite ;
let o be OperSymbol of C;
attr o is nullary means :Def13: :: ABCMIZ_A:def 13
 the_arity_of o = {} ;
attr o is unary means :Def14: :: ABCMIZ_A:def 14
 len (the_arity_of o) = 1;
attr o is binary means :Def15: :: ABCMIZ_A:def 15
 len (the_arity_of o) = 2;
end;

:: deftheorem Def12 defines arity-rich ABCMIZ_A:def 12 :
for C being non void Signature holds
( C is arity-rich iff for n being Nat
for s being SortSymbol of C holds not { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite );

:: deftheorem Def13 defines nullary ABCMIZ_A:def 13 :
for C being non void Signature
for o being OperSymbol of C holds
( o is nullary iff the_arity_of o = {} );

:: deftheorem Def14 defines unary ABCMIZ_A:def 14 :
for C being non void Signature
for o being OperSymbol of C holds
( o is unary iff len (the_arity_of o) = 1 );

:: deftheorem Def15 defines binary ABCMIZ_A:def 15 :
for C being non void Signature
for o being OperSymbol of C holds
( o is binary iff len (the_arity_of o) = 2 );

theorem Th37: :: ABCMIZ_A:37
for C being non void Signature
for o being OperSymbol of C holds
( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
proof end;

registration
let C be ConstructorSignature;
cluster non_op C -> unary ;
coherence
non_op C is unary
proof end;
cluster ast C -> binary ;
coherence
ast C is binary
proof end;
end;

registration
let C be ConstructorSignature;
cluster nullary -> constructor Element of the carrier' of C;
coherence
for b1 being OperSymbol of C st b1 is nullary holds
b1 is constructor
proof end;
end;

theorem Th38: :: ABCMIZ_A:38
for C being ConstructorSignature holds
( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) )
proof end;

registration
let C be initialized ConstructorSignature;
cluster constructor nullary OperSymbol of a_Type C;
existence
ex b1 being OperSymbol of a_Type C st
( b1 is nullary & b1 is constructor )
proof end;
cluster constructor nullary OperSymbol of an_Adj C;
existence
ex b1 being OperSymbol of an_Adj C st
( b1 is nullary & b1 is constructor )
proof end;
end;

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

registration
cluster non void V147() arity-rich -> non void with_an_operation_for_each_sort ManySortedSign ;
coherence
for b1 being non void Signature st b1 is arity-rich holds
b1 is with_an_operation_for_each_sort
proof end;
cluster V147() constructor arity-rich -> initialized ManySortedSign ;
coherence
for b1 being ConstructorSignature st b1 is arity-rich holds
b1 is initialized
proof end;
end;

registration
cluster MaxConstrSign -> arity-rich ;
coherence
MaxConstrSign is arity-rich
proof end;
end;

registration
cluster non empty non void V147() constructor initialized arity-rich ManySortedSign ;
existence
ex b1 being ConstructorSignature st
( b1 is arity-rich & b1 is initialized )
proof end;
end;

registration
let C be arity-rich ConstructorSignature;
let s be SortSymbol of C;
cluster constructor nullary OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is nullary & b1 is constructor )
proof end;
cluster constructor unary OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is unary & b1 is constructor )
proof end;
cluster constructor binary OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is binary & b1 is constructor )
proof end;
end;

registration
let C be arity-rich ConstructorSignature;
cluster constructor unary Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st
( b1 is unary & b1 is constructor )
proof end;
cluster constructor binary Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st
( b1 is binary & b1 is constructor )
proof end;
end;

theorem Th39: :: ABCMIZ_A:39
for C being initialized ConstructorSignature
for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o
proof end;

definition
let C be initialized ConstructorSignature;
let m be constructor nullary OperSymbol of a_Type C;
:: original: term
redefine func m term -> pure expression of C, a_Type C;
coherence
m term is pure expression of C, a_Type C
proof end;
end;

definition
let c be Element of Constructors ;
func @ c -> constructor OperSymbol of MaxConstrSign equals :: ABCMIZ_A:def 16
c;
coherence
c is constructor OperSymbol of MaxConstrSign
proof end;
end;

:: deftheorem defines @ ABCMIZ_A:def 16 :
for c being Element of Constructors holds @ c = c;

definition
let m be Element of Modes ;
:: original: @
redefine func @ m -> constructor OperSymbol of a_Type MaxConstrSign;
coherence
@ m is constructor OperSymbol of a_Type MaxConstrSign
proof end;
end;

registration
cluster @ set-constr -> constructor nullary ;
coherence
@ set-constr is nullary
proof end;
end;

theorem :: ABCMIZ_A:40
the_arity_of (@ set-constr) = {} by Def13;

definition
func set-type -> quasi-type equals :: ABCMIZ_A:def 17
({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);
coherence
({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term) is quasi-type ;
end;

:: deftheorem defines set-type ABCMIZ_A:def 17 :
set-type = ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);

theorem :: ABCMIZ_A:41
( adjs set-type = {} & the_base_of set-type = (@ set-constr) term ) by MCART_1:7;

definition
let l be FinSequence of Vars ;
func args l -> FinSequence of QuasiTerms MaxConstrSign means :Def18: :: ABCMIZ_A:def 18
( len it = len l & ( for i being Nat st i in dom l holds
it . i = (l /. i) -term MaxConstrSign ) );
existence
ex b1 being FinSequence of QuasiTerms MaxConstrSign st
( len b1 = len l & ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) )
proof end;
uniqueness
for b1, b2 being FinSequence of QuasiTerms MaxConstrSign st len b1 = len l & ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) & len b2 = len l & ( for i being Nat st i in dom l holds
b2 . i = (l /. i) -term MaxConstrSign ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines args ABCMIZ_A:def 18 :
for l being FinSequence of Vars
for b2 being FinSequence of QuasiTerms MaxConstrSign holds
( b2 = args l iff ( len b2 = len l & ( for i being Nat st i in dom l holds
b2 . i = (l /. i) -term MaxConstrSign ) ) );

definition
let c be Element of Constructors ;
func base_exp_of c -> expression equals :: ABCMIZ_A:def 19
(@ c) -trm (args (loci_of c));
coherence
(@ c) -trm (args (loci_of c)) is expression ;
end;

:: deftheorem defines base_exp_of ABCMIZ_A:def 19 :
for c being Element of Constructors holds base_exp_of c = (@ c) -trm (args (loci_of c));

theorem Th42: :: ABCMIZ_A:42
for o being OperSymbol of MaxConstrSign holds
( o is constructor iff o in Constructors )
proof end;

theorem :: ABCMIZ_A:43
for m being nullary OperSymbol of MaxConstrSign holds main-constr (m term) = m
proof end;

theorem :: ABCMIZ_A:44
for m being constructor unary OperSymbol of MaxConstrSign
for t being quasi-term holds main-constr (m term t) = m
proof end;

theorem :: ABCMIZ_A:45
for a being quasi-adjective holds main-constr ((non_op MaxConstrSign) term a) = non_op
proof end;

theorem :: ABCMIZ_A:46
for m being constructor binary OperSymbol of MaxConstrSign
for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m
proof end;

theorem :: ABCMIZ_A:47
for q being expression of MaxConstrSign , a_Type MaxConstrSign
for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *
proof end;

definition
let T be quasi-type;
func constrs T -> set equals :: ABCMIZ_A:def 20
(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } );
coherence
(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ) is set ;
end;

:: deftheorem defines constrs ABCMIZ_A:def 20 :
for T being quasi-type holds constrs T = (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } );

theorem :: ABCMIZ_A:48
for q being pure expression of MaxConstrSign , a_Type MaxConstrSign
for A being finite Subset of (QuasiAdjs MaxConstrSign) holds constrs (A ast q) = (constrs q) \/ (union { (constrs a) where a is quasi-adjective : a in A } )
proof end;

theorem :: ABCMIZ_A:49
for a being quasi-adjective
for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T)
proof end;

begin

definition
let C be initialized ConstructorSignature;
let t, p be expression of C;
pred t matches_with p means :: ABCMIZ_A:def 21
 ex f being valuation of C st t = p at f;
reflexivity
for t being expression of C ex f being valuation of C st t = t at f
proof end;
end;

:: deftheorem defines matches_with ABCMIZ_A:def 21 :
for C being initialized ConstructorSignature
for t, p being expression of C holds
( t matches_with p iff ex f being valuation of C st t = p at f );

theorem :: ABCMIZ_A:50
for C being initialized ConstructorSignature
for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds
t1 matches_with t3
proof end;

definition
let C be initialized ConstructorSignature;
let A, B be Subset of (QuasiAdjs C);
pred A matches_with B means :: ABCMIZ_A:def 22
 ex f being valuation of C st B at f c= A;
reflexivity
for A being Subset of (QuasiAdjs C) ex f being valuation of C st A at f c= A
proof end;
end;

:: deftheorem defines matches_with ABCMIZ_A:def 22 :
for C being initialized ConstructorSignature
for A, B being Subset of (QuasiAdjs C) holds
( A matches_with B iff ex f being valuation of C st B at f c= A );

theorem :: ABCMIZ_A:51
for C being initialized ConstructorSignature
for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds
A1 matches_with A3
proof end;

definition
let C be initialized ConstructorSignature;
let T, P be quasi-type of C;
pred T matches_with P means :: ABCMIZ_A:def 23
 ex f being valuation of C st
( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T );
reflexivity
for T being quasi-type of C ex f being valuation of C st
( (adjs T) at f c= adjs T & (the_base_of T) at f = the_base_of T )
proof end;
end;

:: deftheorem defines matches_with ABCMIZ_A:def 23 :
for C being initialized ConstructorSignature
for T, P being quasi-type of C holds
( T matches_with P iff ex f being valuation of C st
( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T ) );

theorem :: ABCMIZ_A:52
for C being initialized ConstructorSignature
for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds
T1 matches_with T3
proof end;

definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
let f be valuation of C;
pred f unifies t1,t2 means :Def24: :: ABCMIZ_A:def 24
t1 at f = t2 at f;
end;

:: deftheorem Def24 defines unifies ABCMIZ_A:def 24 :
for C being initialized ConstructorSignature
for t1, t2 being expression of C
for f being valuation of C holds
( f unifies t1,t2 iff t1 at f = t2 at f );

theorem Th53: :: ABCMIZ_A:53
for C being initialized ConstructorSignature
for t1, t2 being expression of C
for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
proof end;

definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
pred t1,t2 are_unifiable means :: ABCMIZ_A:def 25
 ex f being valuation of C st f unifies t1,t2;
reflexivity
for t1 being expression of C ex f being valuation of C st f unifies t1,t1
proof end;
symmetry
for t1, t2 being expression of C st ex f being valuation of C st f unifies t1,t2 holds
ex f being valuation of C st f unifies t2,t1
proof end;
end;

:: deftheorem defines are_unifiable ABCMIZ_A:def 25 :
for C being initialized ConstructorSignature
for t1, t2 being expression of C holds
( t1,t2 are_unifiable iff ex f being valuation of C st f unifies t1,t2 );

definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
pred t1,t2 are_weakly-unifiable means :: ABCMIZ_A:def 26
 ex g being one-to-one irrelevant valuation of C st
( variables_in t2 c= dom g & t1,t2 at g are_unifiable );
reflexivity
for t1 being expression of C ex g being one-to-one irrelevant valuation of C st
( variables_in t1 c= dom g & t1,t1 at g are_unifiable )
proof end;
end;

:: deftheorem defines are_weakly-unifiable ABCMIZ_A:def 26 :
for C being initialized ConstructorSignature
for t1, t2 being expression of C holds
( t1,t2 are_weakly-unifiable iff ex g being one-to-one irrelevant valuation of C st
( variables_in t2 c= dom g & t1,t2 at g are_unifiable ) );

theorem :: ABCMIZ_A:54
for C being initialized ConstructorSignature
for t1, t2 being expression of C st t1,t2 are_unifiable holds
t1,t2 are_weakly-unifiable
proof end;

definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
pred t is_a_unification_of t1,t2 means :: ABCMIZ_A:def 27
 ex f being valuation of C st
( f unifies t1,t2 & t = t1 at f );
end;

:: deftheorem defines is_a_unification_of ABCMIZ_A:def 27 :
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_unification_of t1,t2 iff ex f being valuation of C st
( f unifies t1,t2 & t = t1 at f ) );

theorem :: ABCMIZ_A:55
for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
t is_a_unification_of t2,t1
proof end;

theorem :: ABCMIZ_A:56
for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
( t matches_with t1 & t matches_with t2 )
proof end;

definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
pred t is_a_general-unification_of t1,t2 means :: ABCMIZ_A:def 28
( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds
u matches_with t ) );
end;

:: deftheorem defines is_a_general-unification_of ABCMIZ_A:def 28 :
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_general-unification_of t1,t2 iff ( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds
u matches_with t ) ) );

begin

theorem Th57: :: ABCMIZ_A:57
for n being Nat
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n
proof end;

theorem Th58: :: ABCMIZ_A:58
for l being quasi-loci
for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
proof end;

theorem Th59: :: ABCMIZ_A:59
for X being finite Subset of Vars st varcl X = X holds
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
proof end;

definition
let d be PartFunc of Vars,QuasiTypes;
attr d is even means :Def29: :: ABCMIZ_A:def 29
 for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x;
end;

:: deftheorem Def29 defines even ABCMIZ_A:def 29 :
for d being PartFunc of Vars,QuasiTypes holds
( d is even iff for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x );

definition
let l be quasi-loci;
mode type-distribution of l -> PartFunc of Vars,QuasiTypes means :Def30: :: ABCMIZ_A:def 30
( dom it = rng l & it is even );
existence
ex b1 being PartFunc of Vars,QuasiTypes st
( dom b1 = rng l & b1 is even )
proof end;
end;

:: deftheorem Def30 defines type-distribution ABCMIZ_A:def 30 :
for l being quasi-loci
for b2 being PartFunc of Vars,QuasiTypes holds
( b2 is type-distribution of l iff ( dom b2 = rng l & b2 is even ) );

theorem :: ABCMIZ_A:60
for l being empty quasi-loci holds {} is type-distribution of l
proof end;