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

theorem Th1: :: ABCMIZ_1:1

for x being set
for f being Function holds f . x c= Union f

proof end;

theorem :: ABCMIZ_1:2

for x being set
for f being Function st Union f = {} holds
f . x = {} by Th1, XBOOLE_1:3;

theorem Th3: :: ABCMIZ_1:3

for f being Function
for x, y being object st f = [x,y] holds
x = y

proof end;

theorem Th4: :: ABCMIZ_1:4

for X, Y being set holds (id X) .: Y c= Y

proof end;

theorem Th5: :: ABCMIZ_1:5

for S being non void Signature
for X being V8() ManySortedSet of the carrier of S
for t being Term of S,X holds not t is pair

proof end;

registration

let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;

cluster -> non pair for Element of Union the Sorts of (Free (S,X));

coherence
for b₁ being Element of (Free (S,X)) holds not b₁ is pair

proof end;

end;

theorem Th6: :: ABCMIZ_1:6

for x, y, z being set st x in {z} * & y in {z} * & card x = card y holds
x = y

proof end;

definition

let S be non void Signature;
let A be MSAlgebra over S;
mode Subset of A is Subset of (Union the Sorts of A);
mode FinSequence of A is FinSequence of Union the Sorts of A;

end;

registration

let S be non void Signature;
let X be V9() ManySortedSet of S;

cluster -> DTree-yielding for FinSequence of Union the Sorts of (Free (S,X));

coherence
for b₁ being FinSequence of (Free (S,X)) holds b₁ is DTree-yielding

proof end;

end;

theorem Th7: :: ABCMIZ_1:7

for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )

proof end;

definition

let A be set ;

func varcl A -> set means :Def1: :: ABCMIZ_1:def 1
( A c= it & ( for x, y being set st [x,y] in it holds
x c= it ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
it c= B ) );

uniqueness
for b₁, b₂ being set st A c= b₁ & ( for x, y being set st [x,y] in b₁ holds
x c= b₁ ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₁ c= B ) & A c= b₂ & ( for x, y being set st [x,y] in b₂ holds
x c= b₂ ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₂ c= B ) holds
b₁ = b₂

proof end;

existence
ex b₁ being set st
( A c= b₁ & ( for x, y being set st [x,y] in b₁ holds
x c= b₁ ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₁ c= B ) )

proof end;

projectivity
for b₁, b₂ being set st b₂ c= b₁ & ( for x, y being set st [x,y] in b₁ holds
x c= b₁ ) & ( for B being set st b₂ c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₁ c= B ) holds
( b₁ c= b₁ & ( for x, y being set st [x,y] in b₁ holds
x c= b₁ ) & ( for B being set st b₁ c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
b₁ c= B ) ) ;

end;

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

theorem Th8: :: ABCMIZ_1:8

varcl {} = {}

proof end;

theorem Th9: :: ABCMIZ_1:9

for A, B being set st A c= B holds
varcl A c= varcl B

proof end;

theorem Th10: :: ABCMIZ_1:10

for A being set holds varcl (union A) = union { (varcl a) where a is Element of A : verum }

proof end;

scheme :: ABCMIZ_1:sch 1
Sch14{ F₁() -> set , F₂( set ) -> set , P₁[ set ] } :

varcl (union { F₂(z) where z is Element of F₁() : P₁[z] } ) = union { (varcl F₂(z)) where z is Element of F₁() : P₁[z] }

proof end;

theorem Th11: :: ABCMIZ_1:11

for X, Y being set holds varcl (X \/ Y) = (varcl X) \/ (varcl Y)

proof end;

theorem Th12: :: ABCMIZ_1:12

for A being non empty set st ( for a being Element of A holds varcl a = a ) holds
varcl (meet A) = meet A

proof end;

theorem Th13: :: ABCMIZ_1:13

for X, Y being set holds varcl ((varcl X) /\ (varcl Y)) = (varcl X) /\ (varcl Y)

proof end;

registration

let A be empty set ;

cluster varcl A -> empty ;

coherence
varcl A is empty by Th8;

end;

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

definition

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

existence
ex b₁ being set ex V being ManySortedSet of NAT st
( b₁ = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) )

proof end;

uniqueness
for b₁, b₂ being set st ex V being ManySortedSet of NAT st
( b₁ = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) & ex V being ManySortedSet of NAT st
( b₂ = Union V & V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) ) holds
b₁ = b₂

proof end;

end;

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

theorem Th14: :: ABCMIZ_1:14

for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds
for i, j being Element of NAT st i <= j holds
V . i c= V . j

proof end;

theorem Th15: :: ABCMIZ_1:15

for V being ManySortedSet of NAT st V . 0 = { [{},i] where i is Element of NAT : verum } & ( for n being Nat holds V . (n + 1) = { [(varcl A),j] where A is Subset of (V . n), j is Element of NAT : A is finite } ) holds
for A being finite Subset of Vars ex i being Element of NAT st A c= V . i

proof end;

theorem Th16: :: ABCMIZ_1:16

{ [{},i] where i is Element of NAT : verum } c= Vars

proof end;

theorem Th17: :: ABCMIZ_1:17

for A being finite Subset of Vars
for i being Nat holds [(varcl A),i] in Vars

proof end;

theorem Th18: :: ABCMIZ_1:18

Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite }

proof end;

theorem Th19: :: ABCMIZ_1:19

varcl Vars = Vars

proof end;

theorem Th20: :: ABCMIZ_1:20

for X being set st the_rank_of X is finite holds
X is finite

proof end;

theorem Th21: :: ABCMIZ_1:21

for X being set holds the_rank_of (varcl X) = the_rank_of X

proof end;

theorem Th22: :: ABCMIZ_1:22

for X being finite Subset of (Rank omega) holds X in Rank omega

proof end;

theorem Th23: :: ABCMIZ_1:23

Vars c= Rank omega

proof end;

theorem Th24: :: ABCMIZ_1:24

for A being finite Subset of Vars holds varcl A is finite Subset of Vars

proof end;

registration

cluster Vars -> non empty ;

correctness
coherence
not Vars is empty ;

proof end;

end;

definition

mode variable is Element of Vars ;

end;

registration

let x be variable;

cluster vars x -> finite for set ;

coherence
for b₁ being set st b₁ = x `1 holds
b₁ is finite

proof end;

end;

notation

let x be variable;
synonym vars x for x `1 ;

end;

definition

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

proof end;

end;

theorem :: ABCMIZ_1:25

for i being Nat holds [{},i] in Vars

proof end;

theorem Th26: :: ABCMIZ_1:26

for j being Element of NAT
for A being Subset of Vars holds varcl {[(varcl A),j]} = (varcl A) \/ {[(varcl A),j]}

proof end;

theorem Th27: :: ABCMIZ_1:27

for x being variable holds varcl {x} = (vars x) \/ {x}

proof end;

theorem :: ABCMIZ_1:28

for i being Nat
for x being variable holds [((vars x) \/ {x}),i] in Vars

proof end;

notation

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

end;

definition

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

