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

theorem :: ABCMIZ_A:1

canceled;

::$CT

scheme :: ABCMIZ_A:sch 1
MinimalElement{ F₁() -> non empty finite set , P₁[ set , set ] } :

ex x being set st
( x in F₁() & ( for y being set st y in F₁() holds
not P₁[y,x] ) )

provided

A1: for x, y being set st x in F₁() & y in F₁() & P₁[x,y] holds
not P₁[y,x] and
A2: for x, y, z being set st x in F₁() & y in F₁() & z in F₁() & P₁[x,y] & P₁[y,z] holds
P₁[x,z]

proof end;

scheme :: ABCMIZ_A:sch 2
FiniteC{ F₁() -> finite set , P₁[ set ] } :

P₁[F₁()]

provided

A1: for A being Subset of F₁() st ( for B being set st B c< A holds
P₁[B] ) holds
P₁[A]

proof end;

scheme :: ABCMIZ_A:sch 3
Numeration{ F₁() -> finite set , P₁[ set , set ] } :

ex s being one-to-one FinSequence st
( rng s = F₁() & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) )

provided

A1: for x, y being set st x in F₁() & y in F₁() & P₁[x,y] holds
not P₁[y,x] and
A2: for x, y, z being set st x in F₁() & y in F₁() & z in F₁() & P₁[x,y] & P₁[y,z] holds
P₁[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;

registration

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₁ being quasi-loci st b₁ 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 V71() strict V150() constructor initialized standardized for ManySortedSign ;

existence
ex b₁ being ConstructorSignature st
( b₁ is initialized & b₁ is standardized & b₁ 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 V150() constructor for Subsignature of C;

existence
ex b₁ being Subsignature of C st b₁ is constructor

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster non empty non void V71() V150() constructor initialized for Subsignature of C;

existence
ex b₁ being constructor Subsignature of C st b₁ is initialized

proof end;

end;

registration

let C be standardized ConstructorSignature;

cluster constructor -> constructor standardized for Subsignature of C;

coherence
for b₁ being constructor Subsignature of C holds b₁ 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 non pair Function-like finite DecoratedTree-like finite-branching non compound for expression of C, a_Term C;

existence
not for b₁ being quasi-term of C holds b₁ is compound

proof end;

end;

registration

cluster -> pair for Element of Vars ;

coherence
for b₁ being Element of Vars holds b₁ 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;

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

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

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 b₁ being expression of C st b₁ 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 ;

end;

:: deftheorem defines subexpression ABCMIZ_A:def 7 :
for C being initialized ConstructorSignature
for e, b₃ being expression of C holds
( b₃ is subexpression of e iff b₃ 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 } ;

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

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 b₁ being set holds verum;
;

:: x-term C = [x, a_Term]-tree {}
:: (ast C)term(a,t) = [*, the carrier of C]-tree<*a,t*>
:: (non_op C)term a = [non_op, the carrier of C]-tree<*a*>
:: c-trm p = [c, the carrier of C]-tree p
:: problem gdy '{}' moze byc 'c'

func args e -> DTree-yielding FinSequence means :ARGS: :: ABCMIZ_A:def 10
e = (e . {}) -tree it;

existence
ex b₁ being DTree-yielding FinSequence st e = (e . {}) -tree b₁

proof end;

uniqueness
for b₁, b₂ being DTree-yielding FinSequence st e = (e . {}) -tree b₁ & e = (e . {}) -tree b₂ holds
b₁ = b₂ by TREES_4:15;

end;

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

:: 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₄ being DTree-yielding FinSequence holds
( b₄ = args e iff e = (e . {}) -tree 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))

proof end;

end;

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 for Element of Union the Sorts of (Free (C,(MSVars C)));

coherence
for b₁ being expression of C st b₁ is constructor holds
b₁ is compound ;

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 b₁ being expression of C st b₁ is constructor

proof end;

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 b₁ being subexpression of e st b₁ 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;

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

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

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

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 for Element of the carrier' of C;

coherence
for b₁ being OperSymbol of C st b₁ is nullary holds
b₁ 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 for OperSymbol of a_Type C;

existence
ex b₁ being OperSymbol of a_Type C st
( b₁ is nullary & b₁ is constructor )

proof end;

cluster constructor nullary for OperSymbol of an_Adj C;

existence
ex b₁ being OperSymbol of an_Adj C st
( b₁ is nullary & b₁ is constructor )

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster constructor nullary for Element of the carrier' of C;

existence
ex b₁ being OperSymbol of C st
( b₁ is nullary & b₁ is constructor )

proof end;

end;

registration

cluster non void V150() arity-rich -> non void with_an_operation_for_each_sort for ManySortedSign ;

coherence
for b₁ being non void Signature st b₁ is arity-rich holds
b₁ is with_an_operation_for_each_sort

proof end;

cluster V150() constructor arity-rich -> initialized for ManySortedSign ;

coherence
for b₁ being ConstructorSignature st b₁ is arity-rich holds
b₁ is initialized

proof end;

end;

registration

cluster MaxConstrSign -> arity-rich ;

coherence
MaxConstrSign is arity-rich

proof end;

end;

registration

cluster non empty non void V71() V150() constructor initialized arity-rich for ManySortedSign ;

existence
ex b₁ being ConstructorSignature st
( b₁ is arity-rich & b₁ is initialized )

proof end;

end;

registration

let C be arity-rich ConstructorSignature;
let s be SortSymbol of C;

cluster constructor nullary for OperSymbol of s;

existence
ex b₁ being OperSymbol of s st
( b₁ is nullary & b₁ is constructor )

proof end;

cluster constructor unary for OperSymbol of s;

existence
ex b₁ being OperSymbol of s st
( b₁ is unary & b₁ is constructor )

proof end;

cluster constructor binary for OperSymbol of s;

existence
ex b₁ being OperSymbol of s st
( b₁ is binary & b₁ is constructor )

proof end;

end;

registration

let C be arity-rich ConstructorSignature;

cluster constructor unary for Element of the carrier' of C;

existence
ex b₁ being OperSymbol of C st
( b₁ is unary & b₁ is constructor )

proof end;

cluster constructor binary for Element of the carrier' of C;

existence
ex b₁ being OperSymbol of C st
( b₁ is binary & b₁ 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 ) ;

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 b₁ being FinSequence of QuasiTerms MaxConstrSign st
( len b₁ = len l & ( for i being Nat st i in dom l holds
b₁ . i = (l /. i) -term MaxConstrSign ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of QuasiTerms MaxConstrSign st len b₁ = len l & ( for i being Nat st i in dom l holds
b₁ . i = (l /. i) -term MaxConstrSign ) & len b₂ = len l & ( for i being Nat st i in dom l holds
b₂ . i = (l /. i) -term MaxConstrSign ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines args ABCMIZ_A:def 18 :
for l being FinSequence of Vars
for b₂ being FinSequence of QuasiTerms MaxConstrSign holds
( b₂ = args l iff ( len b₂ = len l & ( for i being Nat st i in dom l holds
b₂ . 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 } ) ;

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;

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;

:: Unification of Mizar terms

pred f unifies t1,t2 means :: ABCMIZ_A:def 24
t1 at f = t2 at f;

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

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 ;

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

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

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 :: 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 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 b₁ being PartFunc of Vars,QuasiTypes st
( dom b₁ = rng l & b₁ is even )

proof end;

end;

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

theorem :: ABCMIZ_A:60

for l being empty quasi-loci holds {} is type-distribution of l

proof end;