:: Terms over many sorted universal algebra
:: by Grzegorz Bancerek
::
:: Received November 25, 1994
:: Copyright (c) 1994 Association of Mizar Users
Lm1:
for n being set
for p being FinSequence st n in dom p holds
ex k being Element of NAT st
( n = k + 1 & k < len p )
:: deftheorem Def1 defines -Terms MSATERM:def 1 :
:: deftheorem Def2 defines ArgumentSeq MSATERM:def 2 :
theorem Th1: :: MSATERM:1
Lm3:
now
let S be non
empty non
void ManySortedSign ;
:: thesis: for V being V5() ManySortedSet of
for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )let V be
V5()
ManySortedSet of ;
:: thesis: for x being set holds
( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )let x be
set ;
:: thesis: ( ( x in Terminals (DTConMSA V) implies ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S
for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V) ) )set X =
V;
set G =
DTConMSA V;
A1:
Terminals (DTConMSA V) = Union (coprod V)
by MSAFREE:6;
let s be
SortSymbol of
S;
:: thesis: for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA V)let a be
Element of
V . s;
:: thesis: ( x = [a,s] implies x in Terminals (DTConMSA V) )assume
x = [a,s]
;
:: thesis: x in Terminals (DTConMSA V)then
x in coprod s,
V
by MSAFREE:def 2;
then A4:
x in (coprod V) . s
by MSAFREE:def 3;
dom (coprod V) = the
carrier of
S
by PARTFUN1:def 4;
hence
x in Terminals (DTConMSA V)
by A1, A4, CARD_5:10;
:: thesis: verum
end;
Lm4:
now
let S be non
empty non
void ManySortedSign ;
:: thesis: for A being MSAlgebra of S
for V being V5() ManySortedSet of
for x being set holds
( ( not x in Terminals (DTConMSA (the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) ) ) )let A be
MSAlgebra of
S;
:: thesis: for V being V5() ManySortedSet of
for x being set holds
( ( not x in Terminals (DTConMSA (the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) ) ) )let V be
V5()
ManySortedSet of ;
:: thesis: for x being set holds
( ( not x in Terminals (DTConMSA (the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) ) ) )let x be
set ;
:: thesis: ( ( not x in Terminals (DTConMSA (the Sorts of A \/ V)) or ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] ) & ( for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) ) ) )set X = the
Sorts of
A \/ V;
set G =
DTConMSA (the Sorts of A \/ V);
A1:
dom (coprod (the Sorts of A \/ V)) = the
carrier of
S
by PARTFUN1:def 4;
A2:
Terminals (DTConMSA (the Sorts of A \/ V)) = Union (coprod (the Sorts of A \/ V))
by MSAFREE:6;
hereby :: thesis: for s being SortSymbol of S holds
( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) )
assume
x in Terminals (DTConMSA (the Sorts of A \/ V))
;
:: thesis: ( ex s being SortSymbol of S ex a being set st
( a in the Sorts of A . s & x = [a,s] ) or ex s being SortSymbol of S ex v being Element of V . s st x = [v,s] )then consider s being
set such that A3:
s in dom (coprod (the Sorts of A \/ V))
and A4:
x in (coprod (the Sorts of A \/ V)) . s
by A2, CARD_5:10;
reconsider s =
s as
SortSymbol of
S by A3, PARTFUN1:def 4;
(coprod (the Sorts of A \/ V)) . s = coprod s,
(the Sorts of A \/ V)
by MSAFREE:def 3;
then consider a being
set such that A5:
a in (the Sorts of A \/ V) . s
and A6:
x = [a,s]
by A4, MSAFREE:def 2;
(the Sorts of A \/ V) . s = (the Sorts of A . s) \/ (V . s)
by PBOOLE:def 7;
then
(
a in the
Sorts of
A . s or
a in V . s )
by A5, XBOOLE_0:def 3;
hence
( ex
s being
SortSymbol of
S ex
a being
set st
(
a in the
Sorts of
A . s &
x = [a,s] ) or ex
s being
SortSymbol of
S ex
v being
Element of
V . s st
x = [v,s] )
by A6;
:: thesis: verum
end;
let s be
SortSymbol of
S;
:: thesis: ( ( for a being set st a in the Sorts of A . s & x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) & ( for a being Element of V . s st x = [a,s] holds
x in Terminals (DTConMSA (the Sorts of A \/ V)) ) )A7:
(the Sorts of A \/ V) . s = (the Sorts of A . s) \/ (V . s)
by PBOOLE:def 7;
let a be
Element of
V . s;
:: thesis: ( x = [a,s] implies x in Terminals (DTConMSA (the Sorts of A \/ V)) )assume A9:
x = [a,s]
;
:: thesis: x in Terminals (DTConMSA (the Sorts of A \/ V))
a in (the Sorts of A \/ V) . s
by A7, XBOOLE_0:def 3;
then
x in coprod s,
(the Sorts of A \/ V)
by A9, MSAFREE:def 2;
then
x in (coprod (the Sorts of A \/ V)) . s
by MSAFREE:def 3;
hence
x in Terminals (DTConMSA (the Sorts of A \/ V))
by A2, A1, CARD_5:10;
:: thesis: verum
end;
theorem Th2: :: MSATERM:2
theorem :: MSATERM:3
theorem Th4: :: MSATERM:4
theorem Th5: :: MSATERM:5
theorem Th6: :: MSATERM:6
theorem :: MSATERM:7
theorem Th8: :: MSATERM:8
theorem :: MSATERM:9
theorem Th10: :: MSATERM:10
:: deftheorem defines -term MSATERM:def 3 :
:: deftheorem defines -term MSATERM:def 4 :
theorem Th11: :: MSATERM:11
theorem :: MSATERM:12
theorem :: MSATERM:13
Lm7:
for x being set holds not x in x
;
:: deftheorem Def5 defines the_sort_of MSATERM:def 5 :
theorem Th14: :: MSATERM:14
theorem Th15: :: MSATERM:15
theorem :: MSATERM:16
theorem Th17: :: MSATERM:17
theorem :: MSATERM:18
theorem Th19: :: MSATERM:19
theorem Th20: :: MSATERM:20
theorem Th21: :: MSATERM:21
Lm8:
for S being non empty non void ManySortedSign
for V being V5() ManySortedSet of
for o being OperSymbol of S
for a being ArgumentSeq of Sym o,V holds
( len a = len (the_arity_of o) & dom a = dom (the_arity_of o) & ( for i being Nat st i in dom a holds
ex t being Term of S,V st
( t = a . i & t = a /. i & the_sort_of t = (the_arity_of o) . i & the_sort_of t = (the_arity_of o) /. i ) ) )
theorem Th22: :: MSATERM:22
theorem :: MSATERM:23
theorem Th24: :: MSATERM:24
theorem :: MSATERM:25
theorem Th26: :: MSATERM:26
theorem :: MSATERM:27
:: deftheorem defines CompoundTerm MSATERM:def 6 :
:: deftheorem defines SetWithCompoundTerm MSATERM:def 7 :
theorem :: MSATERM:28
Lm9:
for n being Element of NAT
for p being FinSequence st n < len p holds
( n + 1 in dom p & p . (n + 1) in rng p )
theorem Th29: :: MSATERM:29
:: deftheorem Def8 defines Variables MSATERM:def 8 :
theorem Th30: :: MSATERM:30
:: deftheorem Def9 defines is_an_evaluation_of MSATERM:def 9 :
theorem Th31: :: MSATERM:31
theorem Th32: :: MSATERM:32
theorem Th33: :: MSATERM:33
theorem Th34: :: MSATERM:34
theorem Th35: :: MSATERM:35
theorem Th36: :: MSATERM:36
theorem Th37: :: MSATERM:37
theorem Th38: :: MSATERM:38
:: deftheorem Def10 defines @ MSATERM:def 10 :
theorem Th39: :: MSATERM:39
theorem :: MSATERM:40
theorem :: MSATERM:41
theorem :: MSATERM:42
theorem :: MSATERM:43