existence
ex b₁ being FinSequenceSet of Vars st
for p being FinSequence of Vars holds
( p in b₁ iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being FinSequenceSet of Vars st ( for p being FinSequence of Vars holds
( p in b₁ iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) ) & ( for p being FinSequence of Vars holds
( p in b<sub>2</sub> iff ( p is one-to-one & ( for i being Nat st i in dom p holds
(p . i) `1 c= rng (p dom i) ) ) ) ) holds
b₁ = b₂;

proof end;

end;

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

theorem Th29: :: ABCMIZ_1:29

<*> Vars in QuasiLoci

proof end;

registration

cluster QuasiLoci -> non empty ;

correctness
coherence
not QuasiLoci is empty ;
by Th29;

end;

definition

mode quasi-loci is Element of QuasiLoci ;

end;

registration

cluster -> one-to-one for Element of QuasiLoci ;

coherence
for b₁ being quasi-loci holds b₁ is one-to-one by Def3;

end;

theorem Th30: :: ABCMIZ_1:30

for l being one-to-one FinSequence of Vars holds
( l is quasi-loci iff for i being Nat
for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) )

proof end;

theorem Th31: :: ABCMIZ_1:31

for l being quasi-loci
for x being variable holds
( l ^ <*x*> is quasi-loci iff ( not x in rng l & vars x c= rng l ) )

proof end;

theorem Th32: :: ABCMIZ_1:32

for p, q being FinSequence st p ^ q is quasi-loci holds
( p is quasi-loci & q is FinSequence of Vars )

proof end;

theorem :: ABCMIZ_1:33

for l being quasi-loci holds varcl (rng l) = rng l

proof end;

theorem Th34: :: ABCMIZ_1:34

for x being variable holds
( <*x*> is quasi-loci iff vars x = {} )

proof end;

theorem Th35: :: ABCMIZ_1:35

for x, y being variable holds
( <*x,y*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} ) )

proof end;

theorem :: ABCMIZ_1:36

for x, y, z being variable holds
( <*x,y,z*> is quasi-loci iff ( vars x = {} & x <> y & vars y c= {x} & x <> z & y <> z & vars z c= {x,y} ) )

proof end;

definition

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

proof end;

end;

definition

func a_Type -> set equals :: ABCMIZ_1:def 4
0 ;

coherence
0 is set ;

func an_Adj -> set equals :: ABCMIZ_1:def 5
1;

coherence
1 is set ;

func a_Term -> set equals :: ABCMIZ_1:def 6
2;

coherence
2 is set ;

func * -> set equals :: ABCMIZ_1:def 7
0 ;

coherence
0 is set ;

func non_op -> set equals :: ABCMIZ_1:def 8
1;

coherence
1 is set ;

end;

:: deftheorem defines a_Type ABCMIZ_1:def 4 :
a_Type = 0 ;

:: deftheorem defines an_Adj ABCMIZ_1:def 5 :
an_Adj = 1;

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

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

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

definition

let C be Signature;

attr C is constructor means :Def9: :: ABCMIZ_1:def 9
( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds
the Arity of C . o in {a_Term} * ) );

end;

:: deftheorem Def9 defines constructor ABCMIZ_1:def 9 :
for C being Signature holds
( C is constructor iff ( the carrier of C = {a_Type,an_Adj,a_Term} & {*,non_op} c= the carrier' of C & the Arity of C . * = <*an_Adj,a_Type*> & the Arity of C . non_op = <*an_Adj*> & the ResultSort of C . * = a_Type & the ResultSort of C . non_op = an_Adj & ( for o being Element of the carrier' of C st o <> * & o <> non_op holds
the Arity of C . o in {a_Term} * ) ) );

registration

cluster V265() constructor -> non empty non void for ManySortedSign ;

coherence
for b₁ being Signature st b₁ is constructor holds
( not b₁ is empty & not b₁ is void ) ;

end;

definition

func MinConstrSign -> strict Signature means :Def10: :: ABCMIZ_1:def 10
( it is constructor & the carrier' of it = {*,non_op} );

existence
ex b₁ being strict Signature st
( b₁ is constructor & the carrier' of b₁ = {*,non_op} )

proof end;

correctness
uniqueness
for b₁, b₂ being strict Signature st b₁ is constructor & the carrier' of b₁ = {*,non_op} & b₂ is constructor & the carrier' of b₂ = {*,non_op} holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :
for b₁ being strict Signature holds
( b₁ = MinConstrSign iff ( b₁ is constructor & the carrier' of b₁ = {*,non_op} ) );

registration

cluster MinConstrSign -> strict constructor ;

coherence
MinConstrSign is constructor by Def10;

end;

registration

cluster strict V265() constructor for ManySortedSign ;

existence
ex b₁ being Signature st
( b₁ is constructor & b₁ is strict )

proof end;

end;

definition

mode ConstructorSignature is constructor Signature;

end;

:: theorem ::?
:: for C being ConstructorSignature holds the carrier of C = 3
:: by CONSTRSIGN,YELLOW11:1;

definition

let C be ConstructorSignature;
let o be OperSymbol of C;

attr o is constructor means :Def11: :: ABCMIZ_1:def 11
( o <> * & o <> non_op );

end;

:: deftheorem Def11 defines constructor ABCMIZ_1:def 11 :
for C being ConstructorSignature
for o being OperSymbol of C holds
( o is constructor iff ( o <> * & o <> non_op ) );

theorem :: ABCMIZ_1:37

for S being ConstructorSignature
for o being OperSymbol of S st o is constructor holds
the_arity_of o = (len (the_arity_of o)) |-> a_Term

proof end;

definition

let C be non empty non void Signature;

attr C is initialized means :Def12: :: ABCMIZ_1:def 12
ex m, a being OperSymbol of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} );

end;

:: deftheorem Def12 defines initialized ABCMIZ_1:def 12 :
for C being non empty non void Signature holds
( C is initialized iff ex m, a being OperSymbol of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) );

definition

let C be ConstructorSignature;
A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

func a_Type C -> SortSymbol of C equals :: ABCMIZ_1:def 13
a_Type ;

coherence
a_Type is SortSymbol of C by A1, ENUMSET1:def 1;

func an_Adj C -> SortSymbol of C equals :: ABCMIZ_1:def 14
an_Adj ;

coherence
an_Adj is SortSymbol of C by A1, ENUMSET1:def 1;

func a_Term C -> SortSymbol of C equals :: ABCMIZ_1:def 15
a_Term ;

coherence
a_Term is SortSymbol of C by A1, ENUMSET1:def 1;
A2: {*,non_op} c= the carrier' of C by Def9;
A3: * in {*,non_op} by TARSKI:def 2;
A4: non_op in {*,non_op} by TARSKI:def 2;

func non_op C -> OperSymbol of C equals :: ABCMIZ_1:def 16
non_op ;

coherence
non_op is OperSymbol of C by A2, A4;

func ast C -> OperSymbol of C equals :: ABCMIZ_1:def 17
* ;

coherence
* is OperSymbol of C by A2, A3;

end;

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

:: deftheorem defines an_Adj ABCMIZ_1:def 14 :
for C being ConstructorSignature holds an_Adj C = an_Adj ;

:: deftheorem defines a_Term ABCMIZ_1:def 15 :
for C being ConstructorSignature holds a_Term C = a_Term ;

:: deftheorem defines non_op ABCMIZ_1:def 16 :
for C being ConstructorSignature holds non_op C = non_op ;

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

theorem :: ABCMIZ_1:38

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

definition

func Modes -> set equals :: ABCMIZ_1:def 18
[:{a_Type},[:QuasiLoci,NAT:]:];

correctness
coherence
[:{a_Type},[:QuasiLoci,NAT:]:] is set ;
;

func Attrs -> set equals :: ABCMIZ_1:def 19
[:{an_Adj},[:QuasiLoci,NAT:]:];

correctness
coherence
[:{an_Adj},[:QuasiLoci,NAT:]:] is set ;
;

func Funcs -> set equals :: ABCMIZ_1:def 20
[:{a_Term},[:QuasiLoci,NAT:]:];

correctness
coherence
[:{a_Term},[:QuasiLoci,NAT:]:] is set ;
;

end;

:: deftheorem defines Modes ABCMIZ_1:def 18 :
Modes = [:{a_Type},[:QuasiLoci,NAT:]:];

:: deftheorem defines Attrs ABCMIZ_1:def 19 :
Attrs = [:{an_Adj},[:QuasiLoci,NAT:]:];

:: deftheorem defines Funcs ABCMIZ_1:def 20 :
Funcs = [:{a_Term},[:QuasiLoci,NAT:]:];

registration

cluster Modes -> non empty ;

coherence
not Modes is empty ;

cluster Attrs -> non empty ;

coherence
not Attrs is empty ;

cluster Funcs -> non empty ;

coherence
not Funcs is empty ;

end;

definition

func Constructors -> non empty set equals :: ABCMIZ_1:def 21
(Modes \/ Attrs) \/ Funcs;

coherence
(Modes \/ Attrs) \/ Funcs is non empty set ;

end;

:: deftheorem defines Constructors ABCMIZ_1:def 21 :
Constructors = (Modes \/ Attrs) \/ Funcs;

theorem :: ABCMIZ_1:39

{*,non_op} misses Constructors

proof end;

definition

let x be Element of [:QuasiLoci,NAT:];
:: original: vars
redefine func x `1 -> quasi-loci;
coherence
vars x is quasi-loci by MCART_1:10;
:: original: the_base_of
redefine func x `2 -> Element of NAT ;
coherence
the_base_of is Element of NAT by MCART_1:10;

end;

notation

let c be Element of Constructors ;
synonym kind_of c for c `1 ;

end;

definition

let c be Element of Constructors ;
:: original: vars
redefine func kind_of c -> Element of {a_Type,an_Adj,a_Term};
coherence
vars c is Element of {a_Type,an_Adj,a_Term}

proof end;

:: original: the_base_of
redefine func c `2 -> Element of [:QuasiLoci,NAT:];
coherence
the_base_of is Element of [:QuasiLoci,NAT:]

proof end;

end;

definition

let c be Element of Constructors ;

func loci_of c -> quasi-loci equals :: ABCMIZ_1:def 22
(c `2) `1 ;

coherence
(c `2) `1 is quasi-loci ;

func index_of c -> Nat equals :: ABCMIZ_1:def 23
(c `2) `2 ;

coherence
(c `2) `2 is Nat ;

end;

:: deftheorem defines loci_of ABCMIZ_1:def 22 :
for c being Element of Constructors holds loci_of c = (c `2) `1 ;

:: deftheorem defines index_of ABCMIZ_1:def 23 :
for c being Element of Constructors holds index_of c = (c `2) `2 ;

theorem :: ABCMIZ_1:40

for c being Element of Constructors holds
( ( kind_of c = a_Type implies c in Modes ) & ( c in Modes implies kind_of c = a_Type ) & ( kind_of c = an_Adj implies c in Attrs ) & ( c in Attrs implies kind_of c = an_Adj ) & ( kind_of c = a_Term implies c in Funcs ) & ( c in Funcs implies kind_of c = a_Term ) )

proof end;

definition

func MaxConstrSign -> strict ConstructorSignature means :Def24: :: ABCMIZ_1:def 24
( the carrier' of it = {*,non_op} \/ Constructors & ( for o being OperSymbol of it st o is constructor holds
( the ResultSort of it . o = o `1 & card ( the Arity of it . o) = card ((o `2) `1) ) ) );

existence
ex b₁ being strict ConstructorSignature st
( the carrier' of b₁ = {*,non_op} \/ Constructors & ( for o being OperSymbol of b₁ st o is constructor holds
( the ResultSort of b₁ . o = o `1 & card ( the Arity of b<sub>1</sub> . o) = card ((o `2) `1) ) ) )

proof end;

uniqueness
for b₁, b₂ being strict ConstructorSignature st the carrier' of b₁ = {*,non_op} \/ Constructors & ( for o being OperSymbol of b₁ st o is constructor holds
( the ResultSort of b₁ . o = o `1 & card ( the Arity of b<sub>1</sub> . o) = card ((o `2) `1) ) ) & the carrier' of b<sub>2</sub> = {*,non_op} \/ Constructors & ( for o being OperSymbol of b<sub>2</sub> st o is constructor holds
( the ResultSort of b<sub>2</sub> . o = o `1 & card ( the Arity of b₂ . o) = card ((o `2) `1) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :
for b₁ being strict ConstructorSignature holds
( b₁ = MaxConstrSign iff ( the carrier' of b₁ = {*,non_op} \/ Constructors & ( for o being OperSymbol of b₁ st o is constructor holds
( the ResultSort of b₁ . o = o `1 & card ( the Arity of b<sub>1</sub> . o) = card ((o `2) `1) ) ) ) );

registration

cluster MinConstrSign -> strict non initialized ;

correctness
coherence
not MinConstrSign is initialized ;

proof end;

cluster MaxConstrSign -> strict initialized ;

correctness
coherence
MaxConstrSign is initialized ;

proof end;

end;

registration

cluster non empty non void V62() strict V265() constructor initialized for ManySortedSign ;

correctness
existence
ex b₁ being ConstructorSignature st
( b₁ is initialized & b₁ is strict );

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster constructor for Element of the carrier' of C;

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

proof end;

end;

definition

let C be ConstructorSignature;
A1: the carrier of C = {a_Type,an_Adj,a_Term} by Def9;

func MSVars C -> ManySortedSet of the carrier of C means :Def25: :: ABCMIZ_1:def 25
( it . a_Type = {} & it . an_Adj = {} & it . a_Term = Vars );

