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


begin

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

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]
proofend;

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]
proofend;

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

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

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

begin

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

definition
let C be ConstructorSignature;
attrC is standardized  means :Def1: :: ABCMIZ_A:def 1
 for o being OperSymbol of C st o is constructor holds
( o in Constructors &amp; o `1 = the_result_sort_of o &amp; 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 &amp; o `1 = the_result_sort_of o &amp; 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 )
proofend;

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

registration
cluster non empty non void V68() strict V146() constructor initialized standardized for ManySortedSign ;
existence
 ex b1 being ConstructorSignature st
( b1 is initialized &amp; b1 is standardized &amp; b1 is strict )
proofend;
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
proofend;
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;
clusterV146() constructor for Subsignature of C;
existence
 ex b1 being Subsignature of C st b1 is constructor
proofend;
end;

registration
let C be initialized ConstructorSignature;
cluster non empty non void V68() V146() constructor initialized for Subsignature of C;
existence
 ex b1 being constructor Subsignature of C st b1 is initialized
proofend;
end;

registration
let C be standardized ConstructorSignature;
cluster constructor  ->  constructor standardized for Subsignature of C;
coherence
 for b1 being constructor Subsignature of C holds b1 is standardized
proofend;
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 #)
proofend;

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

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

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

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

theorem Th8: :: ABCMIZ_A:8
Vars misses Constructors
proofend;

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

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

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 &amp; e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] &amp; ( o in Constructors or o = * or o = non_op ) ) )
proofend;

registration
let C be initialized standardized ConstructorSignature;
let e be expression of C;
clustere . {} ->  pair ;
coherence
 e . {} is pair
