ABCMIZ_1: Towards the construction of a model of Mizar concepts

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

begin

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

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

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

proof end;

existence

proof end;

projectivity ;

end;

:: deftheorem Def1 defines varcl ABCMIZ_1:def 1 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines Vars ABCMIZ_1:def 2 :

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

proof end;

end;

definition

mode variable is Element of Vars ;

end;

registration

let x be variable;

cluster vars x -> finite ;

coherence

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

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;

begin

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

proof end;

correctness

proof end;

end;

:: deftheorem Def3 defines QuasiLoci ABCMIZ_1:def 3 :

theorem Th29: :: ABCMIZ_1:29

<*> Vars in QuasiLoci

proof end;

registration

cluster QuasiLoci -> non empty ;

correctness by Th29;

end;

definition

mode quasi-loci is Element of QuasiLoci ;

end;

registration

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

coherence 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

proof end;

end;

begin

definition

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

coherence ;

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

coherence ;

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

coherence ;

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

coherence ;

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

coherence ;

end;

:: deftheorem defines a_Type ABCMIZ_1:def 4 :

:: deftheorem defines an_Adj ABCMIZ_1:def 5 :

:: deftheorem defines a_Term ABCMIZ_1:def 6 :

:: deftheorem defines * ABCMIZ_1:def 7 :

:: deftheorem defines non_op ABCMIZ_1:def 8 :

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 :

registration

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

coherence

proof end;

end;

definition

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

existence

proof end;

correctness

proof end;

end;

:: deftheorem Def10 defines MinConstrSign ABCMIZ_1:def 10 :

registration

cluster MinConstrSign -> strict constructor ;

coherence by Def10;

end;

registration

cluster strict V259() constructor for ManySortedSign ;

existence

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 :

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 :

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 by A1, ENUMSET1:def 1;

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

coherence by A1, ENUMSET1:def 1;

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

coherence 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 by A2, A4;

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

coherence by A2, A3;

end;

:: deftheorem defines a_Type ABCMIZ_1:def 13 :

:: deftheorem defines an_Adj ABCMIZ_1:def 14 :

:: deftheorem defines a_Term ABCMIZ_1:def 15 :

:: deftheorem defines non_op ABCMIZ_1:def 16 :

:: deftheorem defines ast ABCMIZ_1:def 17 :

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 ;

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

correctness ;

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

correctness ;

end;

:: deftheorem defines Modes ABCMIZ_1:def 18 :

:: deftheorem defines Attrs ABCMIZ_1:def 19 :

:: deftheorem defines Funcs ABCMIZ_1:def 20 :

registration

cluster Modes -> non empty ;

coherence ;

cluster Attrs -> non empty ;

coherence ;

cluster Funcs -> non empty ;

coherence ;

end;

definition

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

coherence ;

end;