uniqueness
for b₁, b₂ being ManySortedSet of the carrier of C st b₁ . a_Type = {} & b₁ . an_Adj = {} & b₁ . a_Term = Vars & b₂ . a_Type = {} & b₂ . an_Adj = {} & b₂ . a_Term = Vars holds
b₁ = b₂

proof end;

existence
ex b₁ being ManySortedSet of the carrier of C st
( b₁ . a_Type = {} & b₁ . an_Adj = {} & b₁ . a_Term = Vars )

proof end;

end;

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

:: theorem
:: for C being ConstructorSignature
:: for x being variable holds
:: (C variables_in root-tree [x, a_Term]).a_Term C = {x} by MSAFREE3:11;

registration

let C be ConstructorSignature;

cluster MSVars C -> V9() ;

coherence
not MSVars C is empty-yielding

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster Free (C,(MSVars C)) -> non-empty ;

correctness
coherence
Free (C,(MSVars C)) is non-empty ;

proof end;

end;

definition

let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;
let t be Element of (Free (S,X));

attr t is ground means :: ABCMIZ_1:def 26
Union (S variables_in t) = {} ;

attr t is compound means :Def27: :: ABCMIZ_1:def 27
t . {} in [: the carrier' of S,{ the carrier of S}:];

end;

:: deftheorem defines ground ABCMIZ_1:def 26 :
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( t is ground iff Union (S variables_in t) = {} );

:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( t is compound iff t . {} in [: the carrier' of S,{ the carrier of S}:] );

definition

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

end;

definition

let C be initialized ConstructorSignature;
let s be SortSymbol of C;

mode expression of C,s -> expression of C means :Def28: :: ABCMIZ_1:def 28
it in the Sorts of (Free (C,(MSVars C))) . s;

existence
ex b₁ being expression of C st b₁ in the Sorts of (Free (C,(MSVars C))) . s

proof end;

end;

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

theorem Th41: :: ABCMIZ_1:41

for z being set
for C being initialized ConstructorSignature
for s being SortSymbol of C holds
( z is expression of C,s iff z in the Sorts of (Free (C,(MSVars C))) . s )

proof end;

definition

let C be initialized ConstructorSignature;
let c be constructor OperSymbol of C;
assume A1: len (the_arity_of c) = 0 ;

func c term -> expression of C equals :: ABCMIZ_1:def 29
[c, the carrier of C] -tree {};

coherence
[c, the carrier of C] -tree {} is expression of C

proof end;

end;

:: deftheorem defines term ABCMIZ_1:def 29 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C st len (the_arity_of c) = 0 holds
c term = [c, the carrier of C] -tree {};

theorem Th42: :: ABCMIZ_1:42

for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 1 holds
for a being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & a is expression of C,s ) holds
[o, the carrier of C] -tree <*a*> is expression of C, the_result_sort_of o

proof end;

definition

let C be initialized ConstructorSignature;
let o be OperSymbol of C;
assume A1: len (the_arity_of o) = 1 ;
let e be expression of C;
assume A2: ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & e is expression of C,s ) ;

func o term e -> expression of C equals :Def30: :: ABCMIZ_1:def 30
[o, the carrier of C] -tree <*e*>;

coherence
[o, the carrier of C] -tree <*e*> is expression of C by A1, A2, Th42;

end;

:: deftheorem Def30 defines term ABCMIZ_1:def 30 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 1 holds
for e being expression of C st ex s being SortSymbol of C st
( s = (the_arity_of o) . 1 & e is expression of C,s ) holds
o term e = [o, the carrier of C] -tree <*e*>;

theorem Th43: :: ABCMIZ_1:43

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( (non_op C) term a is expression of C, an_Adj C & (non_op C) term a = [non_op, the carrier of C] -tree <*a*> )

proof end;

theorem Th44: :: ABCMIZ_1:44

for C being initialized ConstructorSignature
for a, b being expression of C, an_Adj C st (non_op C) term a = (non_op C) term b holds
a = b

proof end;

registration

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;

cluster (non_op C) term a -> compound ;

coherence
(non_op C) term a is compound

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like compound for Element of Union the Sorts of (Free (C,(MSVars C)));

existence
ex b₁ being expression of C st b₁ is compound

proof end;

end;

theorem Th45: :: ABCMIZ_1:45

for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for a, b being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & a is expression of C,s1 & b is expression of C,s2 ) holds
[o, the carrier of C] -tree <*a,b*> is expression of C, the_result_sort_of o

proof end;

definition

let C be initialized ConstructorSignature;
let o be OperSymbol of C;
assume A1: len (the_arity_of o) = 2 ;
let e1, e2 be expression of C;
assume A2: ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) ;

func o term (e1,e2) -> expression of C equals :Def31: :: ABCMIZ_1:def 31
[o, the carrier of C] -tree <*e1,e2*>;

coherence
[o, the carrier of C] -tree <*e1,e2*> is expression of C by A1, A2, Th45;

end;

:: deftheorem Def31 defines term ABCMIZ_1:def 31 :
for C being initialized ConstructorSignature
for o being OperSymbol of C st len (the_arity_of o) = 2 holds
for e1, e2 being expression of C st ex s1, s2 being SortSymbol of C st
( s1 = (the_arity_of o) . 1 & s2 = (the_arity_of o) . 2 & e1 is expression of C,s1 & e2 is expression of C,s2 ) holds
o term (e1,e2) = [o, the carrier of C] -tree <*e1,e2*>;

theorem Th46: :: ABCMIZ_1:46

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds
( (ast C) term (a,t) is expression of C, a_Type C & (ast C) term (a,t) = [*, the carrier of C] -tree <*a,t*> )

proof end;

theorem :: ABCMIZ_1:47

for C being initialized ConstructorSignature
for a, b being expression of C, an_Adj C
for t1, t2 being expression of C, a_Type C st (ast C) term (a,t1) = (ast C) term (b,t2) holds
( a = b & t1 = t2 )

proof end;

registration

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;
let t be expression of C, a_Type C;

cluster (ast C) term (a,t) -> compound ;

coherence
(ast C) term (a,t) is compound

proof end;

end;

definition

let S be non void Signature;
let s be SortSymbol of S;
assume A1: ex o being OperSymbol of S st the_result_sort_of o = s ;

mode OperSymbol of s -> OperSymbol of S means :: ABCMIZ_1:def 32
the_result_sort_of it = s;

existence
ex b₁ being OperSymbol of S st the_result_sort_of b₁ = s by A1;

end;

:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :
for S being non void Signature
for s being SortSymbol of S st ex o being OperSymbol of S st the_result_sort_of o = s holds
for b₃ being OperSymbol of S holds
( b₃ is OperSymbol of s iff the_result_sort_of b₃ = s );

definition

let C be ConstructorSignature;
:: original: non_op
redefine func non_op C -> OperSymbol of an_Adj C;
coherence
non_op C is OperSymbol of an_Adj C

proof end;

:: original: ast
redefine func ast C -> OperSymbol of a_Type C;
coherence
ast C is OperSymbol of a_Type C

proof end;

end;

theorem Th48: :: ABCMIZ_1:48

for C being initialized ConstructorSignature
for s1, s2 being SortSymbol of C st s1 <> s2 holds
for t1 being expression of C,s1
for t2 being expression of C,s2 holds t1 <> t2

proof end;

definition

let C be initialized ConstructorSignature;
A1: the Sorts of (Free (C,(MSVars C))) . (a_Term C) c= Union the Sorts of (Free (C,(MSVars C)))

proof end;

func QuasiTerms C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 33
the Sorts of (Free (C,(MSVars C))) . (a_Term C);

coherence
the Sorts of (Free (C,(MSVars C))) . (a_Term C) is Subset of (Free (C,(MSVars C))) by A1;

end;

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

registration

let C be initialized ConstructorSignature;

cluster QuasiTerms C -> non empty constituted-DTrees ;

coherence
( not QuasiTerms C is empty & QuasiTerms C is constituted-DTrees ) ;

end;

definition

let C be initialized ConstructorSignature;
mode quasi-term of C is expression of C, a_Term C;

end;

theorem :: ABCMIZ_1:49

for z being set
for C being initialized ConstructorSignature holds
( z is quasi-term of C iff z in QuasiTerms C ) by Th41;

definition

let x be variable;
let C be initialized ConstructorSignature;

func x -term C -> quasi-term of C equals :: ABCMIZ_1:def 34
root-tree [x,a_Term];

coherence
root-tree [x,a_Term] is quasi-term of C

proof end;

end;

:: deftheorem defines -term ABCMIZ_1:def 34 :
for x being variable
for C being initialized ConstructorSignature holds x -term C = root-tree [x,a_Term];

theorem Th50: :: ABCMIZ_1:50

for x1, x2 being variable
for C1, C2 being initialized ConstructorSignature st x1 -term C1 = x2 -term C2 holds
x1 = x2

proof end;

registration

let x be variable;
let C be initialized ConstructorSignature;

cluster x -term C -> non compound ;

coherence
not x -term C is compound

proof end;

end;

theorem Th51: :: ABCMIZ_1:51

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being DTree-yielding FinSequence holds
( [c, the carrier of C] -tree p is expression of C iff ( len p = len (the_arity_of c) & p in (QuasiTerms C) * ) )

proof end;

definition

let C be initialized ConstructorSignature;
let c be constructor OperSymbol of C;
let p be FinSequence of QuasiTerms C;
assume A1: len p = len (the_arity_of c) ;
A2: p in (QuasiTerms C) * by FINSEQ_1:def 11;

func c -trm p -> compound expression of C equals :Def35: :: ABCMIZ_1:def 35
[c, the carrier of C] -tree p;

coherence
[c, the carrier of C] -tree p is compound expression of C

proof end;

end;

:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p = [c, the carrier of C] -tree p;

theorem Th52: :: ABCMIZ_1:52

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p is expression of C, the_result_sort_of c

proof end;

theorem Th53: :: ABCMIZ_1:53

for C being initialized ConstructorSignature
for e being expression of C holds
( ex x being variable st e = x -term C or ex c being constructor OperSymbol of C ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of c) & e = c -trm p ) or ex a being expression of C, an_Adj C st e = (non_op C) term a or ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t) )

proof end;

theorem Th54: :: ABCMIZ_1:54

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for a being expression of C, an_Adj C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (non_op C) term a

proof end;