proofend;
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
proofend;

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 ) &amp; ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
proofend;

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

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

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

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 &amp; e = x -term C )
proofend;

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

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

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 &amp; the_result_sort_of o = o `1 &amp; e is expression of C, the_result_sort_of o )
proofend;

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 &amp; ((t . {}) `1) `1 = a_Term ) )
proofend;

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

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 &amp; ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
proofend;

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 &amp; ((a . {}) `1) `1 = an_Adj ) )
proofend;

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

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 &amp; ((t . {}) `1) `1 = a_Type ) )
proofend;

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
proofend;
:: original:Attrs
redefine func Attrs  ->  non empty Subset of Constructors;
coherence
 Attrs is non empty Subset of Constructors
proofend;
:: 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
proofend;
end;

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

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

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

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

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

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

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))) &amp; o -tree p in X holds
p is FinSequence of X
proofend;

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:11;
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 ) &amp; ( 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
proofend;
uniqueness
 for b1, b2 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 &amp; 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 ) &amp; ( 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
proofend;

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

definition
let C be initialized ConstructorSignature;
let e be expression of C;
attre is constructor  means :Def11: :: ABCMIZ_A:def 11
( e is compound &amp; 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 &amp; main-constr e is constructor OperSymbol of C ) );

registration
let C be initialized ConstructorSignature;
cluster constructor  ->  compound for 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 non pair Function-like finite DecoratedTree-like finite-branching constructor for Element of Union the Sorts of (Free (C,(MSVars C)));
existence
 ex b1 being expression of C st b1 is constructor
proofend;
end;

registration
let C be initialized ConstructorSignature;
let e be constructor expression of C;
cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching constructor for subexpression of e;
existence
 ex b1 being subexpression of e st b1 is constructor
proofend;
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
proofend;
end;

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

begin

definition
let C be non void Signature;
attrC is arity-rich  means :Def12: :: ABCMIZ_A:def 12
 for n being Nat
for s being SortSymbol of C holds  {  o where o is OperSymbol of C : ( the_result_sort_of o = s &amp; len (the_arity_of o) = n )  }  is infinite ;
let o be OperSymbol of C;
attro is nullary  means :Def13: :: ABCMIZ_A:def 13
 the_arity_of o = {} ;
attro is unary  means :Def14: :: ABCMIZ_A:def 14
 len (the_arity_of o) = 1;
attro 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  {  o where o is OperSymbol of C : ( the_result_sort_of o = s &amp; len (the_arity_of o) = n )  }  is infinite );

:: 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 ) &amp; ( o is nullary implies not o is binary ) &amp; ( o is unary implies not o is binary ) )
proofend;

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

registration
let C be ConstructorSignature;
cluster nullary  ->  constructor for Element of the carrier' of C;
coherence
 for b1 being OperSymbol of C st b1 is nullary holds
b1 is constructor
proofend;
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 &amp; a is nullary ) )
proofend;

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

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

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

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

registration
cluster non empty non void V68() V146() constructor initialized arity-rich for ManySortedSign ;
existence
 ex b1 being ConstructorSignature st
( b1 is arity-rich &amp; b1 is initialized )
proofend;
end;

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

registration
let C be arity-rich ConstructorSignature;
cluster constructor unary for Element of the carrier' of C;
existence
 ex b1 being OperSymbol of C st
( b1 is unary &amp; b1 is constructor )
proofend;
cluster constructor binary for Element of the carrier' of C;
existence
 ex b1 being OperSymbol of C st
( b1 is binary &amp; b1 is constructor )
proofend;
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
proofend;

definition
let C be initialized ConstructorSignature;
let m be constructor nullary OperSymbol of a_Type C;
:: original:term
redefine funcm term  ->  pure expression of C, a_Type C;
coherence
 m term is pure expression of C, a_Type C
proofend;
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
proofend;
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
proofend;
end;

registration
cluster @ set-constr ->  constructor nullary ;
coherence
 @ set-constr is nullary
proofend;
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 = {} &amp; 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 &amp; ( 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 &amp; ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of QuasiTerms MaxConstrSign st len b1 = len l &amp; ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) &amp; len b2 = len l &amp; ( for i being Nat st i in dom l holds
b2 . i = (l /. i) -term MaxConstrSign ) holds
b1 = b2
proofend;
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 &amp; ( 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 )
proofend;

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

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

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

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

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)) = *
proofend;

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

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

begin

definition
let C be initialized ConstructorSignature;
let t, p be expression of C;
predt 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
proofend;
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 &amp; t2 matches_with t3 holds
t1 matches_with t3
proofend;

definition
let C be initialized ConstructorSignature;
let A, B be Subset of (QuasiAdjs C);
predA 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
proofend;
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 &amp; A2 matches_with A3 holds
A1 matches_with A3
proofend;

definition
let C be initialized ConstructorSignature;
let T, P be quasi-type of C;
predT matches_with P means :: ABCMIZ_A:def 23
 ex f being valuation of C st
( (adjs P) at f c= adjs T &amp; (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 &amp; (the_base_of T) at f = the_base_of T )
proofend;
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 &amp; (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 &amp; T2 matches_with T3 holds
T1 matches_with T3
proofend;

definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
let f be valuation of C;
:: [WP: ] Unification_of_Mizar_terms
predf 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
proofend;

definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
predt1,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
proofend;
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
proofend;
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;
predt1,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 &amp; 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 &amp; t1,t1 at g are_unifiable )
proofend;
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 &amp; t1,t2 at g are_unifiable ) );

:: theorem
:: for t1,t2 being expression of C st t1 matches_with t2
:: holds t1,t2 are_weakly-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
proofend;

definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
predt is_a_unification_of t1,t2 means :: ABCMIZ_A:def 27
 ex f being valuation of C st
( f unifies t1,t2 &amp; 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 &amp; 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
proofend;

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 &amp; t matches_with t2 )
proofend;

definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
predt is_a_general-unification_of t1,t2 means :: ABCMIZ_A:def 28
( t is_a_unification_of t1,t2 &amp; ( 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 &amp; ( 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
proofend;

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

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) &amp; vars (m -trm p) = X )
proofend;

definition
let d be PartFunc of Vars,QuasiTypes;
attrd is even  means :Def29: :: ABCMIZ_A:def 29
 for x being variable
for T being quasi-type st x in dom d &amp; 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 &amp; 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 &amp; it is even );
existence
 ex b1 being PartFunc of Vars,QuasiTypes st
( dom b1 = rng l &amp; b1 is even )
proofend;
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 &amp; b2 is even ) );

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