:: by Grzegorz Bancerek

::

:: Received November 20, 2009

:: Copyright (c) 2009-2017 Association of Mizar Users

scheme :: ABCMIZ_A:sch 1

MinimalElement{ F_{1}() -> non empty finite set , P_{1}[ set , set ] } :

provided

MinimalElement{ F

provided

A1:
for x, y being set st x in F_{1}() & y in F_{1}() & P_{1}[x,y] holds

not P_{1}[y,x]
and

A2: for x, y, z being set st x in F_{1}() & y in F_{1}() & z in F_{1}() & P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

not P

A2: for x, y, z being set st x in F

P

proof end;

scheme :: ABCMIZ_A:sch 3

Numeration{ F_{1}() -> finite set , P_{1}[ set , set ] } :

Numeration{ F

ex s being one-to-one FinSequence st

( rng s = F_{1}() & ( for i, j being Nat st i in dom s & j in dom s & P_{1}[s . i,s . j] holds

i < j ) )

provided( rng s = F

i < j ) )

A1:
for x, y being set st x in F_{1}() & y in F_{1}() & P_{1}[x,y] holds

not P_{1}[y,x]
and

A2: for x, y, z being set st x in F_{1}() & y in F_{1}() & z in F_{1}() & P_{1}[x,y] & P_{1}[y,z] holds

P_{1}[x,z]

not P

A2: for x, y, z being set st x in F

P

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 )

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;

registration

ex b_{1} being quasi-loci st b_{1} is empty
by ABCMIZ_1:29;

end;

cluster empty Relation-like omega -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like for Element of QuasiLoci ;

existence ex b

definition

let C be ConstructorSignature;

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

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

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

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 )

for o being OperSymbol of C holds

( o is constructor iff o in Constructors )

proof end;

registration
end;

registration

ex b_{1} being ConstructorSignature st

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

cluster non empty non void V71() strict V150() constructor initialized standardized for ManySortedSign ;

existence ex b

( b

proof end;

definition

let C be initialized standardized ConstructorSignature;

let c be constructor OperSymbol of C;

coherence

(c `2) `1 is quasi-loci

end;
let c be constructor OperSymbol of C;

coherence

(c `2) `1 is quasi-loci

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

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;

existence

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

end;
existence

ex b

proof end;

registration

let C be initialized ConstructorSignature;

existence

ex b_{1} being constructor Subsignature of C st b_{1} is initialized

end;
existence

ex b

proof end;

registration

let C be standardized ConstructorSignature;

coherence

for b_{1} being constructor Subsignature of C holds b_{1} is standardized

end;
coherence

for b

proof 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 #)

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;

registration

let C be initialized ConstructorSignature;

not for b_{1} being quasi-term of C holds b_{1} is compound

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

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

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;

coherence

e . {} is pair

end;
let e be expression of C;

coherence

e . {} is pair

proof 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

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

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

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)

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 )

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 )

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)

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

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 )

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

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 )

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

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

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 )

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

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;

set MC = MaxConstrSign ;

definition

mode expression is expression of MaxConstrSign;

mode valuation is valuation of MaxConstrSign;

mode quasi-adjective is quasi-adjective of MaxConstrSign;

QuasiAdjs MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;

mode quasi-term is quasi-term of MaxConstrSign;

QuasiTerms MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;

mode quasi-type is quasi-type of MaxConstrSign ;

coherence

QuasiTypes MaxConstrSign is set ;

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

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;

QuasiTerms MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;

mode quasi-type is quasi-type of MaxConstrSign ;

coherence

QuasiTypes MaxConstrSign is set ;

registration

coherence

not QuasiAdjs is empty ;

coherence

not QuasiTerms is empty ;

coherence

not QuasiTypes is empty ;

end;
not QuasiAdjs is empty ;

coherence

not QuasiTerms is empty ;

coherence

not QuasiTypes is empty ;

definition

:: original: Modes

redefine func Modes -> non empty Subset of Constructors;

coherence

Modes is non empty Subset of Constructors

redefine func Attrs -> non empty Subset of Constructors;

coherence

Attrs is non empty Subset of Constructors

redefine func Funcs -> non empty Subset of Constructors;

coherence

Funcs is non empty Subset of Constructors by XBOOLE_1:7;

end;
redefine func Modes -> non empty Subset of Constructors;

coherence

Modes is non empty Subset of Constructors

proof end;

:: original: Attrsredefine func Attrs -> non empty Subset of Constructors;

coherence

Attrs is non empty Subset of Constructors

proof end;

:: original: Funcsredefine func Funcs -> non empty Subset of Constructors;

coherence

Funcs is non empty Subset of Constructors by XBOOLE_1:7;

theorem :: ABCMIZ_A:27

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 )

for l being quasi-loci holds

( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )

proof end;

theorem Th32: :: ABCMIZ_A:32

for S being non empty non void ManySortedSign

for Y being V6() ManySortedSet of the carrier of S

for X, o being set

for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & o -tree p in X holds

p is FinSequence of X

for Y being V6() ManySortedSet of the carrier of S

for X, o being set