theorem Th55: :: ABCMIZ_1:55

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for a being expression of C, an_Adj C
for t being expression of C, a_Type C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
c -trm p <> (ast C) term (a,t)

proof end;

theorem :: ABCMIZ_1:56

for C being initialized ConstructorSignature
for a, b being expression of C, an_Adj C
for t being expression of C, a_Type C holds (non_op C) term a <> (ast C) term (b,t)

proof end;

theorem Th57: :: ABCMIZ_1:57

for C being initialized ConstructorSignature
for e being expression of C st e . {} = [non_op, the carrier of C] holds
ex a being expression of C, an_Adj C st e = (non_op C) term a

proof end;

theorem Th58: :: ABCMIZ_1:58

for C being initialized ConstructorSignature
for e being expression of C st e . {} = [*, the carrier of C] holds
ex a being expression of C, an_Adj C ex t being expression of C, a_Type C st e = (ast C) term (a,t)

proof end;

definition

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;

func Non a -> expression of C, an_Adj C equals :Def36: :: ABCMIZ_1:def 36
a | <*0*> if ex a9 being expression of C, an_Adj C st a = (non_op C) term a9
otherwise (non_op C) term a;

coherence
( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies a | <*0*> is expression of C, an_Adj C ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C ) )

proof end;

consistency
for b₁ being expression of C, an_Adj C holds verum ;

end;

:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( ( ex a9 being expression of C, an_Adj C st a = (non_op C) term a9 implies Non a = a | <*0*> ) & ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies Non a = (non_op C) term a ) );

definition

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;

attr a is positive means :Def37: :: ABCMIZ_1:def 37
for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9;

end;

:: deftheorem Def37 defines positive ABCMIZ_1:def 37 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is positive iff for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 );

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive for expression of C, an_Adj C;

existence
ex b₁ being expression of C, an_Adj C st b₁ is positive

proof end;

end;

theorem Th59: :: ABCMIZ_1:59

for C being initialized ConstructorSignature
for a being positive expression of C, an_Adj C holds Non a = (non_op C) term a

proof end;

definition

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;

attr a is negative means :Def38: :: ABCMIZ_1:def 38
ex a9 being expression of C, an_Adj C st
( a9 is positive & a = (non_op C) term a9 );

end;

:: deftheorem Def38 defines negative ABCMIZ_1:def 38 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is negative iff ex a9 being expression of C, an_Adj C st
( a9 is positive & a = (non_op C) term a9 ) );

registration

let C be initialized ConstructorSignature;
let a be positive expression of C, an_Adj C;

cluster Non a -> non positive negative ;

coherence
( Non a is negative & not Non a is positive )

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like non positive negative for expression of C, an_Adj C;

existence
ex b₁ being expression of C, an_Adj C st
( b₁ is negative & not b₁ is positive )

proof end;

end;

theorem Th60: :: ABCMIZ_1:60

for C being initialized ConstructorSignature
for a being non positive expression of C, an_Adj C ex a9 being expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 )

proof end;

theorem Th61: :: ABCMIZ_1:61

for C being initialized ConstructorSignature
for a being negative expression of C, an_Adj C ex a9 being positive expression of C, an_Adj C st
( a = (non_op C) term a9 & Non a = a9 )

proof end;

theorem Th62: :: ABCMIZ_1:62

for C being initialized ConstructorSignature
for a being non positive expression of C, an_Adj C holds (non_op C) term (Non a) = a

proof end;

registration

let C be initialized ConstructorSignature;
let a be negative expression of C, an_Adj C;

cluster Non a -> positive ;

coherence
Non a is positive

proof end;

end;

definition

let C be initialized ConstructorSignature;
let a be expression of C, an_Adj C;

attr a is regular means :Def39: :: ABCMIZ_1:def 39
( a is positive or a is negative );

end;

:: deftheorem Def39 defines regular ABCMIZ_1:def 39 :
for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds
( a is regular iff ( a is positive or a is negative ) );

registration

let C be initialized ConstructorSignature;

cluster positive -> non negative regular for expression of C, an_Adj C;

coherence
for b₁ being expression of C, an_Adj C st b₁ is positive holds
( b₁ is regular & not b₁ is negative ) ;

cluster negative -> non positive regular for expression of C, an_Adj C;

coherence
for b₁ being expression of C, an_Adj C st b₁ is negative holds
( b₁ is regular & not b₁ is positive ) ;

end;

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like regular for expression of C, an_Adj C;

existence
ex b₁ being expression of C, an_Adj C st b₁ is regular

proof end;

end;

definition

let C be initialized ConstructorSignature;
set X = { a where a is expression of C, an_Adj C : a is regular } ;
A1: { a where a is expression of C, an_Adj C : a is regular } c= Union the Sorts of (Free (C,(MSVars C)))

proof end;

func QuasiAdjs C -> Subset of (Free (C,(MSVars C))) equals :: ABCMIZ_1:def 40
{ a where a is expression of C, an_Adj C : a is regular } ;

coherence
{ a where a is expression of C, an_Adj C : a is regular } is Subset of (Free (C,(MSVars C))) by A1;

end;

:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :
for C being initialized ConstructorSignature holds QuasiAdjs C = { a where a is expression of C, an_Adj C : a is regular } ;

registration

let C be initialized ConstructorSignature;

cluster QuasiAdjs C -> non empty constituted-DTrees ;

coherence
( not QuasiAdjs C is empty & QuasiAdjs C is constituted-DTrees )

proof end;

end;

definition

let C be initialized ConstructorSignature;
mode quasi-adjective of C is regular expression of C, an_Adj C;

end;

theorem Th63: :: ABCMIZ_1:63

for z being set
for C being initialized ConstructorSignature holds
( z is quasi-adjective of C iff z in QuasiAdjs C )

proof end;

theorem :: ABCMIZ_1:64

for z being set
for C being initialized ConstructorSignature holds
( z is quasi-adjective of C iff ( z is positive expression of C, an_Adj C or z is negative expression of C, an_Adj C ) ) by Def39;

registration

let C be initialized ConstructorSignature;

cluster non positive regular -> negative for expression of C, an_Adj C;

coherence
for b₁ being quasi-adjective of C st not b₁ is positive holds
b₁ is negative by Def39;

cluster non negative regular -> positive for expression of C, an_Adj C;

coherence
for b₁ being quasi-adjective of C st not b₁ is negative holds
b₁ is positive ;

end;

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like positive regular for expression of C, an_Adj C;

existence
ex b₁ being quasi-adjective of C st b₁ is positive

proof end;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like negative regular for expression of C, an_Adj C;

existence
ex b₁ being quasi-adjective of C st b₁ is negative

proof end;

end;

theorem Th65: :: ABCMIZ_1:65

for C being initialized ConstructorSignature
for a being positive quasi-adjective of C ex v being constructor OperSymbol of C st
( the_result_sort_of v = an_Adj C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of v) & a = v -trm p ) )

proof end;

theorem Th66: :: ABCMIZ_1:66

for C being initialized ConstructorSignature
for p being FinSequence of QuasiTerms C
for v being constructor OperSymbol of C st the_result_sort_of v = an_Adj C & len p = len (the_arity_of v) holds
v -trm p is positive quasi-adjective of C

proof end;

registration

let C be initialized ConstructorSignature;
let a be quasi-adjective of C;

cluster Non a -> regular ;

coherence
Non a is regular

proof end;

end;

theorem Th67: :: ABCMIZ_1:67

for C being initialized ConstructorSignature
for a being quasi-adjective of C holds Non (Non a) = a

proof end;

theorem :: ABCMIZ_1:68

for C being initialized ConstructorSignature
for a1, a2 being quasi-adjective of C st Non a1 = Non a2 holds
a1 = a2

proof end;

theorem :: ABCMIZ_1:69

for C being initialized ConstructorSignature
for a being quasi-adjective of C holds Non a <> a

proof end;

definition

let C be initialized ConstructorSignature;
let q be expression of C, a_Type C;

attr q is pure means :Def41: :: ABCMIZ_1:def 41
for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds not q = (ast C) term (a,t);

end;

:: deftheorem Def41 defines pure ABCMIZ_1:def 41 :
for C being initialized ConstructorSignature
for q being expression of C, a_Type C holds
( q is pure iff for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds not q = (ast C) term (a,t) );

theorem Th70: :: ABCMIZ_1:70

for C being initialized ConstructorSignature
for m being OperSymbol of C st the_result_sort_of m = a_Type & the_arity_of m = {} holds
ex t being expression of C, a_Type C st
( t = root-tree [m, the carrier of C] & t is pure )

proof end;

theorem Th71: :: ABCMIZ_1:71

for C being initialized ConstructorSignature
for v being OperSymbol of C st the_result_sort_of v = an_Adj & the_arity_of v = {} holds
ex a being expression of C, an_Adj C st
( a = root-tree [v, the carrier of C] & a is positive )

proof end;

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like pure for expression of C, a_Type C;

existence
ex b₁ being expression of C, a_Type C st b₁ is pure

proof end;

end;

definition

let C be initialized ConstructorSignature;