:: deftheorem defines Constructors ABCMIZ_1:def 21 :

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 by MCART_1:10;
:: original: the_base_of
redefine func x `2 -> Element of NAT ;
coherence 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

proof end;

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

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 ;

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

coherence ;

end;

:: deftheorem defines loci_of ABCMIZ_1:def 22 :

:: deftheorem defines index_of ABCMIZ_1:def 23 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines MaxConstrSign ABCMIZ_1:def 24 :

registration

cluster MinConstrSign -> strict non initialized ;

correctness

proof end;

cluster MaxConstrSign -> strict initialized ;

correctness

proof end;

end;

registration

cluster non empty non void V58() strict V259() constructor initialized for ManySortedSign ;

correctness

proof end;

end;

registration

let C be initialized ConstructorSignature;

cluster constructor for Element of the carrier' of C;

existence

proof end;

end;

begin

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

proof end;

existence

proof end;

end;

:: deftheorem Def25 defines MSVars ABCMIZ_1:def 25 :

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

proof end;

end;

registration

let C be initialized ConstructorSignature;

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

correctness

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 :

:: deftheorem Def27 defines compound ABCMIZ_1:def 27 :

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

proof end;

end;

:: deftheorem Def28 defines expression ABCMIZ_1:def 28 :

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

proof end;

end;

:: deftheorem defines term ABCMIZ_1:def 29 :

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 by A1, A2, Th42;

end;

:: deftheorem Def30 defines term ABCMIZ_1:def 30 :

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

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

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 by A1, A2, Th45;

end;

:: deftheorem Def31 defines term ABCMIZ_1:def 31 :

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

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 by A1;

end;

:: deftheorem defines OperSymbol ABCMIZ_1:def 32 :

definition

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

proof end;

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

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;

begin

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 by A1;

end;

:: deftheorem defines QuasiTerms ABCMIZ_1:def 33 :

registration

let C be initialized ConstructorSignature;

cluster QuasiTerms C -> non empty constituted-DTrees ;

coherence

proof end;

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

proof end;

end;

:: deftheorem defines -term ABCMIZ_1:def 34 :

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

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 B1: len p = len (the_arity_of c) ;
A1: 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

proof end;

end;

:: deftheorem Def35 defines -trm ABCMIZ_1:def 35 :

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;

begin

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

proof end;

consistency ;

end;

:: deftheorem Def36 defines Non ABCMIZ_1:def 36 :

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 :

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

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 :

registration

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

cluster Non a -> non positive negative ;

coherence

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

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

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 :

registration

let C be initialized ConstructorSignature;

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

coherence

proof end;

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

coherence by Def39;

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

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 by A1;

end;

:: deftheorem defines QuasiAdjs ABCMIZ_1:def 40 :

registration

let C be initialized ConstructorSignature;

cluster QuasiAdjs C -> non empty constituted-DTrees ;

coherence

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 by Def39;

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

coherence ;

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

proof end;

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

existence

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

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;

begin

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 :

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

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 ;

end;

:: deftheorem defines QuasiTypes ABCMIZ_1:def 42 :

registration

let C be initialized ConstructorSignature;

cluster QuasiTypes C -> non empty ;

coherence

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

proof end;

end;

:: deftheorem Def43 defines quasi-type ABCMIZ_1:def 43 :

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

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 by Th73;

end;

registration

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

cluster vars T -> finite ;

coherence

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

proof end;

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

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)

proof end;

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

proof end;

end;

:: deftheorem defines ast ABCMIZ_1:def 44 :

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

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)

proof end;

begin

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

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

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

proof end;

existence

proof end;

end;

:: deftheorem Def45 defines variables_in ABCMIZ_1:def 45 :

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

proof end;

end;

:: deftheorem defines variables_in ABCMIZ_1:def 46 :

registration

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

cluster variables_in e -> finite ;

coherence ;

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 by Th24;

end;

:: deftheorem defines vars ABCMIZ_1:def 47 :

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 {}) = [[0]] 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

proof end;

end;

:: deftheorem defines variables_in ABCMIZ_1:def 48 :

registration

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

cluster variables_in T -> finite ;

coherence

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 by Th24;

end;

:: deftheorem defines vars ABCMIZ_1:def 49 :

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 :

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

proof end;

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

existence

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 by Th108;

end;

registration

let C be initialized ConstructorSignature;

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

existence

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

proof end;

end;

begin

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

proof end;

end;

:: deftheorem defines VarPoset ABCMIZ_1:def 51 :

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

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 by Th111;

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

compatibility 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

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

proof end;

existence

proof end;

end;

:: deftheorem defines vars-function ABCMIZ_1:def 52 :

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 :

registration

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

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

coherence

proof end;

end;

begin

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

:: deftheorem Def55 defines with_missing_variables ABCMIZ_1:def 55 :

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

proof end;

let C be ConstructorSignature;

cluster MSVars C -> with_missing_variables ;

coherence

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

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

proof end;

end;

registration

cluster non empty non void V58() strict V259() constructor initialized with_an_operation_for_each_sort for ManySortedSign ;

existence

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

proof end;

end;

definition

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

proof end;

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

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

proof end;

end;

:: deftheorem Def56 defines term-transformation ABCMIZ_1:def 56 :

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 :

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;

begin

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

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

proof end;

end;

registration

let C be initialized ConstructorSignature;

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

existence

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

proof end;

end;

:: deftheorem defines idval ABCMIZ_1:def 59 :

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

proof end;

end;

registration

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

cluster C idval X -> empty ;

coherence

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

proof end;

correctness

proof end;

end;

:: deftheorem Def60 defines # ABCMIZ_1:def 60 :

registration

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

cluster f # -> substitution ;

coherence

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 ;

end;

:: deftheorem defines at ABCMIZ_1:def 61 :

definition

let C be initialized ConstructorSignature;
let f be valuation of C;
let p be FinSequence;
assume B1: 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

proof end;

end;

:: deftheorem Def62 defines at ABCMIZ_1:def 62 :

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

proof end;

compatibility

proof end;

end;

:: deftheorem defines at ABCMIZ_1:def 63 :

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;

:: theorem
:: for t being expression of C
:: for f1,f2 being valuation of C
:: holds (t at f1) at f2 = ((f2# )*(f1# )).t by FUNCT_2:21;

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

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

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

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

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

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

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

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

proof end;

end;

:: deftheorem defines at ABCMIZ_1:def 64 :

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

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 ;

end;

:: deftheorem defines at ABCMIZ_1:def 65 :

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def66 defines at ABCMIZ_1:def 66 :

registration

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

cluster f at g -> irrelevant ;

coherence

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;