for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (S,Y)) & 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;

existence

ex b_{1} being expression of C st b_{1} in Subtrees e
by TREES_9:11;

(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } is set ;

end;
let e be expression of C;

existence

ex b

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

(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } is set ;

:: deftheorem defines subexpression ABCMIZ_A:def 7 :

for C being initialized ConstructorSignature

for e, b_{3} being expression of C holds

( b_{3} is subexpression of e iff b_{3} in Subtrees e );

for C being initialized ConstructorSignature

for e, b

( b

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

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

definition

let S be non empty non void ManySortedSign ;

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

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

coherence

( ( e is compound implies (e . {}) `1 is set ) & ( not e is compound implies {} is set ) );

consistency

for b_{1} being set holds verum;

;

existence

ex b_{1} being DTree-yielding FinSequence st e = (e . {}) -tree b_{1}

for b_{1}, b_{2} being DTree-yielding FinSequence st e = (e . {}) -tree b_{1} & e = (e . {}) -tree b_{2} holds

b_{1} = b_{2}
by TREES_4:15;

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

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

func main-constr e -> set equals :Def9: :: ABCMIZ_A:def 9

(e . {}) `1 if e is compound

otherwise {} ;

correctness (e . {}) `1 if e is compound

otherwise {} ;

coherence

( ( e is compound implies (e . {}) `1 is set ) & ( not e is compound implies {} is set ) );

consistency

for b

;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines main-constr ABCMIZ_A:def 9 :

for S being non empty non void ManySortedSign

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

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

( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) );

for S being non empty non void ManySortedSign

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

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

( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) );

:: deftheorem ARGS defines args ABCMIZ_A:def 10 :

for S being non empty non void ManySortedSign

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

for e being Element of (Free (S,X))

for b_{4} being DTree-yielding FinSequence holds

( b_{4} = args e iff e = (e . {}) -tree b_{4} );

for S being non empty non void ManySortedSign

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

for e being Element of (Free (S,X))

for b

( b

definition

let S be non empty non void ManySortedSign ;

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

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

:: original: args

redefine func args e -> FinSequence of (Free (S,X));

coherence

args e is FinSequence of (Free (S,X))

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

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

:: original: args

redefine func args e -> FinSequence of (Free (S,X));

coherence

args e is FinSequence of (Free (S,X))

proof end;

theorem Th33: :: ABCMIZ_A:33

for C being initialized ConstructorSignature

for e being expression of C holds e is subexpression of e

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;

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

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;

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

( e is compound & main-constr e is constructor OperSymbol of C );

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

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;

coherence

for b_{1} being expression of C st b_{1} is constructor holds

b_{1} is compound
;

end;
coherence

for b

b

registration

let C be initialized ConstructorSignature;

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

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

proof end;

registration

let C be initialized ConstructorSignature;

let e be constructor expression of C;

ex b_{1} being subexpression of e st b_{1} is constructor

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

proof end;

registration

let S be non void Signature;

let X be V6() ManySortedSet of S;

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

coherence

rng t is Relation-like

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

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

coherence

rng t is Relation-like

proof end;

theorem :: ABCMIZ_A:36

for C being initialized ConstructorSignature

for e being constructor expression of C holds main-constr e in constrs e

for e being constructor expression of C holds main-constr e in constrs e

proof end;

definition

let C be non void Signature;

end;
attr C 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 & len (the_arity_of o) = n ) } is infinite ;

let o be OperSymbol of C;for n being Nat

for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ;

:: 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 & len (the_arity_of o) = n ) } is infinite );

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

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

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

for C being non void Signature

for o being OperSymbol of C holds

( o is binary iff len (the_arity_of o) = 2 );

registration

let C be ConstructorSignature;

coherence

non_op C is unary

ast C is binary

end;
coherence

non_op C is unary

proof end;

coherence ast C is binary

proof end;

registration

let C be ConstructorSignature;

coherence

for b_{1} being OperSymbol of C st b_{1} is nullary holds

b_{1} is constructor

end;
coherence

for b

b

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

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

existence

ex b_{1} being OperSymbol of a_Type C st

( b_{1} is nullary & b_{1} is constructor )

ex b_{1} being OperSymbol of an_Adj C st

( b_{1} is nullary & b_{1} is constructor )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let C be initialized ConstructorSignature;

existence

ex b_{1} being OperSymbol of C st

( b_{1} is nullary & b_{1} is constructor )

end;
existence

ex b