func QuasiTypes C -> set equals :: ABCMIZ_1:def 42
{ [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

coherence
{ [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } is set ;

end;

:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :
for C being initialized ConstructorSignature holds QuasiTypes C = { [A,t] where t is expression of C, a_Type C, A is finite Subset of (QuasiAdjs C) : t is pure } ;

registration

let C be initialized ConstructorSignature;

cluster QuasiTypes C -> non empty ;

coherence
not QuasiTypes C is empty

proof end;

end;

definition

let C be initialized ConstructorSignature;

mode quasi-type of C -> set means :Def43: :: ABCMIZ_1:def 43
it in QuasiTypes C;

existence
ex b₁ being set st b₁ in QuasiTypes C

proof end;

end;

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

theorem Th72: :: ABCMIZ_1:72

for z being set
for C being initialized ConstructorSignature holds
( z is quasi-type of C iff ex A being finite Subset of (QuasiAdjs C) ex q being pure expression of C, a_Type C st z = [A,q] )

proof end;

theorem Th73: :: ABCMIZ_1:73

for x, y being set
for C being initialized ConstructorSignature holds
( [x,y] is quasi-type of C iff ( x is finite Subset of (QuasiAdjs C) & y is pure expression of C, a_Type C ) )

proof end;

registration

let C be initialized ConstructorSignature;

cluster -> pair for quasi-type of C;

coherence
for b₁ being quasi-type of C holds b₁ is pair

proof end;

end;

theorem Th74: :: ABCMIZ_1:74

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C ex m being constructor OperSymbol of C st
( the_result_sort_of m = a_Type C & ex p being FinSequence of QuasiTerms C st
( len p = len (the_arity_of m) & q = m -trm p ) )

proof end;

theorem Th75: :: ABCMIZ_1:75

for C being initialized ConstructorSignature
for p being FinSequence of QuasiTerms C
for m being constructor OperSymbol of C st the_result_sort_of m = a_Type C & len p = len (the_arity_of m) holds
m -trm p is pure expression of C, a_Type C

proof end;

theorem :: ABCMIZ_1:76

for C being initialized ConstructorSignature holds
( QuasiTerms C misses QuasiAdjs C & QuasiTerms C misses QuasiTypes C & QuasiTypes C misses QuasiAdjs C )

proof end;

theorem :: ABCMIZ_1:77

for C being initialized ConstructorSignature
for e being set holds
( ( e is quasi-term of C implies not e is quasi-adjective of C ) & ( e is quasi-term of C implies not e is quasi-type of C ) & ( e is quasi-type of C implies not e is quasi-adjective of C ) ) by Th48;

notation

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

end;

definition

let C be initialized ConstructorSignature;
let A be finite Subset of (QuasiAdjs C);
let q be pure expression of C, a_Type C;
:: original: ast
redefine func A ast q -> quasi-type of C;
coherence
q ast is quasi-type of C by Th73;

end;

registration

let C be initialized ConstructorSignature;
let T be quasi-type of C;

cluster vars T -> finite for set ;

coherence
for b₁ being set st b₁ = T `1 holds
b₁ is finite

proof end;

end;

notation

let C be initialized ConstructorSignature;
let T be quasi-type of C;
synonym adjs T for C `1 ;
synonym the_base_of T for C `2 ;

end;

definition

let C be initialized ConstructorSignature;
let T be quasi-type of C;
:: original: vars
redefine func adjs T -> Subset of (QuasiAdjs C);
coherence
vars T is Subset of (QuasiAdjs C)

proof end;

:: original: the_base_of
redefine func the_base_of T -> pure expression of C, a_Type C;
coherence
the_base_of is pure expression of C, a_Type C

proof end;

end;

theorem :: ABCMIZ_1:78

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds
( adjs (A ast q) = A & the_base_of (A ast q) = q ) ;

theorem :: ABCMIZ_1:79

for C being initialized ConstructorSignature
for A1, A2 being finite Subset of (QuasiAdjs C)
for q1, q2 being pure expression of C, a_Type C st A1 ast q1 = A2 ast q2 holds
( A1 = A2 & q1 = q2 ) by XTUPLE_0:1;

theorem Th80: :: ABCMIZ_1:80

for C being initialized ConstructorSignature
for T being quasi-type of C holds T = (adjs T) ast (the_base_of T) ;

theorem :: ABCMIZ_1:81

for C being initialized ConstructorSignature
for T1, T2 being quasi-type of C st adjs T1 = adjs T2 & the_base_of T1 = the_base_of T2 holds
T1 = T2

proof end;

definition

let C be initialized ConstructorSignature;
let T be quasi-type of C;
let a be quasi-adjective of C;

func a ast T -> quasi-type of C equals :: ABCMIZ_1:def 44
[({a} \/ (adjs T)),(the_base_of T)];

coherence
[({a} \/ (adjs T)),(the_base_of T)] is quasi-type of C

proof end;

end;

:: deftheorem defines ast ABCMIZ_1:def 44 :
for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds a ast T = [({a} \/ (adjs T)),(the_base_of T)];

theorem :: ABCMIZ_1:82

for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds
( adjs (a ast T) = {a} \/ (adjs T) & the_base_of (a ast T) = the_base_of T ) ;

theorem :: ABCMIZ_1:83

for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds a ast (a ast T) = a ast T

proof end;

theorem :: ABCMIZ_1:84

for C being initialized ConstructorSignature
for T being quasi-type of C
for a, b being quasi-adjective of C holds a ast (b ast T) = b ast (a ast T) by XBOOLE_1:4;

registration

let S be non void Signature;
let s be SortSymbol of S;
let X be V8() ManySortedSet of the carrier of S;
let t be Term of S,X;

cluster (variables_in t) . s -> finite ;

coherence
(variables_in t) . s is finite

proof end;

end;

registration

let S be non void Signature;
let s be SortSymbol of S;
let X be V9() ManySortedSet of the carrier of S;
let t be Element of (Free (S,X));

cluster (S variables_in t) . s -> finite ;

coherence
(S variables_in t) . s is finite

proof end;

end;

definition

let S be non void Signature;
let X be V9() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

func (X,s) variables_in -> Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) means :Def45: :: ABCMIZ_1:def 45
for t being Element of (Free (S,X)) holds it . t = (S variables_in t) . s;

uniqueness
for b₁, b₂ being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st ( for t being Element of (Free (S,X)) holds b₁ . t = (S variables_in t) . s ) & ( for t being Element of (Free (S,X)) holds b₂ . t = (S variables_in t) . s ) holds
b₁ = b₂

proof end;

existence
ex b₁ being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) st
for t being Element of (Free (S,X)) holds b₁ . t = (S variables_in t) . s

proof end;

end;

:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :
for S being non void Signature
for X being V9() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b₄ being Function of (Union the Sorts of (Free (S,X))),(bool (X . s)) holds
( b₄ = (X,s) variables_in iff for t being Element of (Free (S,X)) holds b₄ . t = (S variables_in t) . s );

definition

let C be initialized ConstructorSignature;
let e be expression of C;

func variables_in e -> Subset of Vars equals :: ABCMIZ_1:def 46
(C variables_in e) . (a_Term C);

coherence
(C variables_in e) . (a_Term C) is Subset of Vars

proof end;

end;

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

registration

let C be initialized ConstructorSignature;
let e be expression of C;

cluster variables_in e -> finite ;

coherence
variables_in e is finite ;

end;

definition

let C be initialized ConstructorSignature;
let e be expression of C;

func vars e -> finite Subset of Vars equals :: ABCMIZ_1:def 47
varcl (variables_in e);

coherence
varcl (variables_in e) is finite Subset of Vars by Th24;

end;

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

theorem :: ABCMIZ_1:85

for C being initialized ConstructorSignature
for e being expression of C holds varcl (vars e) = vars e ;

theorem :: ABCMIZ_1:86

for C being initialized ConstructorSignature
for x being variable holds variables_in (x -term C) = {x} by MSAFREE3:10;

theorem :: ABCMIZ_1:87

for C being initialized ConstructorSignature
for x being variable holds vars (x -term C) = {x} \/ (vars x)

proof end;

theorem Th88: :: ABCMIZ_1:88

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for e being expression of C
for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
variables_in e = union { (variables_in t) where t is quasi-term of C : t in rng p }

proof end;

theorem Th89: :: ABCMIZ_1:89

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for e being expression of C
for p being DTree-yielding FinSequence st e = [c, the carrier of C] -tree p holds
vars e = union { (vars t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:90

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
variables_in (c -trm p) = union { (variables_in t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:91

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
vars (c -trm p) = union { (vars t) where t is quasi-term of C : t in rng p }

proof end;

theorem :: ABCMIZ_1:92

for S being ManySortedSign
for o being set holds S variables_in ([o, the carrier of S] -tree {}) = EmptyMS the carrier of S

proof end;

theorem Th93: :: ABCMIZ_1:93

for S being ManySortedSign
for o being set
for t being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t*>) = S variables_in t

proof end;

theorem Th94: :: ABCMIZ_1:94

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds variables_in ((non_op C) term a) = variables_in a

proof end;

theorem :: ABCMIZ_1:95

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds vars ((non_op C) term a) = vars a by Th94;

theorem Th96: :: ABCMIZ_1:96

for S being ManySortedSign
for o being set
for t1, t2 being DecoratedTree holds S variables_in ([o, the carrier of S] -tree <*t1,t2*>) = (S variables_in t1) (\/) (S variables_in t2)

proof end;

theorem Th97: :: ABCMIZ_1:97

for C being initialized ConstructorSignature
for t being expression of C, a_Type C
for a being expression of C, an_Adj C holds variables_in ((ast C) term (a,t)) = (variables_in a) \/ (variables_in t)

proof end;

theorem :: ABCMIZ_1:98

for C being initialized ConstructorSignature
for t being expression of C, a_Type C
for a being expression of C, an_Adj C holds vars ((ast C) term (a,t)) = (vars a) \/ (vars t)

proof end;

theorem Th99: :: ABCMIZ_1:99

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds variables_in (Non a) = variables_in a

proof end;

theorem :: ABCMIZ_1:100

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C holds vars (Non a) = vars a by Th99;

definition

let C be initialized ConstructorSignature;
let T be quasi-type of C;

func variables_in T -> Subset of Vars equals :: ABCMIZ_1:def 48
(union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

coherence
(union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T)) is Subset of Vars

proof end;

end;

:: deftheorem defines variables_in ABCMIZ_1:def 48 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds variables_in T = (union ((((MSVars C),(a_Term C)) variables_in) .: (adjs T))) \/ (variables_in (the_base_of T));

registration

let C be initialized ConstructorSignature;
let T be quasi-type of C;

cluster variables_in T -> finite ;

coherence
variables_in T is finite

proof end;

end;

definition

let C be initialized ConstructorSignature;
let T be quasi-type of C;

func vars T -> finite Subset of Vars equals :: ABCMIZ_1:def 49
varcl (variables_in T);

coherence
varcl (variables_in T) is finite Subset of Vars by Th24;

end;

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

theorem :: ABCMIZ_1:101

for C being initialized ConstructorSignature
for T being quasi-type of C holds varcl (vars T) = vars T ;

theorem Th102: :: ABCMIZ_1:102

for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds variables_in (a ast T) = (variables_in a) \/ (variables_in T)

proof end;

theorem :: ABCMIZ_1:103

for C being initialized ConstructorSignature
for T being quasi-type of C
for a being quasi-adjective of C holds vars (a ast T) = (vars a) \/ (vars T)

proof end;

theorem Th104: :: ABCMIZ_1:104

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds variables_in (A ast q) = (union { (variables_in a) where a is quasi-adjective of C : a in A } ) \/ (variables_in q)

proof end;

theorem :: ABCMIZ_1:105

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C
for A being finite Subset of (QuasiAdjs C) holds vars (A ast q) = (union { (vars a) where a is quasi-adjective of C : a in A } ) \/ (vars q)

proof end;

theorem Th106: :: ABCMIZ_1:106

for C being initialized ConstructorSignature
for q being pure expression of C, a_Type C holds variables_in (({} (QuasiAdjs C)) ast q) = variables_in q

proof end;

theorem Th107: :: ABCMIZ_1:107

for C being initialized ConstructorSignature
for e being expression of C holds
( e is ground iff variables_in e = {} )

proof end;

definition

let C be initialized ConstructorSignature;
let T be quasi-type of C;

attr T is ground means :Def50: :: ABCMIZ_1:def 50
variables_in T = {} ;

end;

:: deftheorem Def50 defines ground ABCMIZ_1:def 50 :
for C being initialized ConstructorSignature
for T being quasi-type of C holds
( T is ground iff variables_in T = {} );

registration

let C be initialized ConstructorSignature;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground pure for expression of C, a_Type C;

existence
ex b₁ being expression of C, a_Type C st
( b₁ is ground & b₁ is pure )

proof end;

cluster non pair non empty Relation-like Function-like finite DecoratedTree-like ground regular for expression of C, an_Adj C;

existence
ex b₁ being quasi-adjective of C st b₁ is ground

proof end;

end;

theorem Th108: :: ABCMIZ_1:108

for C being initialized ConstructorSignature
for t being ground pure expression of C, a_Type C holds ({} (QuasiAdjs C)) ast t is ground

proof end;

registration

let C be initialized ConstructorSignature;
let t be ground pure expression of C, a_Type C;

cluster t ast -> ground for quasi-type of C;

coherence
for b₁ being quasi-type of C st b₁ = ({} (QuasiAdjs C)) ast t holds
b₁ is ground by Th108;

end;

registration

let C be initialized ConstructorSignature;

cluster pair non empty ground for quasi-type of C;

existence
ex b₁ being quasi-type of C st b₁ is ground

proof end;

end;

registration

let C be initialized ConstructorSignature;
let T be ground quasi-type of C;
let a be ground quasi-adjective of C;

cluster a ast T -> ground ;

coherence
a ast T is ground

proof end;

end;

:: Type widening is smooth iff
:: vars-function is sup-semilattice homomorphism from widening sup-semilattice
:: into VarPoset

definition

func VarPoset -> non empty strict Poset equals :: ABCMIZ_1:def 51
(InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp ;

coherence
(InclPoset { (varcl A) where A is finite Subset of Vars : verum } ) opp is non empty strict Poset

proof end;

end;

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

theorem Th109: :: ABCMIZ_1:109

for x, y being Element of VarPoset holds
( x <= y iff y c= x )

proof end;

:: registration
:: let V1,V2 be Element of VarPoset;
:: identify V1 <= V2 with V2 c= V1;
:: compatibility by Th22;
:: end;

theorem Th110: :: ABCMIZ_1:110

for x being set holds
( x is Element of VarPoset iff ( x is finite Subset of Vars & varcl x = x ) )

proof end;

registration

cluster VarPoset -> non empty strict with_suprema with_infima ;

coherence
( VarPoset is with_infima & VarPoset is with_suprema )

proof end;

end;

theorem Th111: :: ABCMIZ_1:111

for V1, V2 being Element of VarPoset holds
( V1 "\/" V2 = V1 /\ V2 & V1 "/\" V2 = V1 \/ V2 )

proof end;

registration

let V1, V2 be Element of VarPoset;

identify V1 "\/" V2 with V1 /\ V2;

compatibility
V1 "\/" V2 = V1 /\ V2 by Th111;

identify V1 "/\" V2 with V1 \/ V2;

compatibility
V1 "/\" V2 = V1 \/ V2 by Th111;

end;

theorem Th112: :: ABCMIZ_1:112

for X being non empty Subset of VarPoset holds
( ex_sup_of X, VarPoset & sup X = meet X )

proof end;

registration

cluster VarPoset -> non empty strict up-complete ;

coherence
VarPoset is up-complete

proof end;

end;

theorem :: ABCMIZ_1:113

Top VarPoset = {}

proof end;

definition

let C be initialized ConstructorSignature;

func vars-function C -> Function of (QuasiTypes C), the carrier of VarPoset means :: ABCMIZ_1:def 52
for T being quasi-type of C holds it . T = vars T;

uniqueness
for b₁, b₂ being Function of (QuasiTypes C), the carrier of VarPoset st ( for T being quasi-type of C holds b₁ . T = vars T ) & ( for T being quasi-type of C holds b₂ . T = vars T ) holds
b₁ = b₂

proof end;

existence
ex b₁ being Function of (QuasiTypes C), the carrier of VarPoset st
for T being quasi-type of C holds b₁ . T = vars T

proof end;

end;

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

definition

let L be non empty Poset;

attr L is smooth means :: ABCMIZ_1:def 53
ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st
( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) );

end;

:: deftheorem defines smooth ABCMIZ_1:def 53 :
for L being non empty Poset holds
( L is smooth iff ex C being initialized ConstructorSignature ex f being Function of L,VarPoset st
( the carrier of L c= QuasiTypes C & f = (vars-function C) | the carrier of L & ( for x, y being Element of L holds f preserves_sup_of {x,y} ) ) );

registration

let C be initialized ConstructorSignature;
let T be ground quasi-type of C;

cluster RelStr(# {T},(id {T}) #) -> smooth ;

coherence
RelStr(# {T},(id {T}) #) is smooth

proof end;

end;

scheme :: ABCMIZ_1:sch 2
StructInd{ F₁() -> initialized ConstructorSignature, P₁[ set ], F₂() -> expression of F₁() } :

P₁[F₂()]

provided

A1: for x being variable holds P₁[x -term F₁()] and
A2: for c being constructor OperSymbol of F₁()
for p being FinSequence of QuasiTerms F₁() st len p = len (the_arity_of c) & ( for t being quasi-term of F₁() st t in rng p holds
P₁[t] ) holds
P₁[c -trm p] and
A3: for a being expression of F₁(), an_Adj F₁() st P₁[a] holds
P₁[(non_op F₁()) term a] and
A4: for a being expression of F₁(), an_Adj F₁() st P₁[a] holds
for t being expression of F₁(), a_Type F₁() st P₁[t] holds
P₁[(ast F₁()) term (a,t)]

proof end;

definition

let S be ManySortedSign ;

attr S is with_an_operation_for_each_sort means :Def54: :: ABCMIZ_1:def 54
the carrier of S c= rng the ResultSort of S;

let X be ManySortedSet of the carrier of S;

attr X is with_missing_variables means :: ABCMIZ_1:def 55
X " {{}} c= rng the ResultSort of S;

end;

:: deftheorem Def54 defines with_an_operation_for_each_sort ABCMIZ_1:def 54 :
for S being ManySortedSign holds
( S is with_an_operation_for_each_sort iff the carrier of S c= rng the ResultSort of S );

:: deftheorem defines with_missing_variables ABCMIZ_1:def 55 :
for S being ManySortedSign
for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff X " {{}} c= rng the ResultSort of S );

theorem Th114: :: ABCMIZ_1:114

for S being non void Signature
for X being ManySortedSet of the carrier of S holds
( X is with_missing_variables iff for s being SortSymbol of S st X . s = {} holds
ex o being OperSymbol of S st the_result_sort_of o = s )

proof end;

registration

cluster MaxConstrSign -> strict with_an_operation_for_each_sort ;

coherence
MaxConstrSign is with_an_operation_for_each_sort

proof end;

let C be ConstructorSignature;

cluster MSVars C -> with_missing_variables ;

coherence
MSVars C is with_missing_variables

proof end;

end;

registration

let S be ManySortedSign ;

cluster Relation-like V8() the carrier of S -defined Function-like total -> with_missing_variables for set ;

coherence
for b₁ being ManySortedSet of the carrier of S st b₁ is V8() holds
b₁ is with_missing_variables

proof end;

end;

registration

let S be ManySortedSign ;

cluster Relation-like the carrier of S -defined Function-like total with_missing_variables for set ;

existence
ex b₁ being ManySortedSet of the carrier of S st b₁ is with_missing_variables

proof end;

end;

registration

cluster non empty non void V62() strict V265() constructor initialized with_an_operation_for_each_sort for ManySortedSign ;

existence
ex b₁ being ConstructorSignature st
( b₁ is initialized & b₁ is with_an_operation_for_each_sort & b₁ is strict )

proof end;

end;

registration

let C be with_an_operation_for_each_sort ManySortedSign ;

cluster Relation-like the carrier of C -defined Function-like total -> with_missing_variables for set ;

coherence
for b₁ being ManySortedSet of the carrier of C holds b₁ is with_missing_variables

proof end;

end;

definition

let G be non empty DTConstrStr ;
:: original: Terminals
redefine func Terminals G -> Subset of G;
coherence
Terminals G is Subset of G

proof end;

:: original: NonTerminals
redefine func NonTerminals G -> Subset of G;
coherence
NonTerminals G is Subset of G

proof end;

end;

theorem Th115: :: ABCMIZ_1:115

for D1, D2 being non empty DTConstrStr st the Rules of D1 c= the Rules of D2 holds
( NonTerminals D1 c= NonTerminals D2 & the carrier of D1 /\ (Terminals D2) c= Terminals D1 & ( Terminals D1 c= Terminals D2 implies the carrier of D1 c= the carrier of D2 ) )

proof end;

theorem Th116: :: ABCMIZ_1:116

for D1, D2 being non empty DTConstrStr st Terminals D1 c= Terminals D2 & the Rules of D1 c= the Rules of D2 holds
TS D1 c= TS D2

proof end;

theorem Th117: :: ABCMIZ_1:117

for S being ManySortedSign
for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds
Y is with_missing_variables

proof end;

theorem Th118: :: ABCMIZ_1:118

for S being set
for X, Y being ManySortedSet of S st X c= Y holds
Union (coprod X) c= Union (coprod Y)

proof end;

theorem :: ABCMIZ_1:119

for S being non void Signature
for X, Y being ManySortedSet of the carrier of S st X c= Y holds
the carrier of (DTConMSA X) c= the carrier of (DTConMSA Y) by Th118, XBOOLE_1:9;

theorem Th120: :: ABCMIZ_1:120

for S being non void Signature
for X being ManySortedSet of the carrier of S st X is with_missing_variables holds
( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) )

proof end;

theorem :: ABCMIZ_1:121

for S being non void Signature
for X, Y being ManySortedSet of the carrier of S st X c= Y & X is with_missing_variables holds
( Terminals (DTConMSA X) c= Terminals (DTConMSA Y) & the Rules of (DTConMSA X) c= the Rules of (DTConMSA Y) & TS (DTConMSA X) c= TS (DTConMSA Y) )

proof end;

theorem Th122: :: ABCMIZ_1:122

for C being initialized ConstructorSignature
for t being set holds
( t in Terminals (DTConMSA (MSVars C)) iff ex x being variable st t = [x,(a_Term C)] )

proof end;

theorem Th123: :: ABCMIZ_1:123

for C being initialized ConstructorSignature
for t being set holds
( t in NonTerminals (DTConMSA (MSVars C)) iff ( t = [(ast C), the carrier of C] or t = [(non_op C), the carrier of C] or ex c being constructor OperSymbol of C st t = [c, the carrier of C] ) )

proof end;

theorem Th124: :: ABCMIZ_1:124

for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being set st t in Union the Sorts of (Free (S,X)) holds
t is Term of S,(X (\/) ( the carrier of S --> {0}))

proof end;

theorem :: ABCMIZ_1:125

for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S
for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in Union the Sorts of (Free (S,X)) holds
t in the Sorts of (Free (S,X)) . (the_sort_of t)

proof end;

theorem :: ABCMIZ_1:126

for G being non empty DTConstrStr
for s being Element of G
for p being FinSequence st s ==> p holds
p is FinSequence of the carrier of G

proof end;

theorem Th127: :: ABCMIZ_1:127

for S being non void Signature
for X, Y being ManySortedSet of the carrier of S
for g1 being Symbol of (DTConMSA X)
for g2 being Symbol of (DTConMSA Y)
for p1 being FinSequence of the carrier of (DTConMSA X)
for p2 being FinSequence of the carrier of (DTConMSA Y) st g1 = g2 & p1 = p2 & g1 ==> p1 holds
g2 ==> p2

proof end;

theorem Th128: :: ABCMIZ_1:128

for S being non void Signature
for X being with_missing_variables ManySortedSet of the carrier of S holds Union the Sorts of (Free (S,X)) = TS (DTConMSA X)

proof end;

definition

let S be non void Signature;
let X be ManySortedSet of the carrier of S;

mode term-transformation of S,X -> UnOp of (Union the Sorts of (Free (S,X))) means :Def56: :: ABCMIZ_1:def 56
for s being SortSymbol of S holds it .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s;

existence
ex b₁ being UnOp of (Union the Sorts of (Free (S,X))) st
for s being SortSymbol of S holds b₁ .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s

proof end;

end;

:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for b₃ being UnOp of (Union the Sorts of (Free (S,X))) holds
( b₃ is term-transformation of S,X iff for s being SortSymbol of S holds b₃ .: ( the Sorts of (Free (S,X)) . s) c= the Sorts of (Free (S,X)) . s );

theorem Th129: :: ABCMIZ_1:129

for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being UnOp of (Union the Sorts of (Free (S,X))) holds
( f is term-transformation of S,X iff for s being SortSymbol of S
for a being set st a in the Sorts of (Free (S,X)) . s holds
f . a in the Sorts of (Free (S,X)) . s )

proof end;

theorem Th130: :: ABCMIZ_1:130

for S being non void Signature
for X being non empty ManySortedSet of the carrier of S
for f being term-transformation of S,X
for s being SortSymbol of S
for p being FinSequence of the Sorts of (Free (S,X)) . s holds
( f * p is FinSequence of the Sorts of (Free (S,X)) . s & card (f * p) = len p )

proof end;

definition

let S be non void Signature;
let X be ManySortedSet of the carrier of S;
let t be term-transformation of S,X;

attr t is substitution means :: ABCMIZ_1:def 57
for o being OperSymbol of S
for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds
t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q;

end;

:: deftheorem defines substitution ABCMIZ_1:def 57 :
for S being non void Signature
for X being ManySortedSet of the carrier of S
for t being term-transformation of S,X holds
( t is substitution iff for o being OperSymbol of S
for p, q being FinSequence of (Free (S,X)) st [o, the carrier of S] -tree p in Union the Sorts of (Free (S,X)) & q = t * p holds
t . ([o, the carrier of S] -tree p) = [o, the carrier of S] -tree q );

scheme :: ABCMIZ_1:sch 3
StructDef{ F₁() -> initialized ConstructorSignature, F₂( set ) -> expression of F₁(), F₃( set ) -> expression of F₁(), F₄( set , set ) -> expression of F₁(), F₅( set , set ) -> expression of F₁() } :

ex f being term-transformation of F₁(), MSVars F₁() st
( ( for x being variable holds f . (x -term F₁()) = F₂(x) ) & ( for c being constructor OperSymbol of F₁()
for p, q being FinSequence of QuasiTerms F₁() st len p = len (the_arity_of c) & q = f * p holds
f . (c -trm p) = F₄(c,q) ) & ( for a being expression of F₁(), an_Adj F₁() holds f . ((non_op F₁()) term a) = F₃((f . a)) ) & ( for a being expression of F₁(), an_Adj F₁()
for t being expression of F₁(), a_Type F₁() holds f . ((ast F₁()) term (a,t)) = F₅((f . a),(f . t)) ) )

provided

A1: for x being variable holds F₂(x) is quasi-term of F₁() and
A2: for c being constructor OperSymbol of F₁()
for p being FinSequence of QuasiTerms F₁() st len p = len (the_arity_of c) holds
F₄(c,p) is expression of F₁(), the_result_sort_of c and
A3: for a being expression of F₁(), an_Adj F₁() holds F₃(a) is expression of F₁(), an_Adj F₁() and
A4: for a being expression of F₁(), an_Adj F₁()
for t being expression of F₁(), a_Type F₁() holds F₅(a,t) is expression of F₁(), a_Type F₁()

proof end;

definition

let A be set ;
let x, y be set ;
let a, b be Element of A;
:: original: IFIN
redefine func IFIN (x,y,a,b) -> Element of A;
coherence
IFIN (x,y,a,b) is Element of A by MATRIX_7:def 1;

end;

definition

let C be initialized ConstructorSignature;
mode valuation of C is PartFunc of Vars,(QuasiTerms C);

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;

attr f is irrelevant means :Def58: :: ABCMIZ_1:def 58
for x being variable st x in dom f holds
ex y being variable st f . x = y -term C;

end;

:: deftheorem Def58 defines irrelevant ABCMIZ_1:def 58 :
for C being initialized ConstructorSignature
for f being valuation of C holds
( f is irrelevant iff for x being variable st x in dom f holds
ex y being variable st f . x = y -term C );

notation

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

end;

registration

let C be initialized ConstructorSignature;

cluster empty Function-like -> irrelevant for Element of bool [:Vars,(QuasiTerms C):];

coherence
for b₁ being valuation of C st b₁ is empty holds
b₁ is irrelevant ;

end;

registration

let C be initialized ConstructorSignature;

cluster empty Relation-like Vars -defined QuasiTerms C -valued Function-like Function-yielding V119() for Element of bool [:Vars,(QuasiTerms C):];

existence
ex b₁ being valuation of C st b₁ is empty

proof end;

end;

definition

let C be initialized ConstructorSignature;
let X be Subset of Vars;

func C idval X -> valuation of C equals :: ABCMIZ_1:def 59
{ [x,(x -term C)] where x is variable : x in X } ;

coherence
{ [x,(x -term C)] where x is variable : x in X } is valuation of C

proof end;

end;

:: deftheorem defines idval ABCMIZ_1:def 59 :
for C being initialized ConstructorSignature
for X being Subset of Vars holds C idval X = { [x,(x -term C)] where x is variable : x in X } ;

theorem Th131: :: ABCMIZ_1:131

for C being initialized ConstructorSignature
for X being Subset of Vars holds
( dom (C idval X) = X & ( for x being variable st x in X holds
(C idval X) . x = x -term C ) )

proof end;

registration

let C be initialized ConstructorSignature;
let X be Subset of Vars;

cluster C idval X -> one-to-one irrelevant ;

coherence
( C idval X is irrelevant & C idval X is one-to-one )

proof end;

end;

registration

let C be initialized ConstructorSignature;
let X be empty Subset of Vars;

cluster C idval X -> empty ;

coherence
C idval X is empty

proof end;

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;

func f # -> term-transformation of C, MSVars C means :Def60: :: ABCMIZ_1:def 60
( ( for x being variable holds
( ( x in dom f implies it . (x -term C) = f . x ) & ( not x in dom f implies it . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = it * p holds
it . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds it . ((non_op C) term a) = (non_op C) term (it . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds it . ((ast C) term (a,t)) = (ast C) term ((it . a),(it . t)) ) );

existence
ex b₁ being term-transformation of C, MSVars C st
( ( for x being variable holds
( ( x in dom f implies b₁ . (x -term C) = f . x ) & ( not x in dom f implies b₁ . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b₁ * p holds
b₁ . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b₁ . ((non_op C) term a) = (non_op C) term (b₁ . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b₁ . ((ast C) term (a,t)) = (ast C) term ((b₁ . a),(b₁ . t)) ) )

proof end;

correctness
uniqueness
for b₁, b₂ being term-transformation of C, MSVars C st ( for x being variable holds
( ( x in dom f implies b₁ . (x -term C) = f . x ) & ( not x in dom f implies b₁ . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b₁ * p holds
b₁ . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b₁ . ((non_op C) term a) = (non_op C) term (b₁ . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b₁ . ((ast C) term (a,t)) = (ast C) term ((b₁ . a),(b₁ . t)) ) & ( for x being variable holds
( ( x in dom f implies b₂ . (x -term C) = f . x ) & ( not x in dom f implies b₂ . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b₂ * p holds
b₂ . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b₂ . ((non_op C) term a) = (non_op C) term (b₂ . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b₂ . ((ast C) term (a,t)) = (ast C) term ((b₂ . a),(b₂ . t)) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def60 defines # ABCMIZ_1:def 60 :
for C being initialized ConstructorSignature
for f being valuation of C
for b₃ being term-transformation of C, MSVars C holds
( b₃ = f # iff ( ( for x being variable holds
( ( x in dom f implies b₃ . (x -term C) = f . x ) & ( not x in dom f implies b₃ . (x -term C) = x -term C ) ) ) & ( for c being constructor OperSymbol of C
for p, q being FinSequence of QuasiTerms C st len p = len (the_arity_of c) & q = b₃ * p holds
b₃ . (c -trm p) = c -trm q ) & ( for a being expression of C, an_Adj C holds b₃ . ((non_op C) term a) = (non_op C) term (b₃ . a) ) & ( for a being expression of C, an_Adj C
for t being expression of C, a_Type C holds b₃ . ((ast C) term (a,t)) = (ast C) term ((b₃ . a),(b₃ . t)) ) ) );

registration

let C be initialized ConstructorSignature;
let f be valuation of C;

cluster f # -> substitution ;

coherence
f # is substitution

proof end;

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let e be expression of C;

func e at f -> expression of C equals :: ABCMIZ_1:def 61
(f #) . e;

coherence
(f #) . e is expression of C ;

end;

:: deftheorem defines at ABCMIZ_1:def 61 :
for C being initialized ConstructorSignature
for f being valuation of C
for e being expression of C holds e at f = (f #) . e;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let p be FinSequence;
assume A1: rng p c= Union the Sorts of (Free (C,(MSVars C))) ;

func p at f -> FinSequence equals :Def62: :: ABCMIZ_1:def 62
(f #) * p;

coherence
(f #) * p is FinSequence

proof end;

end;

:: deftheorem Def62 defines at ABCMIZ_1:def 62 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence st rng p c= Union the Sorts of (Free (C,(MSVars C))) holds
p at f = (f #) * p;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let p be FinSequence of QuasiTerms C;

:: original: at
redefine func p at f -> FinSequence of QuasiTerms C equals :: ABCMIZ_1:def 63
(f #) * p;

coherence
p at f is FinSequence of QuasiTerms C

proof end;

compatibility
for b₁ being FinSequence of QuasiTerms C holds
( b₁ = p at f iff b₁ = (f #) * p )

proof end;

end;

:: deftheorem defines at ABCMIZ_1:def 63 :
for C being initialized ConstructorSignature
for f being valuation of C
for p being FinSequence of QuasiTerms C holds p at f = (f #) * p;

theorem :: ABCMIZ_1:132

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

theorem :: ABCMIZ_1:133

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

theorem :: ABCMIZ_1:134

for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C
for f being valuation of C st len p = len (the_arity_of c) holds
(c -trm p) at f = c -trm (p at f) by Def60;

theorem :: ABCMIZ_1:135

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C
for f being valuation of C holds ((non_op C) term a) at f = (non_op C) term (a at f) by Def60;

theorem :: ABCMIZ_1:136

for C being initialized ConstructorSignature
for t being expression of C, a_Type C
for a being expression of C, an_Adj C
for f being valuation of C holds ((ast C) term (a,t)) at f = (ast C) term ((a at f),(t at f)) by Def60;

theorem Th137: :: ABCMIZ_1:137

for C being initialized ConstructorSignature
for e being expression of C
for X being Subset of Vars holds e at (C idval X) = e

proof end;

theorem :: ABCMIZ_1:138

for C being initialized ConstructorSignature
for X being Subset of Vars holds (C idval X) # = id (Union the Sorts of (Free (C,(MSVars C))))

proof end;

theorem Th139: :: ABCMIZ_1:139

for C being initialized ConstructorSignature
for e being expression of C
for f being empty valuation of C holds e at f = e

proof end;

theorem :: ABCMIZ_1:140

for C being initialized ConstructorSignature
for f being empty valuation of C holds f # = id (Union the Sorts of (Free (C,(MSVars C))))

proof end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let t be quasi-term of C;
:: original: at
redefine func t at f -> quasi-term of C;
coherence
t at f is quasi-term of C

proof end;

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let a be expression of C, an_Adj C;
:: original: at
redefine func a at f -> expression of C, an_Adj C;
coherence
a at f is expression of C, an_Adj C

proof end;

end;

registration

let C be initialized ConstructorSignature;
let f be valuation of C;
let a be positive expression of C, an_Adj C;

cluster a at f -> positive for expression of C, an_Adj C;

coherence
for b₁ being expression of C, an_Adj C st b₁ = a at f holds
b₁ is positive

proof end;

end;

registration

let C be initialized ConstructorSignature;
let f be valuation of C;
let a be negative expression of C, an_Adj C;

cluster a at f -> negative for expression of C, an_Adj C;

coherence
for b₁ being expression of C, an_Adj C st b₁ = a at f holds
b₁ is negative

proof end;

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let a be quasi-adjective of C;
:: original: at
redefine func a at f -> quasi-adjective of C;
coherence
a at f is quasi-adjective of C

proof end;

end;

theorem :: ABCMIZ_1:141

for C being initialized ConstructorSignature
for a being expression of C, an_Adj C
for f being valuation of C holds (Non a) at f = Non (a at f)

proof end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let t be expression of C, a_Type C;
:: original: at
redefine func t at f -> expression of C, a_Type C;
coherence
t at f is expression of C, a_Type C

proof end;

end;

registration

let C be initialized ConstructorSignature;
let f be valuation of C;
let t be pure expression of C, a_Type C;

cluster t at f -> pure for expression of C, a_Type C;

coherence
for b₁ being expression of C, a_Type C st b₁ = t at f holds
b₁ is pure

proof end;

end;

theorem :: ABCMIZ_1:142

for C being initialized ConstructorSignature
for f being one-to-one irrelevant valuation of C ex g being one-to-one irrelevant valuation of C st
for x, y being variable holds
( x in dom f & f . x = y -term C iff ( y in dom g & g . y = x -term C ) )

proof end;

theorem :: ABCMIZ_1:143

for C being initialized ConstructorSignature
for f, g being one-to-one irrelevant valuation of C st ( for x, y being variable st x in dom f & f . x = y -term C holds
( y in dom g & g . y = x -term C ) ) holds
for e being expression of C st variables_in e c= dom f holds
(e at f) at g = e

proof end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let A be Subset of (QuasiAdjs C);

func A at f -> Subset of (QuasiAdjs C) equals :: ABCMIZ_1:def 64
{ (a at f) where a is quasi-adjective of C : a in A } ;

coherence
{ (a at f) where a is quasi-adjective of C : a in A } is Subset of (QuasiAdjs C)

proof end;

end;

:: deftheorem defines at ABCMIZ_1:def 64 :
for C being initialized ConstructorSignature
for f being valuation of C
for A being Subset of (QuasiAdjs C) holds A at f = { (a at f) where a is quasi-adjective of C : a in A } ;

theorem Th144: :: ABCMIZ_1:144

for C being initialized ConstructorSignature
for f being valuation of C
for A being Subset of (QuasiAdjs C)
for a being quasi-adjective of C st A = {a} holds
A at f = {(a at f)}

proof end;

theorem Th145: :: ABCMIZ_1:145

for C being initialized ConstructorSignature
for f being valuation of C
for A, B being Subset of (QuasiAdjs C) holds (A \/ B) at f = (A at f) \/ (B at f)

proof end;

theorem :: ABCMIZ_1:146

for C being initialized ConstructorSignature
for f being valuation of C
for A, B being Subset of (QuasiAdjs C) st A c= B holds
A at f c= B at f

proof end;

registration

let C be initialized ConstructorSignature;
let f be valuation of C;
let A be finite Subset of (QuasiAdjs C);

cluster A at f -> finite ;

coherence
A at f is finite

proof end;

end;

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let T be quasi-type of C;

func T at f -> quasi-type of C equals :: ABCMIZ_1:def 65
((adjs T) at f) ast ((the_base_of T) at f);

coherence
((adjs T) at f) ast ((the_base_of T) at f) is quasi-type of C ;

end;

:: deftheorem defines at ABCMIZ_1:def 65 :
for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C holds T at f = ((adjs T) at f) ast ((the_base_of T) at f);

theorem :: ABCMIZ_1:147

for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C holds
( adjs (T at f) = (adjs T) at f & the_base_of (T at f) = (the_base_of T) at f ) ;

theorem :: ABCMIZ_1:148

for C being initialized ConstructorSignature
for f being valuation of C
for T being quasi-type of C
for a being quasi-adjective of C holds (a ast T) at f = (a at f) ast (T at f)

proof end;

definition

let C be initialized ConstructorSignature;
let f, g be valuation of C;

func f at g -> valuation of C means :Def66: :: ABCMIZ_1:def 66
( dom it = (dom f) \/ (dom g) & ( for x being variable st x in dom it holds
it . x = ((x -term C) at f) at g ) );

existence
ex b₁ being valuation of C st
( dom b₁ = (dom f) \/ (dom g) & ( for x being variable st x in dom b₁ holds
b₁ . x = ((x -term C) at f) at g ) )

proof end;

uniqueness
for b₁, b₂ being valuation of C st dom b₁ = (dom f) \/ (dom g) & ( for x being variable st x in dom b₁ holds
b₁ . x = ((x -term C) at f) at g ) & dom b₂ = (dom f) \/ (dom g) & ( for x being variable st x in dom b₂ holds
b₂ . x = ((x -term C) at f) at g ) holds
b₁ = b₂

proof end;

end;

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

registration

let C be initialized ConstructorSignature;
let f, g be irrelevant valuation of C;

cluster f at g -> irrelevant ;

coherence
f at g is irrelevant

proof end;

end;

theorem Th149: :: ABCMIZ_1:149

for C being initialized ConstructorSignature
for e being expression of C
for f1, f2 being valuation of C holds (e at f1) at f2 = e at (f1 at f2)

proof end;

theorem Th150: :: ABCMIZ_1:150

for C being initialized ConstructorSignature
for A being Subset of (QuasiAdjs C)
for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2)

proof end;

theorem :: ABCMIZ_1:151

for C being initialized ConstructorSignature
for T being quasi-type of C
for f1, f2 being valuation of C holds (T at f1) at f2 = T at (f1 at f2)

proof end;