( b

proof end;

registration

coherence

for b_{1} being non void Signature st b_{1} is arity-rich holds

b_{1} is with_an_operation_for_each_sort

for b_{1} being ConstructorSignature st b_{1} is arity-rich holds

b_{1} is initialized

end;
for b

b

proof end;

coherence for b

b

proof end;

registration
end;

registration

existence

ex b_{1} being ConstructorSignature st

( b_{1} is arity-rich & b_{1} is initialized )

end;
ex b

( b

proof end;

registration

let C be arity-rich ConstructorSignature;

let s be SortSymbol of C;

existence

ex b_{1} being OperSymbol of s st

( b_{1} is nullary & b_{1} is constructor )

ex b_{1} being OperSymbol of s st

( b_{1} is unary & b_{1} is constructor )

ex b_{1} being OperSymbol of s st

( b_{1} is binary & b_{1} is constructor )

end;
let s be SortSymbol of C;

existence

ex b

( b

proof end;

existence ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let C be arity-rich ConstructorSignature;

existence

ex b_{1} being OperSymbol of C st

( b_{1} is unary & b_{1} is constructor )

ex b_{1} being OperSymbol of C st

( b_{1} is binary & b_{1} is constructor )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof 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

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

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

definition

let c be Element of Constructors ;

coherence

c is constructor OperSymbol of MaxConstrSign

end;
coherence

c is constructor OperSymbol of MaxConstrSign

proof end;

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

end;
:: original: @

redefine func @ m -> constructor OperSymbol of a_Type MaxConstrSign;

coherence

@ m is constructor OperSymbol of a_Type MaxConstrSign

proof end;

registration
end;

definition

({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term) is quasi-type ;

end;

func set-type -> quasi-type equals :: ABCMIZ_A:def 17

({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);

coherence ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);

({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term) is quasi-type ;

:: deftheorem defines set-type ABCMIZ_A:def 17 :

set-type = ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);

set-type = ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);

definition

let l be FinSequence of Vars ;

ex b_{1} being FinSequence of QuasiTerms MaxConstrSign st

( len b_{1} = len l & ( for i being Nat st i in dom l holds

b_{1} . i = (l /. i) -term MaxConstrSign ) )

for b_{1}, b_{2} being FinSequence of QuasiTerms MaxConstrSign st len b_{1} = len l & ( for i being Nat st i in dom l holds

b_{1} . i = (l /. i) -term MaxConstrSign ) & len b_{2} = len l & ( for i being Nat st i in dom l holds

b_{2} . i = (l /. i) -term MaxConstrSign ) holds

b_{1} = b_{2}

end;
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 ( len it = len l & ( for i being Nat st i in dom l holds

it . i = (l /. i) -term MaxConstrSign ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def18 defines args ABCMIZ_A:def 18 :

for l being FinSequence of Vars

for b_{2} being FinSequence of QuasiTerms MaxConstrSign holds

( b_{2} = args l iff ( len b_{2} = len l & ( for i being Nat st i in dom l holds

b_{2} . i = (l /. i) -term MaxConstrSign ) ) );

for l being FinSequence of Vars

for b

( b

b

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

for c being Element of Constructors holds base_exp_of c = (@ c) -trm (args (loci_of c));

theorem :: ABCMIZ_A:44

for m being constructor unary OperSymbol of MaxConstrSign

for t being quasi-term holds main-constr (m term t) = m

for t being quasi-term holds main-constr (m term t) = m

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

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

for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *

proof end;

definition

let T be quasi-type;

(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ) is set ;

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

(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ) is set ;

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

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

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)

for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T)

proof end;

definition

let C be initialized ConstructorSignature;

let t, p be expression of C;

reflexivity

for t being expression of C ex f being valuation of C st t = t at f

end;
let t, p be expression of C;

reflexivity

for t being expression of C ex f being valuation of C st t = t at f

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

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

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

reflexivity

for A being Subset of (QuasiAdjs C) ex f being valuation of C st A at f c= A

end;
let A, B be Subset of (QuasiAdjs C);

reflexivity

for A being Subset of (QuasiAdjs C) ex f being valuation of C st A at f c= A

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

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

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;

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 )

end;
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 ex f being valuation of C st

( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T );

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;

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

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

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

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

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

for t1, t2 being expression of C

for f being valuation of C st f unifies t1,t2 holds

f unifies t2,t1 ;

definition

let C be initialized ConstructorSignature;

let t1, t2 be expression of C;

reflexivity

for t1 being expression of C ex f being valuation of C st f unifies t1,t1

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

end;
let t1, t2 be expression of C;

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;

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

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;

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 )

end;
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 ex g being one-to-one irrelevant valuation of C st

( variables_in t2 c= dom g & t1,t2 at g are_unifiable );

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;

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

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

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;

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

ex f being valuation of C st

( f unifies t1,t2 & t = t1 at f );

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

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

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 )

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;

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

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

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

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

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

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

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 )

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;

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

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;

ex b_{1} being PartFunc of Vars,QuasiTypes st

( dom b_{1} = rng l & b_{1} is even )

end;
mode type-distribution of l -> PartFunc of Vars,QuasiTypes means :Def30: :: ABCMIZ_A:def 30

( dom it = rng l & it is even );

existence ( dom it = rng l & it is even );

ex b

( dom b

proof end;

:: deftheorem Def30 defines type-distribution ABCMIZ_A:def 30 :

for l being quasi-loci

for b_{2} being PartFunc of Vars,QuasiTypes holds

( b_{2} is type-distribution of l iff ( dom b_{2} = rng l & b_{2} is even ) );

for l being quasi-loci

for b

( b

:: for t1,t2 being expression of C st t1 matches_with t2

:: holds t1,t2 are_weakly-unifiable;