:: ABCMIZ_A semantic presentation
begin
theorem Th1: :: ABCMIZ_A:1
for x being pair set holds x = [(x `1),(x `2)] ;
scheme :: ABCMIZ_A:sch 1
MinimalElement{ F1() -> non empty finite set , P1[ set , set ] } :
ex x being set st
( x in F1() & ( for y being set st y in F1() holds
not P1[y,x] ) )
provided
A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
not P1[y,x] and
A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds
P1[x,z]
proof
assume A3: for x being set st x in F1() holds
ex y being set st
( y in F1() & P1[y,x] ) ; ::_thesis: contradiction
set n = card F1();
set x0 = the Element of F1();
defpred S1[ Nat, set , set ] means ( $2 in F1() implies ( $3 in F1() & P1[$3,$2] ) );
A4: for m being Element of NAT st 1 <= m & m < (card F1()) + 1 holds
for x being set ex y being set st S1[m,x,y]
proof
let m be Element of NAT ; ::_thesis: ( 1 <= m & m < (card F1()) + 1 implies for x being set ex y being set st S1[m,x,y] )
assume ( 1 <= m & m < (card F1()) + 1 ) ; ::_thesis: for x being set ex y being set st S1[m,x,y]
let x be set ; ::_thesis: ex y being set st S1[m,x,y]
percases ( x nin F1() or x in F1() ) ;
supposeA5: x nin F1() ; ::_thesis: ex y being set st S1[m,x,y]
set y = the set ;
take the set ; ::_thesis: S1[m,x, the set ]
thus S1[m,x, the set ] by A5; ::_thesis: verum
end;
suppose x in F1() ; ::_thesis: ex y being set st S1[m,x,y]
then consider y being set such that
A6: ( y in F1() & P1[y,x] ) by A3;
take y ; ::_thesis: S1[m,x,y]
thus S1[m,x,y] by A6; ::_thesis: verum
end;
end;
end;
consider p being FinSequence such that
A7: len p = (card F1()) + 1 and
A8: ( p . 1 = the Element of F1() or (card F1()) + 1 = 0 ) and
A9: for i being Element of NAT st 1 <= i & i < (card F1()) + 1 holds
S1[i,p . i,p . (i + 1)] from RECDEF_1:sch_3(A4);
defpred S2[ Nat] means ( $1 in dom p implies p . $1 in F1() );
A10: S2[ 0 ] by FINSEQ_3:25;
A11: now__::_thesis:_for_i_being_Nat_st_S2[i]_holds_
S2[i_+_1]
let i be Nat; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A12: S2[i] ; ::_thesis: S2[i + 1]
thus S2[i + 1] ::_thesis: verum
proof
assume i + 1 in dom p ; ::_thesis: p . (i + 1) in F1()
then i + 1 <= (card F1()) + 1 by A7, FINSEQ_3:25;
then A13: i < (card F1()) + 1 by NAT_1:13;
percases ( i = 0 or i > 0 ) by NAT_1:3;
suppose i = 0 ; ::_thesis: p . (i + 1) in F1()
hence p . (i + 1) in F1() by A8; ::_thesis: verum
end;
suppose i > 0 ; ::_thesis: p . (i + 1) in F1()
then ( i >= 0 + 1 & i is Element of NAT ) by NAT_1:13, ORDINAL1:def_12;
hence p . (i + 1) in F1() by A12, A7, A9, A13, FINSEQ_3:25; ::_thesis: verum
end;
end;
end;
end;
A14: for i being Nat holds S2[i] from NAT_1:sch_2(A10, A11);
A15: rng p c= F1()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in F1() )
assume x in rng p ; ::_thesis: x in F1()
then ex i being set st
( i in dom p & x = p . i ) by FUNCT_1:def_3;
hence x in F1() by A14; ::_thesis: verum
end;
A16: for i, j being Nat st 1 <= i & i < j & j <= (card F1()) + 1 holds
P1[p . j,p . i]
proof
let i, j be Nat; ::_thesis: ( 1 <= i & i < j & j <= (card F1()) + 1 implies P1[p . j,p . i] )
assume A17: 1 <= i ; ::_thesis: ( not i < j or not j <= (card F1()) + 1 or P1[p . j,p . i] )
assume A18: i < j ; ::_thesis: ( not j <= (card F1()) + 1 or P1[p . j,p . i] )
then i + 1 <= j by NAT_1:13;
then consider k being Nat such that
A19: j = (i + 1) + k by NAT_1:10;
assume A20: j <= (card F1()) + 1 ; ::_thesis: P1[p . j,p . i]
then i <= (card F1()) + 1 by A18, XXREAL_0:2;
then A21: i in dom p by A17, A7, FINSEQ_3:25;
defpred S3[ Nat] means ( (i + 1) + $1 <= (card F1()) + 1 implies P1[p . ((i + 1) + $1),p . i] );
A22: S3[ 0 ]
proof
assume (i + 1) + 0 <= (card F1()) + 1 ; ::_thesis: P1[p . ((i + 1) + 0),p . i]
then A23: i < (card F1()) + 1 by NAT_1:13;
( p . i in F1() & i is Element of NAT ) by A14, A21;
hence P1[p . ((i + 1) + 0),p . i] by A9, A17, A23; ::_thesis: verum
end;
A24: now__::_thesis:_for_k_being_Nat_st_S3[k]_holds_
S3[k_+_1]
let k be Nat; ::_thesis: ( S3[k] implies S3[k + 1] )
assume A25: S3[k] ; ::_thesis: S3[k + 1]
thus S3[k + 1] ::_thesis: verum
proof
assume A26: (i + 1) + (k + 1) <= (card F1()) + 1 ; ::_thesis: P1[p . ((i + 1) + (k + 1)),p . i]
A27: (i + 1) + (k + 1) = ((i + 1) + k) + 1 ;
then A28: (i + 1) + k < (card F1()) + 1 by A26, NAT_1:13;
A29: p . i in F1() by A14, A21;
(i + 1) + k = 1 + (i + k) ;
then A30: 1 <= (i + 1) + k by NAT_1:11;
then (i + 1) + k in dom p by A7, A28, FINSEQ_3:25;
then A31: ( p . ((i + 1) + k) in F1() & (i + 1) + k is Element of NAT ) by A14;
then ( p . ((i + 1) + (k + 1)) in F1() & P1[p . ((i + 1) + (k + 1)),p . ((i + 1) + k)] ) by A9, A28, A27, A30;
hence P1[p . ((i + 1) + (k + 1)),p . i] by A2, A28, A25, A31, A29; ::_thesis: verum
end;
end;
for k being Nat holds S3[k] from NAT_1:sch_2(A22, A24);
hence P1[p . j,p . i] by A19, A20; ::_thesis: verum
end;
A32: ( dom p = Seg ((card F1()) + 1) & card (Seg ((card F1()) + 1)) = (card F1()) + 1 ) by A7, FINSEQ_1:57, FINSEQ_1:def_3;
card (rng p) c= card F1() by A15, CARD_1:11;
then ( card (rng p) <= card F1() & card F1() < (card F1()) + 1 ) by NAT_1:19, NAT_1:39;
then not dom p, rng p are_equipotent by A32, CARD_1:5;
then not p is one-to-one by WELLORD2:def_4;
then consider i, j being set such that
A33: ( i in dom p & j in dom p & p . i = p . j & i <> j ) by FUNCT_1:def_4;
reconsider i = i, j = j as Nat by A33;
A34: ( 1 <= i & 1 <= j & i <= (card F1()) + 1 & j <= (card F1()) + 1 ) by A7, A33, FINSEQ_3:25;
p . i in rng p by A33, FUNCT_1:def_3;
then A35: p . i in F1() by A15;
( i < j or j < i ) by A33, XXREAL_0:1;
then P1[p . i,p . i] by A16, A33, A34;
hence contradiction by A1, A35; ::_thesis: verum
end;
scheme :: ABCMIZ_A:sch 2
FiniteC{ F1() -> finite set , P1[ set ] } :
P1[F1()]
provided
A1: for A being Subset of F1() st ( for B being set st B c< A holds
P1[B] ) holds
P1[A]
proof
defpred S1[ Nat] means for A being Subset of F1() st card A = $1 holds
P1[A];
A2: for n being Nat st ( for i being Nat st i < n holds
S1[i] ) holds
S1[n]
proof
let n be Nat; ::_thesis: ( ( for i being Nat st i < n holds
S1[i] ) implies S1[n] )
assume A3: for i being Nat st i < n holds
S1[i] ; ::_thesis: S1[n]
let A be Subset of F1(); ::_thesis: ( card A = n implies P1[A] )
assume A4: card A = n ; ::_thesis: P1[A]
now__::_thesis:_for_B_being_set_st_B_c<_A_holds_
P1[B]
let B be set ; ::_thesis: ( B c< A implies P1[B] )
assume A5: B c< A ; ::_thesis: P1[B]
B c= A by A5, XBOOLE_0:def_8;
then reconsider B9 = B as Subset of F1() by XBOOLE_1:1;
card B9 < n by A4, A5, TREES_1:6;
hence P1[B] by A3; ::_thesis: verum
end;
hence P1[A] by A1; ::_thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch_4(A2);
then ( S1[ card F1()] & [#] F1() = F1() ) ;
hence P1[F1()] ; ::_thesis: verum
end;
scheme :: ABCMIZ_A:sch 3
Numeration{ F1() -> finite set , P1[ set , set ] } :
ex s being one-to-one FinSequence st
( rng s = F1() & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j ) )
provided
A1: for x, y being set st x in F1() & y in F1() & P1[x,y] holds
not P1[y,x] and
A2: for x, y, z being set st x in F1() & y in F1() & z in F1() & P1[x,y] & P1[y,z] holds
P1[x,z]
proof
defpred S1[ set ] means ex s being one-to-one FinSequence st
( rng s = $1 & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j ) );
A3: S1[ {} ]
proof
reconsider s = {} as one-to-one FinSequence ;
take s ; ::_thesis: ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j ) )
thus ( rng s = {} & ( for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j ) ) ; ::_thesis: verum
end;
A4: for A being Subset of F1() st ( for B being set st B c< A holds
S1[B] ) holds
S1[A]
proof
let A be Subset of F1(); ::_thesis: ( ( for B being set st B c< A holds
S1[B] ) implies S1[A] )
assume A5: for B being set st B c< A holds
S1[B] ; ::_thesis: S1[A]
percases ( A is empty or not A is empty ) ;
suppose A is empty ; ::_thesis: S1[A]
hence S1[A] by A3; ::_thesis: verum
end;
suppose not A is empty ; ::_thesis: S1[A]
then reconsider A9 = A as non empty finite set ;
A6: for x, y being set st x in A9 & y in A9 & P1[x,y] holds
not P1[y,x] by A1;
A7: for x, y, z being set st x in A9 & y in A9 & z in A9 & P1[x,y] & P1[y,z] holds
P1[x,z] by A2;
consider x being set such that
A8: ( x in A9 & ( for y being set st y in A9 holds
not P1[y,x] ) ) from ABCMIZ_A:sch_1(A6, A7);
set B = A \ {x};
A9: ( x nin A \ {x} & A \ {x} c= A ) by XBOOLE_1:36, ZFMISC_1:56;
then A \ {x} c< A by A8, XBOOLE_0:def_8;
then consider s being one-to-one FinSequence such that
A10: rng s = A \ {x} and
A11: for i, j being Nat st i in dom s & j in dom s & P1[s . i,s . j] holds
i < j by A5;
( <*x*> is one-to-one & rng <*x*> = {x} & {x} misses A \ {x} ) by FINSEQ_1:39, FINSEQ_3:93, XBOOLE_1:79;
then reconsider s9 = <*x*> ^ s as one-to-one FinSequence by A10, FINSEQ_3:91;
A12: {x} c= A by A8, ZFMISC_1:31;
A13: len <*x*> = 1 by FINSEQ_1:40;
thus S1[A] ::_thesis: verum
proof
take s9 ; ::_thesis: ( rng s9 = A & ( for i, j being Nat st i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] holds
i < j ) )
thus rng s9 = (rng <*x*>) \/ (rng s) by FINSEQ_1:31
.= {x} \/ (A \ {x}) by A10, FINSEQ_1:38
.= A by A12, XBOOLE_1:45 ; ::_thesis: for i, j being Nat st i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] holds
i < j
let i, j be Nat; ::_thesis: ( i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] implies i < j )
assume A14: ( i in dom s9 & j in dom s9 & P1[s9 . i,s9 . j] ) ; ::_thesis: i < j
A15: dom <*x*> = Seg 1 by FINSEQ_1:38;
percases ( ( i in dom <*x*> & j in dom <*x*> ) or ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) or ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) or ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ) by A13, A14, FINSEQ_1:25;
suppose ( i in dom <*x*> & j in dom <*x*> ) ; ::_thesis: i < j
then ( i = 1 & j = 1 ) by A15, FINSEQ_1:2, TARSKI:def_1;
then ( s9 . i = x & s9 . j = x ) by FINSEQ_1:41;
hence i < j by A8, A14; ::_thesis: verum
end;
supposeA16: ( i in dom <*x*> & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; ::_thesis: i < j
then A17: i = 1 by A15, FINSEQ_1:2, TARSKI:def_1;
consider n being Nat such that
A18: ( n in dom s & j = 1 + n ) by A16;
1 <= n by A18, FINSEQ_3:25;
hence i < j by A17, A18, NAT_1:13; ::_thesis: verum
end;
supposeA19: ( j in dom <*x*> & ex n being Nat st
( n in dom s & i = 1 + n ) ) ; ::_thesis: i < j
then j = 1 by A15, FINSEQ_1:2, TARSKI:def_1;
then A20: s9 . j = x by FINSEQ_1:41;
consider n being Nat such that
A21: ( n in dom s & i = 1 + n ) by A19;
s9 . i = s . n by A13, A21, FINSEQ_1:def_7;
then s9 . i in rng s by A21, FUNCT_1:def_3;
hence i < j by A8, A14, A20, A9, A10; ::_thesis: verum
end;
suppose ( ex n being Nat st
( n in dom s & i = 1 + n ) & ex n being Nat st
( n in dom s & j = 1 + n ) ) ; ::_thesis: i < j
then consider ni, nj being Nat such that
A22: ( ni in dom s & i = 1 + ni & nj in dom s & j = 1 + nj ) ;
( s9 . i = s . ni & s9 . j = s . nj ) by A13, A22, FINSEQ_1:def_7;
then ni < nj by A11, A14, A22;
hence i < j by A22, XREAL_1:6; ::_thesis: verum
end;
end;
end;
end;
end;
end;
thus S1[F1()] from ABCMIZ_A:sch_2(A4); ::_thesis: verum
end;
theorem Th2: :: ABCMIZ_A:2
for x being variable holds varcl (vars x) = vars x
proof
let x be variable; ::_thesis: varcl (vars x) = vars x
x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A1: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
vars x = varcl A by A1, MCART_1:7;
hence varcl (vars x) = vars x ; ::_thesis: verum
end;
theorem Th3: :: ABCMIZ_A:3
for C being initialized ConstructorSignature
for e being expression of C holds
( e is compound iff for x being Element of Vars holds not e = x -term C )
proof
let C be initialized ConstructorSignature; ::_thesis: for e being expression of C holds
( e is compound iff for x being Element of Vars holds not e = x -term C )
let e be expression of C; ::_thesis: ( e is compound iff for x being Element of Vars holds not e = x -term C )
( 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) ) by ABCMIZ_1:53;
hence ( e is compound iff for x being Element of Vars holds not e = x -term C ) ; ::_thesis: verum
end;
begin
registration
cluster empty Relation-like NAT -defined Vars -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like for Element of QuasiLoci ;
existence
ex b1 being quasi-loci st b1 is empty by ABCMIZ_1:29;
end;
definition
let C be ConstructorSignature;
attrC is standardized means :Def1: :: ABCMIZ_A:def 1
for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) );
end;
:: deftheorem Def1 defines standardized ABCMIZ_A:def_1_:_
for C being ConstructorSignature holds
( C is standardized iff for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) );
theorem Th4: :: ABCMIZ_A:4
for C being ConstructorSignature st C is standardized holds
for o being OperSymbol of C holds
( o is constructor iff o in Constructors )
proof
let C be ConstructorSignature; ::_thesis: ( C is standardized implies for o being OperSymbol of C holds
( o is constructor iff o in Constructors ) )
assume A1: C is standardized ; ::_thesis: for o being OperSymbol of C holds
( o is constructor iff o in Constructors )
let o be OperSymbol of C; ::_thesis: ( o is constructor iff o in Constructors )
thus ( o is constructor implies o in Constructors ) by A1, Def1; ::_thesis: ( o in Constructors implies o is constructor )
assume o in Constructors ; ::_thesis: o is constructor
then not o in {*,non_op} by ABCMIZ_1:39, XBOOLE_0:3;
hence ( o <> * & o <> non_op ) by TARSKI:def_2; :: according to ABCMIZ_1:def_11 ::_thesis: verum
end;
registration
cluster MaxConstrSign -> standardized ;
coherence
MaxConstrSign is standardized
proof
let o be OperSymbol of MaxConstrSign; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) )
A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24;
assume A2: o is constructor ; ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) )
then A3: ( the ResultSort of MaxConstrSign . o = o `1 & card ( the Arity of MaxConstrSign . o) = card ((o `2) `1) ) by ABCMIZ_1:def_24;
( o <> * & o <> non_op ) by A2, ABCMIZ_1:def_11;
then not o in {*,non_op} by TARSKI:def_2;
hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) by A3, A1, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
registration
cluster non empty non void V68() strict V146() constructor initialized standardized for ManySortedSign ;
existence
ex b1 being ConstructorSignature st
( b1 is initialized & b1 is standardized & b1 is strict )
proof
take MaxConstrSign ; ::_thesis: ( MaxConstrSign is initialized & MaxConstrSign is standardized & MaxConstrSign is strict )
thus ( MaxConstrSign is initialized & MaxConstrSign is standardized & MaxConstrSign is strict ) ; ::_thesis: verum
end;
end;
definition
let C be initialized standardized ConstructorSignature;
let c be constructor OperSymbol of C;
func loci_of c -> quasi-loci equals :: ABCMIZ_A:def 2
(c `2) `1 ;
coherence
(c `2) `1 is quasi-loci
proof
reconsider c = c as Element of Constructors by Th4;
loci_of c is quasi-loci ;
hence (c `2) `1 is quasi-loci ; ::_thesis: verum
end;
end;
:: deftheorem defines loci_of ABCMIZ_A:def_2_:_
for C being initialized standardized ConstructorSignature
for c being constructor OperSymbol of C holds loci_of c = (c `2) `1 ;
registration
let C be ConstructorSignature;
clusterV146() constructor for Subsignature of C;
existence
ex b1 being Subsignature of C st b1 is constructor
proof
reconsider S = C as Subsignature of C by INSTALG1:15;
take S ; ::_thesis: S is constructor
thus S is constructor ; ::_thesis: verum
end;
end;
registration
let C be initialized ConstructorSignature;
cluster non empty non void V68() V146() constructor initialized for Subsignature of C;
existence
ex b1 being constructor Subsignature of C st b1 is initialized
proof
reconsider S = C as constructor Subsignature of C by INSTALG1:15;
take S ; ::_thesis: S is initialized
thus S is initialized ; ::_thesis: verum
end;
end;
registration
let C be standardized ConstructorSignature;
cluster constructor -> constructor standardized for Subsignature of C;
coherence
for b1 being constructor Subsignature of C holds b1 is standardized
proof
let S be constructor Subsignature of C; ::_thesis: S is standardized
let o be OperSymbol of S; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) )
assume A1: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def_11 ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) )
A2: the carrier' of S c= the carrier' of C by INSTALG1:10;
o in the carrier' of S ;
then reconsider c = o as OperSymbol of C by A2;
A3: c is constructor by A1, ABCMIZ_1:def_11;
( the Arity of S = the Arity of C | the carrier' of S & the ResultSort of S = the ResultSort of C | the carrier' of S ) by INSTALG1:12;
then ( the_result_sort_of c = the_result_sort_of o & the_arity_of c = the_arity_of o ) by FUNCT_1:49;
hence ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) by A3, Def1; ::_thesis: verum
end;
end;
theorem :: ABCMIZ_A:5
for S1, S2 being standardized ConstructorSignature st the carrier' of S1 = the carrier' of S2 holds
ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
proof
let S1, S2 be standardized ConstructorSignature; ::_thesis: ( the carrier' of S1 = the carrier' of S2 implies ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) )
assume A1: the carrier' of S1 = the carrier' of S2 ; ::_thesis: ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #)
A2: ( the carrier of S1 = 3 & the carrier of S2 = 3 ) by ABCMIZ_1:def_9, YELLOW11:1;
now__::_thesis:_for_o_being_OperSymbol_of_S1_holds_the_Arity_of_S1_._o_=_the_Arity_of_S2_._o
let o be OperSymbol of S1; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1
reconsider o2 = o as OperSymbol of S2 by A1;
percases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def_11;
suppose ( o = * or o = non_op ) ; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1
then ( ( the Arity of S1 . o = <*an_Adj*> & the Arity of S2 . o = <*an_Adj*> ) or ( the Arity of S1 . o = <*an_Adj,a_Type*> & the Arity of S2 . o = <*an_Adj,a_Type*> ) ) by ABCMIZ_1:def_9;
hence the Arity of S1 . o = the Arity of S2 . o ; ::_thesis: verum
end;
suppose ( o is constructor & o2 is constructor ) ; ::_thesis: the Arity of S1 . b1 = the Arity of S2 . b1
then ( card ((o `2) `1) = len (the_arity_of o) & card ((o `2) `1) = len (the_arity_of o2) & the_arity_of o = (len (the_arity_of o)) |-> a_Term & the_arity_of o2 = (len (the_arity_of o2)) |-> a_Term ) by Def1, ABCMIZ_1:37;
hence the Arity of S1 . o = the_arity_of o2
.= the Arity of S2 . o ;
::_thesis: verum
end;
end;
end;
then A3: the Arity of S1 = the Arity of S2 by A1, A2, FUNCT_2:63;
now__::_thesis:_for_o_being_OperSymbol_of_S1_holds_the_ResultSort_of_S1_._o_=_the_ResultSort_of_S2_._o
let o be OperSymbol of S1; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1
reconsider o2 = o as OperSymbol of S2 by A1;
percases ( o = * or o = non_op or ( o is constructor & o2 is constructor ) ) by ABCMIZ_1:def_11;
suppose ( o = * or o = non_op ) ; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1
then ( ( the ResultSort of S1 . o = a_Type & the ResultSort of S2 . o = a_Type ) or ( the ResultSort of S1 . o = an_Adj & the ResultSort of S2 . o = an_Adj ) ) by ABCMIZ_1:def_9;
hence the ResultSort of S1 . o = the ResultSort of S2 . o ; ::_thesis: verum
end;
suppose ( o is constructor & o2 is constructor ) ; ::_thesis: the ResultSort of S1 . b1 = the ResultSort of S2 . b1
then ( the_result_sort_of o = o `1 & the_result_sort_of o2 = o `1 ) by Def1;
hence the ResultSort of S1 . o = the_result_sort_of o2
.= the ResultSort of S2 . o ;
::_thesis: verum
end;
end;
end;
hence ManySortedSign(# the carrier of S1, the carrier' of S1, the Arity of S1, the ResultSort of S1 #) = ManySortedSign(# the carrier of S2, the carrier' of S2, the Arity of S2, the ResultSort of S2 #) by A1, A2, A3, FUNCT_2:63; ::_thesis: verum
end;
theorem :: ABCMIZ_A:6
for C being ConstructorSignature holds
( C is standardized iff C is Subsignature of MaxConstrSign )
proof
let C be ConstructorSignature; ::_thesis: ( C is standardized iff C is Subsignature of MaxConstrSign )
A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24;
A2: dom the Arity of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def_1;
A3: dom the ResultSort of MaxConstrSign = the carrier' of MaxConstrSign by FUNCT_2:def_1;
thus ( C is standardized implies C is Subsignature of MaxConstrSign ) ::_thesis: ( C is Subsignature of MaxConstrSign implies C is standardized )
proof
assume A4: for o being OperSymbol of C st o is constructor holds
( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) ; :: according to ABCMIZ_A:def_1 ::_thesis: C is Subsignature of MaxConstrSign
A5: ( the carrier of C = 3 & the carrier of MaxConstrSign = 3 ) by ABCMIZ_1:def_9, YELLOW11:1;
A6: the Arity of C c= the Arity of MaxConstrSign
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the Arity of C or [x,y] in the Arity of MaxConstrSign )
assume A7: [x,y] in the Arity of C ; ::_thesis: [x,y] in the Arity of MaxConstrSign
then reconsider x = x as OperSymbol of C by ZFMISC_1:87;
( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def_11;
then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def_2;
then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def_3;
A8: y = the Arity of C . x by A7, FUNCT_1:1;
percases ( x = * or x = non_op or x is constructor ) by ABCMIZ_1:def_11;
suppose ( x = * or x = non_op ) ; ::_thesis: [x,y] in the Arity of MaxConstrSign
then ( ( c = * & y = <*an_Adj,a_Type*> ) or ( c = non_op & y = <*an_Adj*> ) ) by A8, ABCMIZ_1:def_9;
then y = the Arity of MaxConstrSign . c by ABCMIZ_1:def_9;
hence [x,y] in the Arity of MaxConstrSign by A2, FUNCT_1:def_2; ::_thesis: verum
end;
supposeA9: x is constructor ; ::_thesis: [x,y] in the Arity of MaxConstrSign
then A10: ( x <> * & x <> non_op ) by ABCMIZ_1:def_11;
then A11: c is constructor by ABCMIZ_1:def_11;
card ((x `2) `1) = len (the_arity_of x) by A4, A9
.= card y by A7, FUNCT_1:1 ;
then A12: card y = card ( the Arity of MaxConstrSign . c) by A11, ABCMIZ_1:def_24;
( y in {a_Term} * & the Arity of MaxConstrSign . c in {a_Term} * ) by A8, A10, ABCMIZ_1:def_9;
then y = the Arity of MaxConstrSign . c by A12, ABCMIZ_1:6;
hence [x,y] in the Arity of MaxConstrSign by A2, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
the ResultSort of C c= the ResultSort of MaxConstrSign
proof
let x, y be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [x,y] in the ResultSort of C or [x,y] in the ResultSort of MaxConstrSign )
assume A13: [x,y] in the ResultSort of C ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign
then reconsider x = x as OperSymbol of C by ZFMISC_1:87;
( x is constructor or x = * or x = non_op ) by ABCMIZ_1:def_11;
then ( x in {*,non_op} or x in Constructors ) by A4, TARSKI:def_2;
then reconsider c = x as OperSymbol of MaxConstrSign by A1, XBOOLE_0:def_3;
A14: y = the ResultSort of C . x by A13, FUNCT_1:1;
percases ( x = * or x = non_op or ( x is constructor & c is constructor ) ) by ABCMIZ_1:def_11;
suppose ( x = * or x = non_op ) ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign
then ( ( c = * & y = a_Type ) or ( c = non_op & y = an_Adj ) ) by A14, ABCMIZ_1:def_9;
then y = the ResultSort of MaxConstrSign . c by ABCMIZ_1:def_9;
hence [x,y] in the ResultSort of MaxConstrSign by A3, FUNCT_1:def_2; ::_thesis: verum
end;
supposeA15: ( x is constructor & c is constructor ) ; ::_thesis: [x,y] in the ResultSort of MaxConstrSign
then x `1 = the_result_sort_of x by A4
.= y by A13, FUNCT_1:1 ;
then y = the_result_sort_of c by A15, Def1
.= the ResultSort of MaxConstrSign . c ;
hence [x,y] in the ResultSort of MaxConstrSign by A3, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;
hence C is Subsignature of MaxConstrSign by A5, A6, INSTALG1:13; ::_thesis: verum
end;
assume A16: C is Subsignature of MaxConstrSign ; ::_thesis: C is standardized
let o be OperSymbol of C; :: according to ABCMIZ_A:def_1 ::_thesis: ( o is constructor implies ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) ) )
assume A17: ( o <> * & o <> non_op ) ; :: according to ABCMIZ_1:def_11 ::_thesis: ( o in Constructors & o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) )
( the carrier' of C c= the carrier' of MaxConstrSign & o in the carrier' of C ) by A16, INSTALG1:10;
then reconsider c = o as OperSymbol of MaxConstrSign ;
A18: c is constructor by A17, ABCMIZ_1:def_11;
not c in {*,non_op} by A17, TARSKI:def_2;
hence o in Constructors by A1, XBOOLE_0:def_3; ::_thesis: ( o `1 = the_result_sort_of o & card ((o `2) `1) = len (the_arity_of o) )
thus o `1 = the ResultSort of MaxConstrSign . c by A18, ABCMIZ_1:def_24
.= ( the ResultSort of MaxConstrSign | the carrier' of C) . o by FUNCT_1:49
.= the ResultSort of C . o by A16, INSTALG1:12
.= the_result_sort_of o ; ::_thesis: card ((o `2) `1) = len (the_arity_of o)
thus card ((o `2) `1) = card ( the Arity of MaxConstrSign . c) by A18, ABCMIZ_1:def_24
.= card (( the Arity of MaxConstrSign | the carrier' of C) . o) by FUNCT_1:49
.= card ( the Arity of C . o) by A16, INSTALG1:12
.= len (the_arity_of o) ; ::_thesis: verum
end;
registration
let C be initialized ConstructorSignature;
cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching non compound for expression of C, a_Term C;
existence
not for b1 being quasi-term of C holds b1 is compound
proof
set x = the Element of Vars ;
take the Element of Vars -term C ; ::_thesis: not the Element of Vars -term C is compound
thus not the Element of Vars -term C is compound ; ::_thesis: verum
end;
end;
registration
cluster -> pair for Element of Vars ;
coherence
for b1 being Element of Vars holds b1 is pair
proof
let x be Element of Vars ; ::_thesis: x is pair
( Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } & x in Vars ) by ABCMIZ_1:18;
then ex A being Subset of Vars ex j being Element of NAT st
( x = [(varcl A),j] & A is finite ) ;
hence x is pair ; ::_thesis: verum
end;
end;
theorem Th7: :: ABCMIZ_A:7
for x being Element of Vars st vars x is natural holds
vars x = 0
proof
let x be Element of Vars ; ::_thesis: ( vars x is natural implies vars x = 0 )
assume x `1 is natural ; ::_thesis: vars x = 0
then reconsider n = x `1 as Element of NAT by ORDINAL1:def_12;
( Vars = { [(varcl A),j] where A is Subset of Vars, j is Element of NAT : A is finite } & x in Vars ) by ABCMIZ_1:18;
then consider A being Subset of Vars, j being Element of NAT such that
A1: ( x = [(varcl A),j] & A is finite ) ;
set i = the Element of n;
assume A2: x `1 <> 0 ; ::_thesis: contradiction
then A3: the Element of n in n ;
reconsider i = the Element of n as Element of NAT by A2, ORDINAL1:10;
( n = varcl A & vars x c= Vars ) by A1, MCART_1:7;
then i in Vars by A3;
hence contradiction ; ::_thesis: verum
end;
theorem Th8: :: ABCMIZ_A:8
Vars misses Constructors
proof
assume Vars meets Constructors ; ::_thesis: contradiction
then consider x being set such that
A1: ( x in Vars & x in Constructors ) by XBOOLE_0:3;
reconsider x = x as Element of Vars by A1;
consider A being Subset of Vars, j being Element of NAT such that
A2: ( x = [(varcl A),j] & A is finite ) by A1, ABCMIZ_1:18;
( x in Modes \/ Attrs or x in Funcs ) by A1, XBOOLE_0:def_3;
then ( x in Modes or x in Attrs or x in Funcs ) by XBOOLE_0:def_3;
then ( x `2 in [:QuasiLoci,NAT:] & x `2 = j ) by A2, MCART_1:7, MCART_1:10;
then ex a, b being set st
( a in QuasiLoci & b in NAT & [a,b] = j ) by ZFMISC_1:def_2;
hence contradiction ; ::_thesis: verum
end;
theorem :: ABCMIZ_A:9
for x being Element of Vars holds
( x <> * & x <> non_op ) ;
theorem Th10: :: ABCMIZ_A:10
for C being standardized ConstructorSignature holds Vars misses the carrier' of C
proof
let C be standardized ConstructorSignature; ::_thesis: Vars misses the carrier' of C
assume Vars meets the carrier' of C ; ::_thesis: contradiction
then consider x being set such that
A1: ( x in Vars & x in the carrier' of C ) by XBOOLE_0:3;
reconsider x = x as Element of Vars by A1;
reconsider c = x as OperSymbol of C by A1;
( x = * or x = non_op or c is constructor ) by ABCMIZ_1:def_11;
then ( x = * or x = non_op or ( x in Constructors & Vars misses Constructors ) ) by Th8, Def1;
hence contradiction by XBOOLE_0:3; ::_thesis: verum
end;
theorem Th11: :: ABCMIZ_A:11
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
let e be expression of C; ::_thesis: ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
set X = MSVars C;
set Y = (MSVars C) \/ ( the carrier of C --> {0});
reconsider q = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
percases ( ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] or q . {} in [: the carrier' of C,{ the carrier of C}:] ) by MSATERM:2;
suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that
A1: q . {} = [v,s] ;
consider z being set such that
A2: ( z in dom the Sorts of (Free (C,(MSVars C))) & e in the Sorts of (Free (C,(MSVars C))) . z ) by CARD_5:2;
reconsider z = z as SortSymbol of C by A2;
the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9;
then A3: ( z = a_Type or z = an_Adj or z = a_Term ) by ENUMSET1:def_1;
A4: q = root-tree [v,s] by A1, MSATERM:5;
then A5: the_sort_of q = s by MSATERM:14;
A6: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) by MSAFREE3:24;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18;
then ( the Sorts of (Free (C,(MSVars C))) . z c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z & FreeMSA ((MSVars C) \/ ( the carrier of C --> {0})) = MSAlgebra(# (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))),(FreeOper ((MSVars C) \/ ( the carrier of C --> {0}))) #) ) by PBOOLE:def_2;
then ( q in the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z & the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . z = FreeSort (((MSVars C) \/ ( the carrier of C --> {0})),z) ) by A2, MSAFREE:def_11;
then A7: s = z by A5, MSATERM:def_5;
then v in (MSVars C) . z by A4, A2, A6, MSAFREE3:18;
then A8: ( v in Vars & z = a_Term ) by A3, ABCMIZ_1:def_25;
then reconsider x = v as Element of Vars ;
e = x -term C by A1, A7, A8, MSATERM:5;
hence ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by A1, A7, A8; ::_thesis: verum
end;
suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) )
then consider o, s being set such that
A9: ( o in the carrier' of C & s in { the carrier of C} & q . {} = [o,s] ) by ZFMISC_1:def_2;
reconsider o = o as OperSymbol of C by A9;
( o is constructor iff ( o <> * & o <> non_op ) ) by ABCMIZ_1:def_11;
then ( s = the carrier of C & ( o in Constructors or o = * or o = non_op ) ) by A9, Def1, TARSKI:def_1;
hence ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by A9; ::_thesis: verum
end;
end;
end;
registration
let C be initialized standardized ConstructorSignature;
let e be expression of C;
clustere . {} -> pair ;
coherence
e . {} is pair
proof
( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;
hence e . {} is pair ; ::_thesis: verum
end;
end;
theorem Th12: :: ABCMIZ_A:12
for C being initialized ConstructorSignature
for e being expression of C
for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
proof
let C be initialized ConstructorSignature; ::_thesis: for e being expression of C
for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
let e be expression of C; ::_thesis: for o being OperSymbol of C st e . {} = [o, the carrier of C] holds
e is expression of C, the_result_sort_of o
let o be OperSymbol of C; ::_thesis: ( e . {} = [o, the carrier of C] implies e is expression of C, the_result_sort_of o )
assume A1: e . {} = [o, the carrier of C] ; ::_thesis: e is expression of C, the_result_sort_of o
set X = MSVars C;
set Y = (MSVars C) \/ ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
variables_in t c= MSVars C by MSAFREE3:27;
then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ;
then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5;
then A2: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24;
the_sort_of t = the_result_sort_of o by A1, MSATERM:17;
hence e is expression of C, the_result_sort_of o by A2, ABCMIZ_1:def_28; ::_thesis: verum
end;
theorem Th13: :: ABCMIZ_A:13
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds
( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
let e be expression of C; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
percases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;
suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
then consider x being Element of Vars such that
A1: ( e = x -term C & e . {} = [x,a_Term] ) ;
thus ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A1, MCART_1:7; ::_thesis: verum
end;
suppose ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) )
then consider o being OperSymbol of C such that
A2: e . {} = [o, the carrier of C] ;
set X = MSVars C;
set Y = (MSVars C) \/ ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
variables_in t c= MSVars C by MSAFREE3:27;
then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ;
then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5;
then A3: e in the Sorts of (Free (C,(MSVars C))) . (the_sort_of t) by MSAFREE3:24;
A4: ( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38;
A5: ( (e . {}) `1 = o & non_op C = non_op & ast C = * ) by A2, MCART_1:7;
the_sort_of t = the_result_sort_of o by A2, MSATERM:17;
hence ( ( (e . {}) `1 = * implies e is expression of C, a_Type C ) & ( (e . {}) `1 = non_op implies e is expression of C, an_Adj C ) ) by A3, A4, A5, ABCMIZ_1:def_28; ::_thesis: verum
end;
end;
end;
theorem Th14: :: ABCMIZ_A:14
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds
( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
let e be expression of C; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
percases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;
suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
then consider x being Element of Vars such that
A1: ( e = x -term C & e . {} = [x,a_Term] ) ;
( (e . {}) `1 = x & (e . {}) `2 = a_Term ) by A1, MCART_1:7;
hence ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) by A1; ::_thesis: verum
end;
suppose ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) )
then consider o being OperSymbol of C such that
A2: ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ;
( (e . {}) `1 = o & (e . {}) `2 = the carrier of C ) by A2, MCART_1:7;
hence ( ( (e . {}) `1 in Vars & (e . {}) `2 = a_Term & e is quasi-term of C ) or ( (e . {}) `2 = the carrier of C & ( ( (e . {}) `1 in Constructors & (e . {}) `1 in the carrier' of C ) or (e . {}) `1 = * or (e . {}) `1 = non_op ) ) ) by A2; ::_thesis: verum
end;
end;
end;
theorem :: ABCMIZ_A:15
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Constructors holds
e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
let e be expression of C; ::_thesis: ( (e . {}) `1 in Constructors implies e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) )
assume A1: (e . {}) `1 in Constructors ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
percases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;
suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
then consider x being Element of Vars such that
A2: ( e = x -term C & e . {} = [x,a_Term] ) ;
(e . {}) `1 = x by A2, MCART_1:7;
hence e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) by A1, Th8, XBOOLE_0:3; ::_thesis: verum
end;
suppose ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1)
then consider o being OperSymbol of C such that
A3: e . {} = [o, the carrier of C] ;
A4: (e . {}) `1 = o by A3, MCART_1:7;
( * in {*,non_op} & non_op in {*,non_op} ) by TARSKI:def_2;
then ( o <> * & o <> non_op ) by A1, A4, ABCMIZ_1:39, XBOOLE_0:3;
then A5: o is constructor by ABCMIZ_1:def_11;
set X = MSVars C;
reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
A6: the_sort_of t = the_result_sort_of o by A3, MSATERM:17
.= o `1 by A5, Def1 ;
variables_in t c= MSVars C by MSAFREE3:27;
then e in { t1 where t1 is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t1 = the_sort_of t & variables_in t1 c= MSVars C ) } ;
then e in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_sort_of t) by MSAFREE3:def_5;
hence e in the Sorts of (Free (C,(MSVars C))) . (((e . {}) `1) `1) by A4, A6, MSAFREE3:23; ::_thesis: verum
end;
end;
end;
theorem :: ABCMIZ_A:16
for C being initialized standardized ConstructorSignature
for e being expression of C holds
( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C holds
( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
let e be expression of C; ::_thesis: ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C )
A1: ( (e . {}) `1 in Vars or (e . {}) `1 in the carrier' of C or (e . {}) `1 = ast C or (e . {}) `1 = non_op C ) by Th14;
Vars misses the carrier' of C by Th10;
hence ( not (e . {}) `1 in Vars iff (e . {}) `1 is OperSymbol of C ) by A1, XBOOLE_0:3; ::_thesis: verum
end;
theorem Th17: :: ABCMIZ_A:17
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Vars holds
ex x being Element of Vars st
( x = (e . {}) `1 & e = x -term C )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Vars holds
ex x being Element of Vars st
( x = (e . {}) `1 & e = x -term C )
let t be expression of C; ::_thesis: ( (t . {}) `1 in Vars implies ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) )
assume A1: (t . {}) `1 in Vars ; ::_thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
set X = MSVars C;
set V = (MSVars C) \/ ( the carrier of C --> {0});
reconsider q = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
percases ( q . {} in [: the carrier' of C,{ the carrier of C}:] or ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ) by MSATERM:2;
suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
then ( (q . {}) `1 in the carrier' of C & the carrier' of C misses Vars ) by Th10, MCART_1:10;
hence ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) by A1, XBOOLE_0:3; ::_thesis: verum
end;
suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C )
then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that
A2: t . {} = [v,s] ;
A3: q = root-tree [v,s] by A2, MSATERM:5;
reconsider x = v as Element of Vars by A1, A2, MCART_1:7;
take x ; ::_thesis: ( x = (t . {}) `1 & t = x -term C )
the carrier of C = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9;
then A4: ( s = a_Term or s = a_Type or s = an_Adj ) by ENUMSET1:def_1;
( the carrier of C --> {0}) . s = {0} by FUNCOP_1:7;
then ((MSVars C) \/ ( the carrier of C --> {0})) . s = ((MSVars C) . s) \/ {0} by PBOOLE:def_4;
then A5: ( s = a_Term or ((MSVars C) \/ ( the carrier of C --> {0})) . s = {} \/ {0} ) by A4, ABCMIZ_1:def_25;
( v in ((MSVars C) \/ ( the carrier of C --> {0})) . s & x <> 0 ) ;
hence ( x = (t . {}) `1 & t = x -term C ) by A2, A3, A5, MCART_1:7; ::_thesis: verum
end;
end;
end;
theorem Th18: :: ABCMIZ_A:18
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 = * holds
ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 = * holds
ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
let e be expression of C; ::_thesis: ( (e . {}) `1 = * implies ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q) )
assume A1: (e . {}) `1 = * ; ::_thesis: ex a being expression of C, an_Adj C ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
for x being Element of Vars holds
( not e = x -term C or not e . {} = [x,a_Term] ) by A1, MCART_1:7;
then consider o being OperSymbol of C such that
A2: e . {} = [o, the carrier of C] and
( o in Constructors or o = * or o = non_op ) by Th11;
set Y = (MSVars C) \/ ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
consider aa being ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) such that
A3: t = [o, the carrier of C] -tree aa by A2, MSATERM:10;
A4: * = [o, the carrier of C] `1 by A1, A3, TREES_4:def_4
.= o ;
A5: the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by ABCMIZ_1:38;
A6: len aa = len (the_arity_of o) by MSATERM:22
.= 2 by A4, A5, FINSEQ_1:44 ;
then dom aa = Seg 2 by FINSEQ_1:def_3;
then A7: ( 1 in dom aa & 2 in dom aa ) ;
then reconsider t1 = aa . 1, t2 = aa . 2 as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSATERM:22;
A8: len (doms aa) = len aa by TREES_3:38;
( (doms aa) . 1 = dom t1 & (doms aa) . 2 = dom t2 ) by A7, FUNCT_6:22;
then A9: ( 0 < 2 & 0 + 1 = 1 & 1 < 2 & 1 + 1 = 2 & {} in (doms aa) . 1 & {} in (doms aa) . 2 & <*0*> ^ (<*> NAT) = <*0*> & <*1*> ^ (<*> NAT) = <*1*> ) by FINSEQ_1:34, TREES_1:22;
dom t = tree (doms aa) by A3, TREES_4:10;
then reconsider 00 = <*0*>, 01 = <*1*> as Element of dom t by A6, A8, A9, TREES_3:def_15;
( 0 < 2 & 1 = 0 + 1 & 1 < 2 & 2 = 1 + 1 & aa is DTree-yielding ) ;
then ( t1 = t | 00 & t2 = t | 01 ) by A3, A6, TREES_4:def_4;
then A10: ( t1 is expression of C & t2 is expression of C & variables_in t1 c= variables_in t & variables_in t2 c= variables_in t ) by MSAFREE3:32, MSAFREE3:33;
then A11: ( variables_in t1 c= MSVars C & variables_in t2 c= MSVars C ) by MSAFREE3:27;
the_sort_of t1 = (the_arity_of o) . 1 by A7, MSATERM:23
.= an_Adj C by A4, A5, FINSEQ_1:44 ;
then t1 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) } by A11;
then t1 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def_5;
then t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24;
then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def_28;
the_sort_of t2 = (the_arity_of o) . 2 by A7, MSATERM:23
.= a_Type C by A4, A5, FINSEQ_1:44 ;
then t2 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = a_Type C & variables_in s c= MSVars C ) } by A11;
then t2 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Type C) by MSAFREE3:def_5;
then t2 in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by MSAFREE3:24;
then reconsider q = t2 as expression of C, a_Type C by A10, ABCMIZ_1:def_28;
take a ; ::_thesis: ex q being expression of C, a_Type C st e = [*,3] -tree (a,q)
take q ; ::_thesis: e = [*,3] -tree (a,q)
A12: the carrier of C = 3 by ABCMIZ_1:def_9, YELLOW11:1;
aa = <*a,q*> by A6, FINSEQ_1:44;
hence e = [*,3] -tree (a,q) by A3, A4, A12, TREES_4:def_6; ::_thesis: verum
end;
theorem Th19: :: ABCMIZ_A:19
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 = non_op holds
ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 = non_op holds
ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
let e be expression of C; ::_thesis: ( (e . {}) `1 = non_op implies ex a being expression of C, an_Adj C st e = [non_op,3] -tree a )
assume A1: (e . {}) `1 = non_op ; ::_thesis: ex a being expression of C, an_Adj C st e = [non_op,3] -tree a
for x being Element of Vars holds
( not e = x -term C or not e . {} = [x,a_Term] ) by A1, MCART_1:7;
then consider o being OperSymbol of C such that
A2: e . {} = [o, the carrier of C] and
( o in Constructors or o = * or o = non_op ) by Th11;
set Y = (MSVars C) \/ ( the carrier of C --> {0});
reconsider t = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
consider aa being ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) such that
A3: t = [o, the carrier of C] -tree aa by A2, MSATERM:10;
A4: non_op = [o, the carrier of C] `1 by A1, A3, TREES_4:def_4
.= o ;
A5: the_arity_of (non_op C) = <*(an_Adj C)*> by ABCMIZ_1:38;
A6: len aa = len (the_arity_of o) by MSATERM:22
.= 1 by A4, A5, FINSEQ_1:40 ;
then dom aa = Seg 1 by FINSEQ_1:def_3;
then A7: 1 in dom aa ;
then reconsider t1 = aa . 1 as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSATERM:22;
A8: len (doms aa) = len aa by TREES_3:38;
(doms aa) . 1 = dom t1 by A7, FUNCT_6:22;
then A9: ( 0 < 1 & 0 + 1 = 1 & {} in (doms aa) . 1 & <*0*> ^ (<*> NAT) = <*0*> ) by FINSEQ_1:34, TREES_1:22;
dom t = tree (doms aa) by A3, TREES_4:10;
then reconsider 00 = <*0*> as Element of dom t by A6, A8, A9, TREES_3:def_15;
t1 = t | 00 by A3, A6, A9, TREES_4:def_4;
then A10: ( t1 is expression of C & variables_in t1 c= variables_in t ) by MSAFREE3:32, MSAFREE3:33;
then A11: variables_in t1 c= MSVars C by MSAFREE3:27;
the_sort_of t1 = (the_arity_of o) . 1 by A7, MSATERM:23
.= an_Adj C by A4, A5, FINSEQ_1:40 ;
then t1 in { s where s is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of s = an_Adj C & variables_in s c= MSVars C ) } by A11;
then t1 in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (an_Adj C) by MSAFREE3:def_5;
then t1 in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by MSAFREE3:24;
then reconsider a = t1 as expression of C, an_Adj C by A10, ABCMIZ_1:def_28;
take a ; ::_thesis: e = [non_op,3] -tree a
A12: the carrier of C = 3 by ABCMIZ_1:def_9, YELLOW11:1;
aa = <*a*> by A6, FINSEQ_1:40;
hence e = [non_op,3] -tree a by A3, A4, A12, TREES_4:def_5; ::_thesis: verum
end;
theorem Th20: :: ABCMIZ_A:20
for C being initialized standardized ConstructorSignature
for e being expression of C st (e . {}) `1 in Constructors holds
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for e being expression of C st (e . {}) `1 in Constructors holds
ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
let e be expression of C; ::_thesis: ( (e . {}) `1 in Constructors implies ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) )
assume A1: (e . {}) `1 in Constructors ; ::_thesis: ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
percases ( ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) or ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ) by Th11;
suppose ex x being Element of Vars st
( e = x -term C & e . {} = [x,a_Term] ) ; ::_thesis: ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
then consider x being Element of Vars such that
A2: ( e = x -term C & e . {} = [x,a_Term] ) ;
( (e . {}) `1 = x & x in Vars ) by A2, MCART_1:7;
hence ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o ) by A1, Th8, XBOOLE_0:3; ::_thesis: verum
end;
suppose ex o being OperSymbol of C st
( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ; ::_thesis: ex o being OperSymbol of C st
( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
then consider o being OperSymbol of C such that
A3: ( e . {} = [o, the carrier of C] & ( o in Constructors or o = * or o = non_op ) ) ;
take o ; ::_thesis: ( o = (e . {}) `1 & the_result_sort_of o = o `1 & e is expression of C, the_result_sort_of o )
A4: ( (e . {}) `1 = o & (e . {}) `2 = the carrier of C ) by A3, MCART_1:7;
( * in {*,non_op} & non_op in {*,non_op} ) by TARSKI:def_2;
then ( o <> * & o <> non_op ) by A1, A4, ABCMIZ_1:39, XBOOLE_0:3;
then o is constructor by ABCMIZ_1:def_11;
hence ( o = (e . {}) `1 & the_result_sort_of o = o `1 ) by A3, Def1, MCART_1:7; ::_thesis: e is expression of C, the_result_sort_of o
set X = MSVars C;
set V = (MSVars C) \/ ( the carrier of C --> {0});
reconsider q = e as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
A5: variables_in q c= MSVars C by MSAFREE3:27;
A6: the_sort_of q = the_result_sort_of o by A3, MSATERM:17;
the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) = (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (the_result_sort_of o) by MSAFREE3:24
.= { a where a is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of a = the_result_sort_of o & variables_in a c= MSVars C ) } by MSAFREE3:def_5 ;
hence e in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A5, A6; :: according to ABCMIZ_1:def_28 ::_thesis: verum
end;
end;
end;
theorem Th21: :: ABCMIZ_A:21
for C being initialized standardized ConstructorSignature
for t being quasi-term of C holds
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for t being quasi-term of C holds
( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
set X = MSVars C;
set V = (MSVars C) \/ ( the carrier of C --> {0});
let t be quasi-term of C; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
( C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) & the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) ) by MSAFREE3:24, PBOOLE:def_18;
then A1: ( FreeMSA ((MSVars C) \/ ( the carrier of C --> {0})) = MSAlgebra(# (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))),(FreeOper ((MSVars C) \/ ( the carrier of C --> {0}))) #) & (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Term C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Term C) & t in (C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0})))) . (a_Term C) ) by ABCMIZ_1:def_28, PBOOLE:def_2;
then t in (FreeSort ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Term C) ;
then A2: t in FreeSort (((MSVars C) \/ ( the carrier of C --> {0})),(a_Term C)) by MSAFREE:def_11;
A3: ( (MSVars C) . a_Term = Vars & a_Term C = a_Term & a_Term = 2 ) by ABCMIZ_1:def_25;
reconsider q = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
percases ( ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] or q . {} in [: the carrier' of C,{ the carrier of C}:] ) by MSATERM:2;
suppose ex s being SortSymbol of C ex v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s st q . {} = [v,s] ; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
then consider s being SortSymbol of C, v being Element of ((MSVars C) \/ ( the carrier of C --> {0})) . s such that
A4: t . {} = [v,s] ;
A5: ( q = root-tree [v,s] & the_sort_of q = a_Term C ) by A2, A4, MSATERM:5, MSATERM:def_5;
then A6: ( a_Term C = s & (t . {}) `1 = v ) by A4, MCART_1:7, MSATERM:14;
then reconsider x = v as Element of Vars by A3, A5, A1, MSAFREE3:18;
( q = x -term C & vars x <> 2 ) by A5, A6, Th7;
hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A6; ::_thesis: verum
end;
suppose q . {} in [: the carrier' of C,{ the carrier of C}:] ; ::_thesis: ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) )
then consider o, k being set such that
A7: ( o in the carrier' of C & k in { the carrier of C} & q . {} = [o,k] ) by ZFMISC_1:def_2;
reconsider o = o as OperSymbol of C by A7;
k = the carrier of C by A7, TARSKI:def_1;
then A8: the_result_sort_of o = the_sort_of q by A7, MSATERM:17
.= a_Term C by A1, MSAFREE3:17 ;
then ( o <> ast C & o <> non_op C ) by ABCMIZ_1:38;
then A9: o is constructor by ABCMIZ_1:def_11;
then A10: a_Term C = o `1 by A8, Def1
.= ((q . {}) `1) `1 by A7, MCART_1:7 ;
A11: (q . {}) `1 = o by A7, MCART_1:7;
now__::_thesis:_for_x_being_Element_of_Vars_holds_not_q_=_x_-term_C
given x being Element of Vars such that A12: q = x -term C ; ::_thesis: contradiction
q . {} = [x,a_Term] by A12, TREES_4:3;
then k = a_Term by A7, XTUPLE_0:1;
then 2 = the carrier of C by A7, TARSKI:def_1;
hence contradiction by ABCMIZ_1:def_9, YELLOW11:1; ::_thesis: verum
end;
hence ( t is compound iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) ) by A9, A10, A11, Th3, Def1; ::_thesis: verum
end;
end;
end;
theorem Th22: :: ABCMIZ_A:22
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds
( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
let t be expression of C; ::_thesis: ( t is non compound quasi-term of C iff (t . {}) `1 in Vars )
hereby ::_thesis: ( (t . {}) `1 in Vars implies t is non compound quasi-term of C )
assume t is non compound quasi-term of C ; ::_thesis: (t . {}) `1 in Vars
then consider x being Element of Vars such that
A1: t = x -term C by Th3;
( t . {} = [x,a_Term] & x in Vars ) by A1, TREES_4:3;
hence (t . {}) `1 in Vars by MCART_1:7; ::_thesis: verum
end;
assume (t . {}) `1 in Vars ; ::_thesis: t is non compound quasi-term of C
then ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) by Th17;
hence t is non compound quasi-term of C ; ::_thesis: verum
end;
theorem :: ABCMIZ_A:23
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds
( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
let t be expression of C; ::_thesis: ( t is quasi-term of C iff ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) )
hereby ::_thesis: ( ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) implies t is quasi-term of C )
assume t is quasi-term of C ; ::_thesis: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars )
then reconsider tr = t as quasi-term of C ;
( tr is compound or not tr is compound ) ;
hence ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) by Th21, Th22; ::_thesis: verum
end;
assume that
A1: ( ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) or (t . {}) `1 in Vars ) and
A2: t is not quasi-term of C ; ::_thesis: contradiction
A3: ( (t . {}) `1 in Vars implies ex x being Element of Vars st
( x = (t . {}) `1 & t = x -term C ) ) by Th17;
then ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Term ) by A1, A2;
then ex o being OperSymbol of C st
( o = (t . {}) `1 & the_result_sort_of o = o `1 & t is expression of C, the_result_sort_of o ) by Th20;
hence contradiction by A2, A3, A1; ::_thesis: verum
end;
theorem Th24: :: ABCMIZ_A:24
for C being initialized standardized ConstructorSignature
for a being expression of C holds
( a is positive quasi-adjective of C iff ( (a . {}) `1 in Constructors & ((a . {}) `1) `1 = an_Adj ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for a being expression of C holds
( a is positive quasi-adjective of C iff ( (a . {}) `1 in Constructors & ((a . {}) `1) `1 = an_Adj ) )
set X = MSVars C;
set V = (MSVars C) \/ ( the carrier of C --> {0});
let t be expression of C; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) )
consider A being MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) such that
A1: ( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) \/ ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def_1;
the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSUALG_2:def_9;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18;
then A2: the Sorts of (Free (C,(MSVars C))) . (an_Adj C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (an_Adj C) by PBOOLE:def_2;
percases ( ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op ) by Th14;
suppose ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) )
hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by Th8, ABCMIZ_1:77, XBOOLE_0:3; ::_thesis: verum
end;
supposethat A3: (t . {}) `2 = the carrier of C and
A4: (t . {}) `1 in Constructors and
A5: (t . {}) `1 in the carrier' of C ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) )
reconsider o = (t . {}) `1 as OperSymbol of C by A5;
reconsider tt = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def_2;
then o is constructor by ABCMIZ_1:def_11;
then A6: o `1 = the_result_sort_of o by Def1;
A7: t . {} = [o,((t . {}) `2)] by Th1;
then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17;
hereby ::_thesis: ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj implies t is positive quasi-adjective of C )
assume t is positive quasi-adjective of C ; ::_thesis: ( (t . {}) `1 in Constructors & not ((t . {}) `1) `1 <> an_Adj )
then A9: t in the Sorts of (Free (C,(MSVars C))) . (an_Adj C) by ABCMIZ_1:def_28;
thus (t . {}) `1 in Constructors by A4; ::_thesis: not ((t . {}) `1) `1 <> an_Adj
assume ((t . {}) `1) `1 <> an_Adj ; ::_thesis: contradiction
hence contradiction by A2, A9, A6, A8, MSAFREE3:7; ::_thesis: verum
end;
assume (t . {}) `1 in Constructors ; ::_thesis: ( not ((t . {}) `1) `1 = an_Adj or t is positive quasi-adjective of C )
assume ((t . {}) `1) `1 = an_Adj ; ::_thesis: t is positive quasi-adjective of C
then reconsider t = t as expression of C, an_Adj C by A3, A6, A7, Th12;
t is positive
proof
given a being expression of C, an_Adj C such that A10: t = (non_op C) term a ; :: according to ABCMIZ_1:def_37 ::_thesis: contradiction
t = [non_op, the carrier of C] -tree <*a*> by A10, ABCMIZ_1:43;
then t . {} = [non_op, the carrier of C] by TREES_4:def_4;
then (t . {}) `1 = non_op by MCART_1:7;
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
hence contradiction by A4, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum
end;
hence t is positive quasi-adjective of C ; ::_thesis: verum
end;
supposeA11: (t . {}) `1 = * ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) )
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
A13: t = [*,3] -tree (a,q) by A11, Th18;
t = [*,3] -tree <*a,q*> by A13, TREES_4:def_6;
then t . {} = [*,3] by TREES_4:def_4;
then (t . {}) `1 = * by MCART_1:7;
then ( t is expression of C, a_Type C & a_Type C = a_Type & a_Type = 0 & an_Adj C = an_Adj & an_Adj = 1 ) by Th13;
hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A12, ABCMIZ_1:48; ::_thesis: verum
end;
supposeA14: (t . {}) `1 = non_op ; ::_thesis: ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) )
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
then A15: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C such that
A16: t = [non_op,3] -tree a by A14, Th19;
t = [non_op,3] -tree <*a*> by A16, TREES_4:def_5
.= [non_op, the carrier of C] -tree <*a*> by ABCMIZ_1:def_9, YELLOW11:1
.= (non_op C) term a by ABCMIZ_1:43 ;
hence ( t is positive quasi-adjective of C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = an_Adj ) ) by A15, ABCMIZ_1:def_37; ::_thesis: verum
end;
end;
end;
theorem :: ABCMIZ_A:25
for C being initialized standardized ConstructorSignature
for a being quasi-adjective of C holds
( a is negative iff (a . {}) `1 = non_op )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for a being quasi-adjective of C holds
( a is negative iff (a . {}) `1 = non_op )
let t be quasi-adjective of C; ::_thesis: ( t is negative iff (t . {}) `1 = non_op )
percases ( t is positive expression of C, an_Adj C or t is negative expression of C, an_Adj C ) ;
supposeA1: t is positive expression of C, an_Adj C ; ::_thesis: ( t is negative iff (t . {}) `1 = non_op )
then ( (t . {}) `1 in Constructors & non_op in {*,non_op} ) by Th24, TARSKI:def_2;
hence ( t is negative iff (t . {}) `1 = non_op ) by A1, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum
end;
supposeA2: t is negative expression of C, an_Adj C ; ::_thesis: ( t is negative iff (t . {}) `1 = non_op )
then consider a being expression of C, an_Adj C such that
A3: ( a is positive & t = (non_op C) term a ) by ABCMIZ_1:def_38;
t = [non_op, the carrier of C] -tree <*a*> by A3, ABCMIZ_1:43;
then t . {} = [non_op, the carrier of C] by TREES_4:def_4;
hence ( t is negative iff (t . {}) `1 = non_op ) by A2, MCART_1:7; ::_thesis: verum
end;
end;
end;
theorem :: ABCMIZ_A:26
for C being initialized standardized ConstructorSignature
for t being expression of C holds
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
proof
let C be initialized standardized ConstructorSignature; ::_thesis: for t being expression of C holds
( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
set X = MSVars C;
set V = (MSVars C) \/ ( the carrier of C --> {0});
let t be expression of C; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
consider A being MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) such that
A1: ( Free (C,(MSVars C)) = GenMSAlg A & A = (Reverse ((MSVars C) \/ ( the carrier of C --> {0}))) "" (MSVars C) ) by MSAFREE3:def_1;
the Sorts of (Free (C,(MSVars C))) is MSSubset of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSUALG_2:def_9;
then the Sorts of (Free (C,(MSVars C))) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) by PBOOLE:def_18;
then A2: the Sorts of (Free (C,(MSVars C))) . (a_Type C) c= the Sorts of (FreeMSA ((MSVars C) \/ ( the carrier of C --> {0}))) . (a_Type C) by PBOOLE:def_2;
percases ( ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) or ( (t . {}) `2 = the carrier of C & (t . {}) `1 in Constructors & (t . {}) `1 in the carrier' of C ) or (t . {}) `1 = * or (t . {}) `1 = non_op ) by Th14;
suppose ( (t . {}) `1 in Vars & (t . {}) `2 = a_Term & t is quasi-term of C ) ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by Th8, ABCMIZ_1:48, XBOOLE_0:3; ::_thesis: verum
end;
supposethat A3: (t . {}) `2 = the carrier of C and
A4: (t . {}) `1 in Constructors and
A5: (t . {}) `1 in the carrier' of C ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
reconsider o = (t . {}) `1 as OperSymbol of C by A5;
reconsider tt = t as Term of C,((MSVars C) \/ ( the carrier of C --> {0})) by MSAFREE3:8;
not o in {*,non_op} by A4, ABCMIZ_1:39, XBOOLE_0:3;
then ( o <> * & o <> non_op ) by TARSKI:def_2;
then o is constructor by ABCMIZ_1:def_11;
then A6: o `1 = the_result_sort_of o by Def1;
A7: t . {} = [o,((t . {}) `2)] by Th1;
then A8: the_sort_of tt = the_result_sort_of o by A3, MSATERM:17;
hereby ::_thesis: ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type implies t is pure expression of C, a_Type C )
assume t is pure expression of C, a_Type C ; ::_thesis: ( (t . {}) `1 in Constructors & not ((t . {}) `1) `1 <> a_Type )
then A9: t in the Sorts of (Free (C,(MSVars C))) . (a_Type C) by ABCMIZ_1:def_28;
thus (t . {}) `1 in Constructors by A4; ::_thesis: not ((t . {}) `1) `1 <> a_Type
assume ((t . {}) `1) `1 <> a_Type ; ::_thesis: contradiction
hence contradiction by A2, A9, A6, A8, MSAFREE3:7; ::_thesis: verum
end;
assume (t . {}) `1 in Constructors ; ::_thesis: ( not ((t . {}) `1) `1 = a_Type or t is pure expression of C, a_Type C )
assume ((t . {}) `1) `1 = a_Type ; ::_thesis: t is pure expression of C, a_Type C
then reconsider t = t as expression of C, a_Type C by A3, A7, Th12, A6;
t is pure
proof
given a being expression of C, an_Adj C, q being expression of C, a_Type C such that A10: t = (ast C) term (a,q) ; :: according to ABCMIZ_1:def_41 ::_thesis: contradiction
t = [*, the carrier of C] -tree <*a,q*> by A10, ABCMIZ_1:46;
then t . {} = [*, the carrier of C] by TREES_4:def_4;
then (t . {}) `1 = * by MCART_1:7;
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
hence contradiction by A4, ABCMIZ_1:39, XBOOLE_0:3; ::_thesis: verum
end;
hence t is pure expression of C, a_Type C ; ::_thesis: verum
end;
supposeA11: (t . {}) `1 = * ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
then A12: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C, q being expression of C, a_Type C such that
A13: t = [*,3] -tree (a,q) by A11, Th18;
t = [*,3] -tree <*a,q*> by A13, TREES_4:def_6
.= [*, the carrier of C] -tree <*a,q*> by ABCMIZ_1:def_9, YELLOW11:1
.= (ast C) term (a,q) by ABCMIZ_1:46 ;
hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by A12, ABCMIZ_1:def_41; ::_thesis: verum
end;
supposeA14: (t . {}) `1 = non_op ; ::_thesis: ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) )
then (t . {}) `1 in {*,non_op} by TARSKI:def_2;
then A15: not (t . {}) `1 in Constructors by ABCMIZ_1:39, XBOOLE_0:3;
consider a being expression of C, an_Adj C such that
A16: t = [non_op,3] -tree a by A14, Th19;
t = [non_op,3] -tree <*a*> by A16, TREES_4:def_5;
then t . {} = [non_op,3] by TREES_4:def_4;
then (t . {}) `1 = non_op by MCART_1:7;
then t is expression of C, an_Adj C by Th13;
hence ( t is pure expression of C, a_Type C iff ( (t . {}) `1 in Constructors & ((t . {}) `1) `1 = a_Type ) ) by A15, ABCMIZ_1:48; ::_thesis: verum
end;
end;
end;
begin
set MC = MaxConstrSign ;
definition
mode expression is expression of MaxConstrSign;
mode valuation is valuation of MaxConstrSign;
mode quasi-adjective is quasi-adjective of MaxConstrSign;
func QuasiAdjs -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 3
QuasiAdjs MaxConstrSign;
coherence
QuasiAdjs MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;
mode quasi-term is quasi-term of MaxConstrSign;
func QuasiTerms -> Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) equals :: ABCMIZ_A:def 4
QuasiTerms MaxConstrSign;
coherence
QuasiTerms MaxConstrSign is Subset of (Free (MaxConstrSign,(MSVars MaxConstrSign))) ;
mode quasi-type is quasi-type of MaxConstrSign ;
func QuasiTypes -> set equals :: ABCMIZ_A:def 5
QuasiTypes MaxConstrSign;
coherence
QuasiTypes MaxConstrSign is set ;
end;
:: deftheorem defines QuasiAdjs ABCMIZ_A:def_3_:_
QuasiAdjs = QuasiAdjs MaxConstrSign;
:: deftheorem defines QuasiTerms ABCMIZ_A:def_4_:_
QuasiTerms = QuasiTerms MaxConstrSign;
:: deftheorem defines QuasiTypes ABCMIZ_A:def_5_:_
QuasiTypes = QuasiTypes MaxConstrSign;
registration
cluster QuasiAdjs -> non empty ;
coherence
not QuasiAdjs is empty ;
cluster QuasiTerms -> non empty ;
coherence
not QuasiTerms is empty ;
cluster QuasiTypes -> non empty ;
coherence
not QuasiTypes is empty ;
end;
definition
:: original: Modes
redefine func Modes -> non empty Subset of Constructors;
coherence
Modes is non empty Subset of Constructors
proof
( Modes c= Modes \/ Attrs & Modes \/ Attrs c= Constructors ) by XBOOLE_1:7;
hence Modes is non empty Subset of Constructors by XBOOLE_1:1; ::_thesis: verum
end;
:: original: Attrs
redefine func Attrs -> non empty Subset of Constructors;
coherence
Attrs is non empty Subset of Constructors
proof
( Attrs c= Modes \/ Attrs & Modes \/ Attrs c= Constructors ) by XBOOLE_1:7;
hence Attrs is non empty Subset of Constructors by XBOOLE_1:1; ::_thesis: verum
end;
:: original: Funcs
redefine func Funcs -> non empty Subset of Constructors;
coherence
Funcs is non empty Subset of Constructors by XBOOLE_1:7;
end;
definition
func set-constr -> Element of Modes equals :: ABCMIZ_A:def 6
[a_Type,[{},0]];
coherence
[a_Type,[{},0]] is Element of Modes
proof
( a_Type in {a_Type} & [{},0] in [:QuasiLoci,NAT:] ) by ABCMIZ_1:29, TARSKI:def_1, ZFMISC_1:def_2;
hence [a_Type,[{},0]] is Element of Modes by ZFMISC_1:def_2; ::_thesis: verum
end;
end;
:: deftheorem defines set-constr ABCMIZ_A:def_6_:_
set-constr = [a_Type,[{},0]];
theorem :: ABCMIZ_A:27
( kind_of set-constr = a_Type & loci_of set-constr = {} & index_of set-constr = 0 )
proof
set-constr `2 = [{},0] by MCART_1:7;
hence ( kind_of set-constr = a_Type & loci_of set-constr = {} & index_of set-constr = 0 ) by MCART_1:7; ::_thesis: verum
end;
theorem Th28: :: ABCMIZ_A:28
Constructors = [:{a_Type,an_Adj,a_Term},[:QuasiLoci,NAT:]:]
proof
thus Constructors = ([:{a_Type},[:QuasiLoci,NAT:]:] \/ [:{an_Adj},[:QuasiLoci,NAT:]:]) \/ Funcs
.= [:({a_Type} \/ {an_Adj}),[:QuasiLoci,NAT:]:] \/ Funcs by ZFMISC_1:97
.= [:{a_Type,an_Adj},[:QuasiLoci,NAT:]:] \/ Funcs by ENUMSET1:1
.= [:({a_Type,an_Adj} \/ {a_Term}),[:QuasiLoci,NAT:]:] by ZFMISC_1:97
.= [:{a_Type,an_Adj,a_Term},[:QuasiLoci,NAT:]:] by ENUMSET1:3 ; ::_thesis: verum
end;
theorem Th29: :: ABCMIZ_A:29
for i being Nat
for l being quasi-loci holds
( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
proof
let i be Nat; ::_thesis: for l being quasi-loci holds
( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
let l be quasi-loci; ::_thesis: ( [(rng l),i] in Vars & l ^ <*[(rng l),i]*> is quasi-loci )
varcl (rng l) = rng l by ABCMIZ_1:33;
hence [(rng l),i] in Vars by ABCMIZ_1:17; ::_thesis: l ^ <*[(rng l),i]*> is quasi-loci
then reconsider x = [(rng l),i] as variable ;
( rng l in {(rng l),i} & {(rng l),i} in x ) by TARSKI:def_2;
then ( vars x = rng l & x nin rng l ) by MCART_1:7, XREGULAR:7;
hence l ^ <*[(rng l),i]*> is quasi-loci by ABCMIZ_1:31; ::_thesis: verum
end;
theorem Th30: :: ABCMIZ_A:30
for i being Nat ex l being quasi-loci st len l = i
proof
let i be Nat; ::_thesis: ex l being quasi-loci st len l = i
defpred S1[ Nat] means ex l being quasi-loci st len l = $1;
( <*> Vars is quasi-loci & len (<*> Vars) = 0 ) by ABCMIZ_1:29;
then A1: S1[ 0 ] ;
A2: for j being Nat st S1[j] holds
S1[j + 1]
proof
let j be Nat; ::_thesis: ( S1[j] implies S1[j + 1] )
given l being quasi-loci such that A3: len l = j ; ::_thesis: S1[j + 1]
reconsider l1 = l ^ <*[(rng l),1]*> as quasi-loci by Th29;
take l1 ; ::_thesis: len l1 = j + 1
thus len l1 = j + 1 by A3, FINSEQ_2:16; ::_thesis: verum
end;
for j being Nat holds S1[j] from NAT_1:sch_2(A1, A2);
hence ex l being quasi-loci st len l = i ; ::_thesis: verum
end;
theorem Th31: :: ABCMIZ_A:31
for X being finite Subset of Vars ex l being quasi-loci st rng l = varcl X
proof
let X be finite Subset of Vars; ::_thesis: ex l being quasi-loci st rng l = varcl X
reconsider Y = varcl X as finite Subset of Vars by ABCMIZ_1:24;
defpred S1[ set , set ] means $1 in $2 `1 ;
A1: for x, y being set st x in Y & y in Y & S1[x,y] holds
not S1[y,x]
proof
let x, y be set ; ::_thesis: ( x in Y & y in Y & S1[x,y] implies not S1[y,x] )
assume A2: ( x in Y & y in Y & S1[x,y] & S1[y,x] ) ; ::_thesis: contradiction
x in Vars by A2;
then consider A being Subset of Vars, j being Element of NAT such that
A3: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
y in Vars by A2;
then consider B being Subset of Vars, k being Element of NAT such that
A4: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
A5: ( y in varcl A & x in varcl B ) by A2, A3, A4, MCART_1:7;
A6: ( varcl A in {(varcl A)} & varcl B in {(varcl B)} ) by TARSKI:def_1;
( {(varcl A)} in x & {(varcl B)} in y ) by A4, A3, TARSKI:def_2;
hence contradiction by A5, A6, XREGULAR:10; ::_thesis: verum
end;
A7: for x, y, z being set st x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] implies S1[x,z] )
assume A8: ( x in Y & y in Y & z in Y & S1[x,y] & S1[y,z] ) ; ::_thesis: S1[x,z]
y in Vars by A8;
then consider B being Subset of Vars, k being Element of NAT such that
A9: ( y = [(varcl B),k] & B is finite ) by ABCMIZ_1:18;
z in Vars by A8;
then consider C being Subset of Vars, j being Element of NAT such that
A10: ( z = [(varcl C),j] & C is finite ) by ABCMIZ_1:18;
A11: ( z `1 = varcl C & y `1 = varcl B ) by A10, A9, MCART_1:7;
then varcl B c= varcl C by A8, A9, ABCMIZ_1:def_1;
hence S1[x,z] by A11, A8; ::_thesis: verum
end;
consider l being one-to-one FinSequence such that
A12: rng l = Y and
A13: for i, j being Nat st i in dom l & j in dom l & S1[l . i,l . j] holds
i < j from ABCMIZ_A:sch_3(A1, A7);
reconsider l = l as one-to-one FinSequence of Vars by A12, FINSEQ_1:def_4;
now__::_thesis:_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_a_being_Nat_st_
(_a_in_dom_l_&_a_<_i_&_y_=_l_._a_)
let i be Nat; ::_thesis: for x being variable st i in dom l & x = l . i holds
for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let x be variable; ::_thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume A14: ( i in dom l & x = l . i ) ; ::_thesis: for y being variable st y in vars x holds
ex a being Nat st
( a in dom l & a < i & y = l . a )
let y be variable; ::_thesis: ( y in vars x implies ex a being Nat st
( a in dom l & a < i & y = l . a ) )
assume A15: y in vars x ; ::_thesis: ex a being Nat st
( a in dom l & a < i & y = l . a )
x in Vars ;
then consider A being Subset of Vars, j being Element of NAT such that
A16: ( x = [(varcl A),j] & A is finite ) by ABCMIZ_1:18;
( x in rng l & vars x = varcl A ) by A14, A16, FUNCT_1:def_3, MCART_1:7;
then vars x c= Y by A12, A16, ABCMIZ_1:def_1;
then consider a being set such that
A17: ( a in dom l & y = l . a ) by A12, A15, FUNCT_1:def_3;
reconsider a = a as Nat by A17;
take a = a; ::_thesis: ( a in dom l & a < i & y = l . a )
thus ( a in dom l & a < i & y = l . a ) by A13, A14, A15, A17; ::_thesis: verum
end;
then reconsider l = l as quasi-loci by ABCMIZ_1:30;
take l ; ::_thesis: rng l = varcl X
thus rng l = varcl X by A12; ::_thesis: verum
end;
theorem Th32: :: ABCMIZ_A:32
for X, o being set
for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X holds
p is FinSequence of X
proof
let X, o be set ; ::_thesis: for p being DTree-yielding FinSequence st ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X holds
p is FinSequence of X
let p be DTree-yielding FinSequence; ::_thesis: ( ex C being initialized ConstructorSignature st X = Union the Sorts of (Free (C,(MSVars C))) & o -tree p in X implies p is FinSequence of X )
given C being initialized ConstructorSignature such that A1: X = Union the Sorts of (Free (C,(MSVars C))) ; ::_thesis: ( not o -tree p in X or p is FinSequence of X )
assume o -tree p in X ; ::_thesis: p is FinSequence of X
then reconsider e = o -tree p as expression of C by A1;
rng p c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng p or z in X )
assume z in rng p ; ::_thesis: z in X
then consider i being set such that
A2: ( i in dom p & z = p . i ) by FUNCT_1:def_3;
reconsider i = i as Nat by A2;
reconsider ppi = p . i as DecoratedTree by A2, TREES_3:24;
A3: ( 1 <= i & i <= len p ) by A2, FINSEQ_3:25;
then A4: (i -' 1) + 1 = i by XREAL_1:235;
then A5: i -' 1 < len p by A3, NAT_1:13;
A6: len (doms p) = len p by TREES_3:38;
A7: (doms p) . i = dom ppi by A2, FUNCT_6:22;
A8: dom e = tree (doms p) by TREES_4:10;
( <*(i -' 1)*> ^ (<*> NAT) = <*(i -' 1)*> & <*> NAT in dom ppi ) by FINSEQ_1:34, TREES_1:22;
then reconsider q = <*(i -' 1)*> as Element of dom e by A4, A5, A6, A7, A8, TREES_3:def_15;
e | q = z by A2, A4, A5, TREES_4:def_4;
then z is Element of (Free (C,(MSVars C))) by MSAFREE3:33;
hence z in X by A1; ::_thesis: verum
end;
hence p is FinSequence of X by FINSEQ_1:def_4; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let e be expression of C;
mode subexpression of e -> expression of C means :: ABCMIZ_A:def 7
it in Subtrees e;
existence
ex b1 being expression of C st b1 in Subtrees e by TREES_9:11;
func constrs e -> set equals :: ABCMIZ_A:def 8
(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ;
coherence
(proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } is set ;
func main-constr e -> set equals :Def9: :: ABCMIZ_A:def 9
(e . {}) `1 if e is compound
otherwise {} ;
correctness
coherence
( ( e is compound implies (e . {}) `1 is set ) & ( not e is compound implies {} is set ) );
consistency
for b1 being set holds verum;
;
func args e -> FinSequence of (Free (C,(MSVars C))) means :: ABCMIZ_A:def 10
e = (e . {}) -tree it;
existence
ex b1 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1
proof
consider v being set , p being DTree-yielding FinSequence such that
A1: e = v -tree p by TREES_9:8;
A2: v = e . {} by A1, TREES_4:def_4;
p is FinSequence of (Free (C,(MSVars C))) by A1, Th32;
hence ex b1 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of (Free (C,(MSVars C))) st e = (e . {}) -tree b1 & e = (e . {}) -tree b2 holds
b1 = b2 by TREES_4:15;
end;
:: deftheorem defines subexpression ABCMIZ_A:def_7_:_
for C being initialized ConstructorSignature
for e, b3 being expression of C holds
( b3 is subexpression of e iff b3 in Subtrees e );
:: deftheorem defines constrs ABCMIZ_A:def_8_:_
for C being initialized ConstructorSignature
for e being expression of C holds constrs e = (proj1 (rng e)) /\ { o where o is constructor OperSymbol of C : verum } ;
:: deftheorem Def9 defines main-constr ABCMIZ_A:def_9_:_
for C being initialized ConstructorSignature
for e being expression of C holds
( ( e is compound implies main-constr e = (e . {}) `1 ) & ( not e is compound implies main-constr e = {} ) );
:: deftheorem defines args ABCMIZ_A:def_10_:_
for C being initialized ConstructorSignature
for e being expression of C
for b3 being FinSequence of (Free (C,(MSVars C))) holds
( b3 = args e iff e = (e . {}) -tree b3 );
theorem Th33: :: ABCMIZ_A:33
for C being initialized ConstructorSignature
for e being expression of C holds e is subexpression of e
proof
let C be initialized ConstructorSignature; ::_thesis: for e being expression of C holds e is subexpression of e
let e be expression of C; ::_thesis: e is subexpression of e
thus e in Subtrees e by TREES_9:11; :: according to ABCMIZ_A:def_7 ::_thesis: verum
end;
theorem :: ABCMIZ_A:34
for x being variable
for C being initialized ConstructorSignature holds main-constr (x -term C) = {} by Def9;
theorem Th35: :: ABCMIZ_A:35
for C being initialized ConstructorSignature
for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
main-constr (c -trm p) = c
proof
let C be initialized ConstructorSignature; ::_thesis: for c being constructor OperSymbol of C
for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
main-constr (c -trm p) = c
let c be constructor OperSymbol of C; ::_thesis: for p being FinSequence of QuasiTerms C st len p = len (the_arity_of c) holds
main-constr (c -trm p) = c
let p be FinSequence of QuasiTerms C; ::_thesis: ( len p = len (the_arity_of c) implies main-constr (c -trm p) = c )
assume len p = len (the_arity_of c) ; ::_thesis: main-constr (c -trm p) = c
then c -trm p = [c, the carrier of C] -tree p by ABCMIZ_1:def_35;
then (c -trm p) . {} = [c, the carrier of C] by TREES_4:def_4;
hence main-constr (c -trm p) = [c, the carrier of C] `1 by Def9
.= c ;
::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let e be expression of C;
attre is constructor means :Def11: :: ABCMIZ_A:def 11
( e is compound & main-constr e is constructor OperSymbol of C );
end;
:: deftheorem Def11 defines constructor ABCMIZ_A:def_11_:_
for C being initialized ConstructorSignature
for e being expression of C holds
( e is constructor iff ( e is compound & main-constr e is constructor OperSymbol of C ) );
registration
let C be initialized ConstructorSignature;
cluster constructor -> compound for Element of Union the Sorts of (Free (C,(MSVars C)));
coherence
for b1 being expression of C st b1 is constructor holds
b1 is compound by Def11;
end;
registration
let C be initialized ConstructorSignature;
cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching constructor for Element of Union the Sorts of (Free (C,(MSVars C)));
existence
ex b1 being expression of C st b1 is constructor
proof
consider m, a being OperSymbol of C such that
A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def_12;
( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38;
then reconsider m = m as constructor OperSymbol of C by A1, ABCMIZ_1:def_11;
set p = <*> (QuasiTerms C);
take e = m -trm (<*> (QuasiTerms C)); ::_thesis: e is constructor
thus e is compound ; :: according to ABCMIZ_A:def_11 ::_thesis: main-constr e is constructor OperSymbol of C
len (<*> (QuasiTerms C)) = len (the_arity_of m) by A1;
hence main-constr e is constructor OperSymbol of C by Th35; ::_thesis: verum
end;
end;
registration
let C be initialized ConstructorSignature;
let e be constructor expression of C;
cluster non empty Relation-like non pair Function-like finite DecoratedTree-like finite-branching constructor for subexpression of e;
existence
ex b1 being subexpression of e st b1 is constructor
proof
e is subexpression of e by Th33;
hence ex b1 being subexpression of e st b1 is constructor ; ::_thesis: verum
end;
end;
registration
let S be non void Signature;
let X be V6() ManySortedSet of S;
let t be Element of (Free (S,X));
cluster proj2 t -> Relation-like ;
coherence
rng t is Relation-like
proof
set Z = the carrier of S --> {0};
set Y = X \/ ( the carrier of S --> {0});
t is Term of S,(X \/ ( the carrier of S --> {0})) by MSAFREE3:8;
then rng t c= the carrier of (DTConMSA (X \/ ( the carrier of S --> {0}))) by RELAT_1:def_19;
hence rng t is Relation-like ; ::_thesis: verum
end;
end;
theorem :: ABCMIZ_A:36
for C being initialized ConstructorSignature
for e being constructor expression of C holds main-constr e in constrs e
proof
let C be initialized ConstructorSignature; ::_thesis: for e being constructor expression of C holds main-constr e in constrs e
let e be constructor expression of C; ::_thesis: main-constr e in constrs e
A1: main-constr e = (e . {}) `1 by Def9;
{} in dom e by TREES_1:22;
then e . {} in rng e by FUNCT_1:def_3;
then A2: main-constr e in proj1 (rng e) by A1, MCART_1:86;
main-constr e is constructor OperSymbol of C by Def11;
then main-constr e in { c where c is constructor OperSymbol of C : verum } ;
hence main-constr e in constrs e by A2, XBOOLE_0:def_4; ::_thesis: verum
end;
begin
definition
let C be non void Signature;
attrC is arity-rich means :Def12: :: ABCMIZ_A:def 12
for n being Nat
for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ;
let o be OperSymbol of C;
attro is nullary means :Def13: :: ABCMIZ_A:def 13
the_arity_of o = {} ;
attro is unary means :Def14: :: ABCMIZ_A:def 14
len (the_arity_of o) = 1;
attro is binary means :Def15: :: ABCMIZ_A:def 15
len (the_arity_of o) = 2;
end;
:: deftheorem Def12 defines arity-rich ABCMIZ_A:def_12_:_
for C being non void Signature holds
( C is arity-rich iff for n being Nat
for s being SortSymbol of C holds { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite );
:: deftheorem Def13 defines nullary ABCMIZ_A:def_13_:_
for C being non void Signature
for o being OperSymbol of C holds
( o is nullary iff the_arity_of o = {} );
:: deftheorem Def14 defines unary ABCMIZ_A:def_14_:_
for C being non void Signature
for o being OperSymbol of C holds
( o is unary iff len (the_arity_of o) = 1 );
:: deftheorem Def15 defines binary ABCMIZ_A:def_15_:_
for C being non void Signature
for o being OperSymbol of C holds
( o is binary iff len (the_arity_of o) = 2 );
theorem Th37: :: ABCMIZ_A:37
for C being non void Signature
for o being OperSymbol of C holds
( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
proof
let C be non void Signature; ::_thesis: for o being OperSymbol of C holds
( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
let o be OperSymbol of C; ::_thesis: ( ( o is nullary implies not o is unary ) & ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
thus ( o is nullary implies not o is unary ) ::_thesis: ( ( o is nullary implies not o is binary ) & ( o is unary implies not o is binary ) )
proof
assume the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: not o is unary
hence len (the_arity_of o) <> 1 ; :: according to ABCMIZ_A:def_14 ::_thesis: verum
end;
thus ( o is nullary implies not o is binary ) ::_thesis: ( o is unary implies not o is binary )
proof
assume the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: not o is binary
hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def_15 ::_thesis: verum
end;
assume len (the_arity_of o) = 1 ; :: according to ABCMIZ_A:def_14 ::_thesis: not o is binary
hence len (the_arity_of o) <> 2 ; :: according to ABCMIZ_A:def_15 ::_thesis: verum
end;
registration
let C be ConstructorSignature;
cluster non_op C -> unary ;
coherence
non_op C is unary
proof
the_arity_of (non_op C) = <*(an_Adj C)*> by ABCMIZ_1:38;
hence len (the_arity_of (non_op C)) = 1 by FINSEQ_1:39; :: according to ABCMIZ_A:def_14 ::_thesis: verum
end;
cluster ast C -> binary ;
coherence
ast C is binary
proof
the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> by ABCMIZ_1:38;
hence len (the_arity_of (ast C)) = 2 by FINSEQ_1:44; :: according to ABCMIZ_A:def_15 ::_thesis: verum
end;
end;
registration
let C be ConstructorSignature;
cluster nullary -> constructor for Element of the carrier' of C;
coherence
for b1 being OperSymbol of C st b1 is nullary holds
b1 is constructor
proof
let o be OperSymbol of C; ::_thesis: ( o is nullary implies o is constructor )
assume A1: the_arity_of o = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: o is constructor
( the_arity_of (ast C) = <*(an_Adj C),(a_Type C)*> & the_arity_of (non_op C) = <*(an_Adj C)*> ) by ABCMIZ_1:38;
hence ( o <> * & o <> non_op ) by A1; :: according to ABCMIZ_1:def_11 ::_thesis: verum
end;
end;
theorem Th38: :: ABCMIZ_A:38
for C being ConstructorSignature holds
( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) )
proof
let C be ConstructorSignature; ::_thesis: ( C is initialized iff ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) )
hereby ::_thesis: ( ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary ) implies C is initialized )
assume C is initialized ; ::_thesis: ex m being OperSymbol of a_Type C ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
then consider m, a being OperSymbol of C such that
A1: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by ABCMIZ_1:def_12;
reconsider m = m as OperSymbol of a_Type C by A1, ABCMIZ_1:def_32;
reconsider a = a as OperSymbol of an_Adj C by A1, ABCMIZ_1:def_32;
take m = m; ::_thesis: ex a being OperSymbol of an_Adj C st
( m is nullary & a is nullary )
take a = a; ::_thesis: ( m is nullary & a is nullary )
thus m is nullary ::_thesis: a is nullary
proof
thus the_arity_of m = {} by A1; :: according to ABCMIZ_A:def_13 ::_thesis: verum
end;
thus a is nullary ::_thesis: verum
proof
thus the_arity_of a = {} by A1; :: according to ABCMIZ_A:def_13 ::_thesis: verum
end;
end;
given m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that A2: ( m is nullary & a is nullary ) ; ::_thesis: C is initialized
take m ; :: according to ABCMIZ_1:def_12 ::_thesis: ex b1 being Element of the carrier' of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b1 = an_Adj & the_arity_of b1 = {} )
take a ; ::_thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
( the_result_sort_of (non_op C) = an_Adj C & the_result_sort_of (ast C) = a_Type C ) by ABCMIZ_1:38;
hence ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A2, Def13, ABCMIZ_1:def_32; ::_thesis: verum
end;
registration
let C be initialized ConstructorSignature;
cluster constructor nullary for OperSymbol of a_Type C;
existence
ex b1 being OperSymbol of a_Type C st
( b1 is nullary & b1 is constructor )
proof
consider m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that
A1: ( m is nullary & a is nullary ) by Th38;
take m ; ::_thesis: ( m is nullary & m is constructor )
thus ( m is nullary & m is constructor ) by A1; ::_thesis: verum
end;
cluster constructor nullary for OperSymbol of an_Adj C;
existence
ex b1 being OperSymbol of an_Adj C st
( b1 is nullary & b1 is constructor )
proof
consider m being OperSymbol of a_Type C, a being OperSymbol of an_Adj C such that
A2: ( m is nullary & a is nullary ) by Th38;
take a ; ::_thesis: ( a is nullary & a is constructor )
thus ( a is nullary & a is constructor ) by A2; ::_thesis: verum
end;
end;
registration
let C be initialized ConstructorSignature;
cluster constructor nullary for Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st
( b1 is nullary & b1 is constructor )
proof
set o = the constructor nullary OperSymbol of a_Type C;
take the constructor nullary OperSymbol of a_Type C ; ::_thesis: ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor )
thus ( the constructor nullary OperSymbol of a_Type C is nullary & the constructor nullary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum
end;
end;
registration
cluster non void V146() arity-rich -> non void with_an_operation_for_each_sort for ManySortedSign ;
coherence
for b1 being non void Signature st b1 is arity-rich holds
b1 is with_an_operation_for_each_sort
proof
let S be non void Signature; ::_thesis: ( S is arity-rich implies S is with_an_operation_for_each_sort )
assume A1: for n being Nat
for s being SortSymbol of S holds { o where o is OperSymbol of S : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite ; :: according to ABCMIZ_A:def_12 ::_thesis: S is with_an_operation_for_each_sort
let v be set ; :: according to TARSKI:def_3,ABCMIZ_1:def_54 ::_thesis: ( not v in the carrier of S or v in rng the ResultSort of S )
assume v in the carrier of S ; ::_thesis: v in rng the ResultSort of S
then reconsider v = v as SortSymbol of S ;
set A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } ;
reconsider A = { o where o is OperSymbol of S : ( the_result_sort_of o = v & len (the_arity_of o) = 0 ) } as infinite set by A1;
set a = the Element of A;
the Element of A in A ;
then consider o being OperSymbol of S such that
A2: ( the Element of A = o & the_result_sort_of o = v & len (the_arity_of o) = 0 ) ;
thus v in rng the ResultSort of S by A2, FUNCT_2:4; ::_thesis: verum
end;
clusterV146() constructor arity-rich -> initialized for ManySortedSign ;
coherence
for b1 being ConstructorSignature st b1 is arity-rich holds
b1 is initialized
proof
let C be ConstructorSignature; ::_thesis: ( C is arity-rich implies C is initialized )
assume A3: C is arity-rich ; ::_thesis: C is initialized
set Xt = { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
set x = the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } is infinite set by A3, Def12;
then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } in { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } ;
then consider m being OperSymbol of C such that
A4: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = a_Type C & len (the_arity_of o) = 0 ) } = m & the_result_sort_of m = a_Type C & len (the_arity_of m) = 0 ) ;
set Xa = { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
set x = the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } is infinite set by A3, Def12;
then the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } in { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } ;
then consider a being OperSymbol of C such that
A5: ( the Element of { o where o is OperSymbol of C : ( the_result_sort_of o = an_Adj C & len (the_arity_of o) = 0 ) } = a & the_result_sort_of a = an_Adj C & len (the_arity_of a) = 0 ) ;
take m ; :: according to ABCMIZ_1:def_12 ::_thesis: ex b1 being Element of the carrier' of C st
( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of b1 = an_Adj & the_arity_of b1 = {} )
take a ; ::_thesis: ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} )
thus ( the_result_sort_of m = a_Type & the_arity_of m = {} & the_result_sort_of a = an_Adj & the_arity_of a = {} ) by A4, A5; ::_thesis: verum
end;
end;
registration
cluster MaxConstrSign -> arity-rich ;
coherence
MaxConstrSign is arity-rich
proof
set C = MaxConstrSign ;
let n be Nat; :: according to ABCMIZ_A:def_12 ::_thesis: for s being SortSymbol of MaxConstrSign holds { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite
let s be SortSymbol of MaxConstrSign; ::_thesis: { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite
A1: the carrier of MaxConstrSign = {0,1,2} by ABCMIZ_1:def_9;
set X = { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } ;
consider l being quasi-loci such that
A2: len l = n by Th30;
deffunc H1( set ) -> set = [s,[l,c1]];
consider f being Function such that
A3: ( dom f = NAT & ( for i being set st i in NAT holds
f . i = H1(i) ) ) from FUNCT_1:sch_3();
f is one-to-one
proof
let i, j be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not i in proj1 f or not j in proj1 f or not f . i = f . j or i = j )
assume ( i in dom f & j in dom f ) ; ::_thesis: ( not f . i = f . j or i = j )
then reconsider i = i, j = j as Element of NAT by A3;
( f . i = H1(i) & f . j = H1(j) ) by A3;
then ( f . i = f . j implies [l,i] = [l,j] ) by XTUPLE_0:1;
hence ( not f . i = f . j or i = j ) by XTUPLE_0:1; ::_thesis: verum
end;
then A4: rng f is infinite by A3, CARD_1:59;
rng f c= { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) }
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } )
assume y in rng f ; ::_thesis: y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) }
then consider x being set such that
A5: ( x in dom f & y = f . x ) by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A3, A5;
A6: ( [l,x] in [:QuasiLoci,NAT:] & y = H1(x) ) by A3, A5;
then y in Constructors by A1, Th28, ZFMISC_1:def_2;
then y in {*,non_op} \/ Constructors by XBOOLE_0:def_3;
then reconsider y = y as OperSymbol of MaxConstrSign by ABCMIZ_1:def_24;
A7: y is constructor by A6, ABCMIZ_1:def_11;
then A8: the_result_sort_of y = y `1 by ABCMIZ_1:def_24
.= s by A6, MCART_1:7 ;
len (the_arity_of y) = card ((y `2) `1) by A7, ABCMIZ_1:def_24
.= card ([l,x] `1) by A6, MCART_1:7
.= len l ;
hence y in { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } by A2, A8; ::_thesis: verum
end;
hence { o where o is OperSymbol of MaxConstrSign : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is infinite by A4; ::_thesis: verum
end;
end;
registration
cluster non empty non void V68() V146() constructor initialized arity-rich for ManySortedSign ;
existence
ex b1 being ConstructorSignature st
( b1 is arity-rich & b1 is initialized )
proof
take MaxConstrSign ; ::_thesis: ( MaxConstrSign is arity-rich & MaxConstrSign is initialized )
thus ( MaxConstrSign is arity-rich & MaxConstrSign is initialized ) ; ::_thesis: verum
end;
end;
registration
let C be arity-rich ConstructorSignature;
let s be SortSymbol of C;
cluster constructor nullary for OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is nullary & b1 is constructor )
proof
set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } is infinite by Def12;
then consider m1, m2 being set such that
A1: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 0 ) } & m1 <> m2 ) by ZFMISC_1:def_10;
consider o1 being OperSymbol of C such that
A2: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 0 ) by A1;
reconsider m1 = m1 as OperSymbol of s by A2, ABCMIZ_1:def_32;
the_arity_of m1 = {} by A2;
then m1 is nullary by Def13;
hence ex b1 being OperSymbol of s st
( b1 is nullary & b1 is constructor ) ; ::_thesis: verum
end;
cluster constructor unary for OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is unary & b1 is constructor )
proof
set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } is infinite by Def12;
then consider m1, m2 being set such that
A3: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 1 ) } & m1 <> m2 ) by ZFMISC_1:def_10;
consider o1 being OperSymbol of C such that
A4: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 1 ) by A3;
consider o2 being OperSymbol of C such that
A5: ( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 1 ) by A3;
reconsider m1 = m1, m2 = m2 as OperSymbol of s by A4, A5, ABCMIZ_1:def_32;
A6: ( m1 is unary & m2 is unary ) by A4, A5, Def14;
then A7: ( m1 <> ast C & m2 <> ast C ) by Th37;
( m1 <> non_op or m2 <> non_op ) by A3;
then ( m1 is constructor or m2 is constructor ) by A7, ABCMIZ_1:def_11;
hence ex b1 being OperSymbol of s st
( b1 is unary & b1 is constructor ) by A6; ::_thesis: verum
end;
cluster constructor binary for OperSymbol of s;
existence
ex b1 being OperSymbol of s st
( b1 is binary & b1 is constructor )
proof
set X = { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } ;
{ o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } is infinite by Def12;
then consider m1, m2 being set such that
A8: ( m1 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m2 in { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = 2 ) } & m1 <> m2 ) by ZFMISC_1:def_10;
consider o1 being OperSymbol of C such that
A9: ( m1 = o1 & the_result_sort_of o1 = s & len (the_arity_of o1) = 2 ) by A8;
consider o2 being OperSymbol of C such that
A10: ( m2 = o2 & the_result_sort_of o2 = s & len (the_arity_of o2) = 2 ) by A8;
reconsider m1 = m1, m2 = m2 as OperSymbol of s by A9, A10, ABCMIZ_1:def_32;
A11: ( m1 is binary & m2 is binary ) by A9, A10, Def15;
then A12: ( m1 <> non_op C & m2 <> non_op C ) by Th37;
( m1 <> * or m2 <> * ) by A8;
then ( m1 is constructor or m2 is constructor ) by A12, ABCMIZ_1:def_11;
hence ex b1 being OperSymbol of s st
( b1 is binary & b1 is constructor ) by A11; ::_thesis: verum
end;
end;
registration
let C be arity-rich ConstructorSignature;
cluster constructor unary for Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st
( b1 is unary & b1 is constructor )
proof
set o = the constructor unary OperSymbol of a_Type C;
take the constructor unary OperSymbol of a_Type C ; ::_thesis: ( the constructor unary OperSymbol of a_Type C is unary & the constructor unary OperSymbol of a_Type C is constructor )
thus ( the constructor unary OperSymbol of a_Type C is unary & the constructor unary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum
end;
cluster constructor binary for Element of the carrier' of C;
existence
ex b1 being OperSymbol of C st
( b1 is binary & b1 is constructor )
proof
set o = the constructor binary OperSymbol of a_Type C;
take the constructor binary OperSymbol of a_Type C ; ::_thesis: ( the constructor binary OperSymbol of a_Type C is binary & the constructor binary OperSymbol of a_Type C is constructor )
thus ( the constructor binary OperSymbol of a_Type C is binary & the constructor binary OperSymbol of a_Type C is constructor ) ; ::_thesis: verum
end;
end;
theorem Th39: :: ABCMIZ_A:39
for C being initialized ConstructorSignature
for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o
proof
let C be initialized ConstructorSignature; ::_thesis: for o being nullary OperSymbol of C holds [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o
let o be nullary OperSymbol of C; ::_thesis: [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o
set X = MSVars C;
set Z = the carrier of C --> {0};
set Y = (MSVars C) \/ ( the carrier of C --> {0});
A1: the_arity_of o = {} by Def13;
A2: the Sorts of (Free (C,(MSVars C))) = C -Terms ((MSVars C),((MSVars C) \/ ( the carrier of C --> {0}))) by MSAFREE3:24;
for i being Nat st i in dom {} holds
ex t being Term of C,((MSVars C) \/ ( the carrier of C --> {0})) st
( t = {} . i & the_sort_of t = (the_arity_of o) . i ) ;
then reconsider p = {} as ArgumentSeq of Sym (o,((MSVars C) \/ ( the carrier of C --> {0}))) by A1, MSATERM:24;
A3: variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p) c= MSVars C
proof
let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of C or (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s )
assume s in the carrier of C ; ::_thesis: (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s c= (MSVars C) . s
then reconsider s9 = s as SortSymbol of C ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s or x in (MSVars C) . s )
assume x in (variables_in ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p)) . s ; ::_thesis: x in (MSVars C) . s
then ex t being DecoratedTree st
( t in rng p & x in (C variables_in t) . s9 ) by MSAFREE3:11;
hence x in (MSVars C) . s ; ::_thesis: verum
end;
set s9 = the_result_sort_of o;
A4: the_sort_of ((Sym (o,((MSVars C) \/ ( the carrier of C --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;
the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) = { t where t is Term of C,((MSVars C) \/ ( the carrier of C --> {0})) : ( the_sort_of t = the_result_sort_of o & variables_in t c= MSVars C ) } by A2, MSAFREE3:def_5;
then [o, the carrier of C] -tree {} in the Sorts of (Free (C,(MSVars C))) . (the_result_sort_of o) by A3, A4;
hence [o, the carrier of C] -tree {} is expression of C, the_result_sort_of o by ABCMIZ_1:41; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let m be constructor nullary OperSymbol of a_Type C;
:: original: term
redefine funcm term -> pure expression of C, a_Type C;
coherence
m term is pure expression of C, a_Type C
proof
set T = m term ;
the_arity_of m = 0 by Def13;
then len (the_arity_of m) = 0 ;
then A1: m term = [m, the carrier of C] -tree {} by ABCMIZ_1:def_29;
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 = {} ) by ABCMIZ_1:def_12;
then the_result_sort_of m = a_Type C by ABCMIZ_1:def_32;
then reconsider T = m term as expression of C, a_Type C by A1, Th39;
T is pure
proof
given a being expression of C, an_Adj C, t being expression of C, a_Type C such that A2: T = (ast C) term (a,t) ; :: according to ABCMIZ_1:def_41 ::_thesis: contradiction
T = [*, the carrier of C] -tree <*a,t*> by A2, ABCMIZ_1:46;
hence contradiction by A1, TREES_4:15; ::_thesis: verum
end;
hence m term is pure expression of C, a_Type C ; ::_thesis: verum
end;
end;
definition
let c be Element of Constructors ;
func @ c -> constructor OperSymbol of MaxConstrSign equals :: ABCMIZ_A:def 16
c;
coherence
c is constructor OperSymbol of MaxConstrSign
proof
( * in {*,non_op} & non_op in {*,non_op} & the carrier' of MaxConstrSign = {*,non_op} \/ Constructors ) by ABCMIZ_1:def_24, TARSKI:def_2;
then ( c <> * & c <> non_op & c in the carrier' of MaxConstrSign ) by ABCMIZ_1:39, XBOOLE_0:3, XBOOLE_0:def_3;
hence c is constructor OperSymbol of MaxConstrSign by ABCMIZ_1:def_11; ::_thesis: verum
end;
end;
:: deftheorem defines @ ABCMIZ_A:def_16_:_
for c being Element of Constructors holds @ c = c;
definition
let m be Element of Modes ;
:: original: @
redefine func @ m -> constructor OperSymbol of a_Type MaxConstrSign;
coherence
@ m is constructor OperSymbol of a_Type MaxConstrSign
proof
A1: m `1 in {a_Type} by MCART_1:10;
the_result_sort_of (@ m) = m `1 by ABCMIZ_1:def_24
.= a_Type by A1, TARSKI:def_1 ;
hence @ m is constructor OperSymbol of a_Type MaxConstrSign by ABCMIZ_1:def_32; ::_thesis: verum
end;
end;
registration
cluster @ set-constr -> constructor nullary ;
coherence
@ set-constr is nullary
proof
len (the_arity_of (@ set-constr)) = card ((set-constr `2) `1) by ABCMIZ_1:def_24
.= card ([{},0] `1) by MCART_1:7
.= card 0 ;
hence the_arity_of (@ set-constr) = {} ; :: according to ABCMIZ_A:def_13 ::_thesis: verum
end;
end;
theorem :: ABCMIZ_A:40
the_arity_of (@ set-constr) = {} by Def13;
definition
func set-type -> quasi-type equals :: ABCMIZ_A:def 17
({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);
coherence
({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term) is quasi-type ;
end;
:: deftheorem defines set-type ABCMIZ_A:def_17_:_
set-type = ({} (QuasiAdjs MaxConstrSign)) ast ((@ set-constr) term);
theorem :: ABCMIZ_A:41
( adjs set-type = {} & the_base_of set-type = (@ set-constr) term ) by MCART_1:7;
definition
let l be FinSequence of Vars ;
func args l -> FinSequence of QuasiTerms MaxConstrSign means :Def18: :: ABCMIZ_A:def 18
( len it = len l & ( for i being Nat st i in dom l holds
it . i = (l /. i) -term MaxConstrSign ) );
existence
ex b1 being FinSequence of QuasiTerms MaxConstrSign st
( len b1 = len l & ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) )
proof
deffunc H1( Nat) -> expression of MaxConstrSign , a_Term MaxConstrSign = (l /. $1) -term MaxConstrSign;
consider g being FinSequence such that
A1: len g = len l and
A2: for i being Nat st i in dom g holds
g . i = H1(i) from FINSEQ_1:sch_2();
A3: dom g = dom l by A1, FINSEQ_3:29;
rng g c= QuasiTerms MaxConstrSign
proof
let j be set ; :: according to TARSKI:def_3 ::_thesis: ( not j in rng g or j in QuasiTerms MaxConstrSign )
assume j in rng g ; ::_thesis: j in QuasiTerms MaxConstrSign
then consider z being set such that
A4: ( z in dom g & j = g . z ) by FUNCT_1:def_3;
reconsider z = z as Nat by A4;
j = H1(z) by A2, A4;
hence j in QuasiTerms MaxConstrSign by ABCMIZ_1:49; ::_thesis: verum
end;
then reconsider g = g as FinSequence of QuasiTerms MaxConstrSign by FINSEQ_1:def_4;
take g ; ::_thesis: ( len g = len l & ( for i being Nat st i in dom l holds
g . i = (l /. i) -term MaxConstrSign ) )
thus ( len g = len l & ( for i being Nat st i in dom l holds
g . i = (l /. i) -term MaxConstrSign ) ) by A1, A2, A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSequence of QuasiTerms MaxConstrSign st len b1 = len l & ( for i being Nat st i in dom l holds
b1 . i = (l /. i) -term MaxConstrSign ) & len b2 = len l & ( for i being Nat st i in dom l holds
b2 . i = (l /. i) -term MaxConstrSign ) holds
b1 = b2
proof
let a1, a2 be FinSequence of QuasiTerms MaxConstrSign; ::_thesis: ( len a1 = len l & ( for i being Nat st i in dom l holds
a1 . i = (l /. i) -term MaxConstrSign ) & len a2 = len l & ( for i being Nat st i in dom l holds
a2 . i = (l /. i) -term MaxConstrSign ) implies a1 = a2 )
assume that
A5: len a1 = len l and
A6: for i being Nat st i in dom l holds
a1 . i = (l /. i) -term MaxConstrSign and
A7: len a2 = len l and
A8: for i being Nat st i in dom l holds
a2 . i = (l /. i) -term MaxConstrSign ; ::_thesis: a1 = a2
A9: ( dom a1 = dom l & dom a2 = dom l ) by A5, A7, FINSEQ_3:29;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_a1_holds_
a1_._i_=_a2_._i
let i be Nat; ::_thesis: ( i in dom a1 implies a1 . i = a2 . i )
assume i in dom a1 ; ::_thesis: a1 . i = a2 . i
then ( a1 . i = (l /. i) -term MaxConstrSign & a2 . i = (l /. i) -term MaxConstrSign ) by A6, A8, A9;
hence a1 . i = a2 . i ; ::_thesis: verum
end;
hence a1 = a2 by A9, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines args ABCMIZ_A:def_18_:_
for l being FinSequence of Vars
for b2 being FinSequence of QuasiTerms MaxConstrSign holds
( b2 = args l iff ( len b2 = len l & ( for i being Nat st i in dom l holds
b2 . i = (l /. i) -term MaxConstrSign ) ) );
definition
let c be Element of Constructors ;
func base_exp_of c -> expression equals :: ABCMIZ_A:def 19
(@ c) -trm (args (loci_of c));
coherence
(@ c) -trm (args (loci_of c)) is expression ;
end;
:: deftheorem defines base_exp_of ABCMIZ_A:def_19_:_
for c being Element of Constructors holds base_exp_of c = (@ c) -trm (args (loci_of c));
theorem Th42: :: ABCMIZ_A:42
for o being OperSymbol of MaxConstrSign holds
( o is constructor iff o in Constructors )
proof
let o be OperSymbol of MaxConstrSign; ::_thesis: ( o is constructor iff o in Constructors )
A1: the carrier' of MaxConstrSign = {*,non_op} \/ Constructors by ABCMIZ_1:def_24;
( o is constructor iff ( o <> * & o <> non_op ) ) by ABCMIZ_1:def_11;
then ( o is constructor iff o nin {*,non_op} ) by TARSKI:def_2;
hence ( o is constructor iff o in Constructors ) by A1, ABCMIZ_1:39, XBOOLE_0:3, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem :: ABCMIZ_A:43
for m being nullary OperSymbol of MaxConstrSign holds main-constr (m term) = m
proof
set C = MaxConstrSign ;
let m be nullary OperSymbol of MaxConstrSign; ::_thesis: main-constr (m term) = m
the_arity_of m = 0 by Def13;
then ( len (the_arity_of m) = 0 & len {} = 0 ) ;
then A1: ( m term = [m, the carrier of MaxConstrSign] -tree {} & m -trm (<*> (QuasiTerms MaxConstrSign)) = [m, the carrier of MaxConstrSign] -tree {} ) by ABCMIZ_1:def_29, ABCMIZ_1:def_35;
hence main-constr (m term) = ((m term) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A1, TREES_4:def_4
.= m ;
::_thesis: verum
end;
theorem :: ABCMIZ_A:44
for m being constructor unary OperSymbol of MaxConstrSign
for t being quasi-term holds main-constr (m term t) = m
proof
set C = MaxConstrSign ;
let m be constructor unary OperSymbol of MaxConstrSign; ::_thesis: for t being quasi-term holds main-constr (m term t) = m
let t be quasi-term; ::_thesis: main-constr (m term t) = m
reconsider w = t as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49;
reconsider p = <*w*> as FinSequence of QuasiTerms MaxConstrSign ;
A1: len (the_arity_of m) = 1 by Def14;
then the_arity_of m = 1 |-> a_Term by ABCMIZ_1:37
.= <*a_Term*> by FINSEQ_2:59 ;
then ( len p = 1 & (the_arity_of m) . 1 = a_Term MaxConstrSign ) by FINSEQ_1:40;
then A2: ( m term t = [m, the carrier of MaxConstrSign] -tree <*t*> & m -trm p = [m, the carrier of MaxConstrSign] -tree <*t*> ) by A1, ABCMIZ_1:def_30, ABCMIZ_1:def_35;
hence main-constr (m term t) = ((m term t) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4
.= m ;
::_thesis: verum
end;
theorem :: ABCMIZ_A:45
for a being quasi-adjective holds main-constr ((non_op MaxConstrSign) term a) = non_op
proof
set C = MaxConstrSign ;
set m = non_op MaxConstrSign;
let a be quasi-adjective; ::_thesis: main-constr ((non_op MaxConstrSign) term a) = non_op
A1: len (the_arity_of (non_op MaxConstrSign)) = 1 by Def14;
the_arity_of (non_op MaxConstrSign) = <*an_Adj*> by ABCMIZ_1:38;
then (the_arity_of (non_op MaxConstrSign)) . 1 = an_Adj MaxConstrSign by FINSEQ_1:40;
then A2: (non_op MaxConstrSign) term a = [(non_op MaxConstrSign), the carrier of MaxConstrSign] -tree <*a*> by A1, ABCMIZ_1:def_30;
thus main-constr ((non_op MaxConstrSign) term a) = (((non_op MaxConstrSign) term a) . {}) `1 by Def9
.= [(non_op MaxConstrSign), the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4
.= non_op ; ::_thesis: verum
end;
theorem :: ABCMIZ_A:46
for m being constructor binary OperSymbol of MaxConstrSign
for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m
proof
set C = MaxConstrSign ;
let m be constructor binary OperSymbol of MaxConstrSign; ::_thesis: for t1, t2 being quasi-term holds main-constr (m term (t1,t2)) = m
let t1, t2 be quasi-term; ::_thesis: main-constr (m term (t1,t2)) = m
reconsider w1 = t1, w2 = t2 as Element of QuasiTerms MaxConstrSign by ABCMIZ_1:49;
reconsider p = <*w1,w2*> as FinSequence of QuasiTerms MaxConstrSign ;
A1: len (the_arity_of m) = 2 by Def15;
then the_arity_of m = 2 |-> a_Term by ABCMIZ_1:37
.= <*a_Term,a_Term*> by FINSEQ_2:61 ;
then ( (the_arity_of m) . 1 = a_Term MaxConstrSign & (the_arity_of m) . 2 = a_Term MaxConstrSign & len p = 2 ) by FINSEQ_1:44;
then A2: ( m term (t1,t2) = [m, the carrier of MaxConstrSign] -tree <*t1,t2*> & m -trm p = [m, the carrier of MaxConstrSign] -tree p ) by A1, ABCMIZ_1:def_31, ABCMIZ_1:def_35;
hence main-constr (m term (t1,t2)) = ((m term (t1,t2)) . {}) `1 by Def9
.= [m, the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4
.= m ;
::_thesis: verum
end;
theorem :: ABCMIZ_A:47
for q being expression of MaxConstrSign , a_Type MaxConstrSign
for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *
proof
set C = MaxConstrSign ;
set m = ast MaxConstrSign;
let q be expression of MaxConstrSign , a_Type MaxConstrSign; ::_thesis: for a being quasi-adjective holds main-constr ((ast MaxConstrSign) term (a,q)) = *
let a be quasi-adjective; ::_thesis: main-constr ((ast MaxConstrSign) term (a,q)) = *
A1: len (the_arity_of (ast MaxConstrSign)) = 2 by Def15;
the_arity_of (ast MaxConstrSign) = <*(an_Adj MaxConstrSign),(a_Type MaxConstrSign)*> by ABCMIZ_1:38;
then ( (the_arity_of (ast MaxConstrSign)) . 1 = an_Adj MaxConstrSign & (the_arity_of (ast MaxConstrSign)) . 2 = a_Type MaxConstrSign ) by FINSEQ_1:44;
then A2: (ast MaxConstrSign) term (a,q) = [(ast MaxConstrSign), the carrier of MaxConstrSign] -tree <*a,q*> by A1, ABCMIZ_1:def_31;
thus main-constr ((ast MaxConstrSign) term (a,q)) = (((ast MaxConstrSign) term (a,q)) . {}) `1 by Def9
.= [(ast MaxConstrSign), the carrier of MaxConstrSign] `1 by A2, TREES_4:def_4
.= * ; ::_thesis: verum
end;
definition
let T be quasi-type;
func constrs T -> set equals :: ABCMIZ_A:def 20
(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } );
coherence
(constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } ) is set ;
end;
:: deftheorem defines constrs ABCMIZ_A:def_20_:_
for T being quasi-type holds constrs T = (constrs (the_base_of T)) \/ (union { (constrs a) where a is quasi-adjective : a in adjs T } );
theorem :: ABCMIZ_A:48
for q being pure expression of MaxConstrSign , a_Type MaxConstrSign
for A being finite Subset of (QuasiAdjs MaxConstrSign) holds constrs (A ast q) = (constrs q) \/ (union { (constrs a) where a is quasi-adjective : a in A } ) ;
theorem :: ABCMIZ_A:49
for a being quasi-adjective
for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T)
proof
let a be quasi-adjective; ::_thesis: for T being quasi-type holds constrs (a ast T) = (constrs a) \/ (constrs T)
let T be quasi-type; ::_thesis: constrs (a ast T) = (constrs a) \/ (constrs T)
set A = { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ;
set B = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ;
A1: { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } = { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)}
proof
thus { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } c= { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} :: according to XBOOLE_0:def_10 ::_thesis: { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} c= { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} )
assume z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)}
then consider a9 being quasi-adjective such that
A2: ( z = constrs a9 & a9 in {a} \/ (adjs T) ) ;
( a9 in {a} or a9 in adjs T ) by A2, XBOOLE_0:def_3;
then ( a9 = a or a9 in adjs T ) by TARSKI:def_1;
then ( z in {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by A2, TARSKI:def_1;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} by XBOOLE_0:def_3; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} or z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } )
assume A3: z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } \/ {(constrs a)} ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }
A4: a in {a} by TARSKI:def_1;
percases ( z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } or z in {(constrs a)} ) by A3, XBOOLE_0:def_3;
suppose z in { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }
then consider a9 being quasi-adjective such that
A5: ( z = constrs a9 & a9 in adjs T ) ;
a9 in {a} \/ (adjs T) by A5, XBOOLE_0:def_3;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } by A5; ::_thesis: verum
end;
suppose z in {(constrs a)} ; ::_thesis: z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) }
then ( z = constrs a & a in {a} \/ (adjs T) ) by A4, TARSKI:def_1, XBOOLE_0:def_3;
hence z in { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ; ::_thesis: verum
end;
end;
end;
adjs (a ast T) = {a} \/ (adjs T) by ABCMIZ_1:82;
hence constrs (a ast T) = (constrs (the_base_of (a ast T))) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } )
.= (constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in {a} \/ (adjs T) } ) by ABCMIZ_1:82
.= (constrs (the_base_of T)) \/ ((union {(constrs a)}) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by A1, ZFMISC_1:78
.= (constrs (the_base_of T)) \/ ((constrs a) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by ZFMISC_1:25
.= ((constrs (the_base_of T)) \/ (constrs a)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } ) by XBOOLE_1:4
.= (constrs a) \/ ((constrs (the_base_of T)) \/ (union { (constrs a9) where a9 is quasi-adjective : a9 in adjs T } )) by XBOOLE_1:4
.= (constrs a) \/ (constrs T) ;
::_thesis: verum
end;
begin
definition
let C be initialized ConstructorSignature;
let t, p be expression of C;
predt matches_with p means :: ABCMIZ_A:def 21
ex f being valuation of C st t = p at f;
reflexivity
for t being expression of C ex f being valuation of C st t = t at f
proof
let t be expression of C; ::_thesis: ex f being valuation of C st t = t at f
take f = the empty valuation of C; ::_thesis: t = t at f
thus t at f = t by ABCMIZ_1:139; ::_thesis: verum
end;
end;
:: deftheorem defines matches_with ABCMIZ_A:def_21_:_
for C being initialized ConstructorSignature
for t, p being expression of C holds
( t matches_with p iff ex f being valuation of C st t = p at f );
theorem :: ABCMIZ_A:50
for C being initialized ConstructorSignature
for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds
t1 matches_with t3
proof
let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t3 being expression of C st t1 matches_with t2 & t2 matches_with t3 holds
t1 matches_with t3
let t1, t2, t3 be expression of C; ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 )
given f1 being valuation of C such that A1: t1 = t2 at f1 ; :: according to ABCMIZ_A:def_21 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: t2 = t3 at f2 ; :: according to ABCMIZ_A:def_21 ::_thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def_21 ::_thesis: t1 = t3 at (f2 at f1)
thus t1 = t3 at (f2 at f1) by A1, A2, ABCMIZ_1:149; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let A, B be Subset of (QuasiAdjs C);
predA matches_with B means :: ABCMIZ_A:def 22
ex f being valuation of C st B at f c= A;
reflexivity
for A being Subset of (QuasiAdjs C) ex f being valuation of C st A at f c= A
proof
let t be Subset of (QuasiAdjs C); ::_thesis: ex f being valuation of C st t at f c= t
take f = the empty valuation of C; ::_thesis: t at f c= t
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in t at f or x in t )
assume x in t at f ; ::_thesis: x in t
then ex a being quasi-adjective of C st
( x = a at f & a in t ) ;
hence x in t by ABCMIZ_1:139; ::_thesis: verum
end;
end;
:: deftheorem defines matches_with ABCMIZ_A:def_22_:_
for C being initialized ConstructorSignature
for A, B being Subset of (QuasiAdjs C) holds
( A matches_with B iff ex f being valuation of C st B at f c= A );
theorem :: ABCMIZ_A:51
for C being initialized ConstructorSignature
for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds
A1 matches_with A3
proof
let C be initialized ConstructorSignature; ::_thesis: for A1, A2, A3 being Subset of (QuasiAdjs C) st A1 matches_with A2 & A2 matches_with A3 holds
A1 matches_with A3
let t1, t2, t3 be Subset of (QuasiAdjs C); ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 )
given f1 being valuation of C such that A1: t2 at f1 c= t1 ; :: according to ABCMIZ_A:def_22 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: t3 at f2 c= t2 ; :: according to ABCMIZ_A:def_22 ::_thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def_22 ::_thesis: t3 at (f2 at f1) c= t1
(t3 at f2) at f1 c= t2 at f1 by A2, ABCMIZ_1:146;
then (t3 at f2) at f1 c= t1 by A1, XBOOLE_1:1;
hence t3 at (f2 at f1) c= t1 by ABCMIZ_1:150; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let T, P be quasi-type of C;
predT matches_with P means :: ABCMIZ_A:def 23
ex f being valuation of C st
( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T );
reflexivity
for T being quasi-type of C ex f being valuation of C st
( (adjs T) at f c= adjs T & (the_base_of T) at f = the_base_of T )
proof
let t be quasi-type of C; ::_thesis: ex f being valuation of C st
( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t )
take f = the empty valuation of C; ::_thesis: ( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t )
thus (adjs t) at f c= adjs t ::_thesis: (the_base_of t) at f = the_base_of t
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (adjs t) at f or x in adjs t )
assume x in (adjs t) at f ; ::_thesis: x in adjs t
then ex a being quasi-adjective of C st
( x = a at f & a in adjs t ) ;
hence x in adjs t by ABCMIZ_1:139; ::_thesis: verum
end;
thus (the_base_of t) at f = the_base_of t by ABCMIZ_1:139; ::_thesis: verum
end;
end;
:: deftheorem defines matches_with ABCMIZ_A:def_23_:_
for C being initialized ConstructorSignature
for T, P being quasi-type of C holds
( T matches_with P iff ex f being valuation of C st
( (adjs P) at f c= adjs T & (the_base_of P) at f = the_base_of T ) );
theorem :: ABCMIZ_A:52
for C being initialized ConstructorSignature
for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds
T1 matches_with T3
proof
let C be initialized ConstructorSignature; ::_thesis: for T1, T2, T3 being quasi-type of C st T1 matches_with T2 & T2 matches_with T3 holds
T1 matches_with T3
let t1, t2, t3 be quasi-type of C; ::_thesis: ( t1 matches_with t2 & t2 matches_with t3 implies t1 matches_with t3 )
given f1 being valuation of C such that A1: ( (adjs t2) at f1 c= adjs t1 & (the_base_of t2) at f1 = the_base_of t1 ) ; :: according to ABCMIZ_A:def_23 ::_thesis: ( not t2 matches_with t3 or t1 matches_with t3 )
given f2 being valuation of C such that A2: ( (adjs t3) at f2 c= adjs t2 & (the_base_of t3) at f2 = the_base_of t2 ) ; :: according to ABCMIZ_A:def_23 ::_thesis: t1 matches_with t3
take f2 at f1 ; :: according to ABCMIZ_A:def_23 ::_thesis: ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 )
((adjs t3) at f2) at f1 c= (adjs t2) at f1 by A2, ABCMIZ_1:146;
then ((adjs t3) at f2) at f1 c= adjs t1 by A1, XBOOLE_1:1;
hence ( (adjs t3) at (f2 at f1) c= adjs t1 & (the_base_of t3) at (f2 at f1) = the_base_of t1 ) by A1, A2, ABCMIZ_1:149, ABCMIZ_1:150; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
let f be valuation of C;
predf unifies t1,t2 means :Def24: :: ABCMIZ_A:def 24
t1 at f = t2 at f;
end;
:: deftheorem Def24 defines unifies ABCMIZ_A:def_24_:_
for C being initialized ConstructorSignature
for t1, t2 being expression of C
for f being valuation of C holds
( f unifies t1,t2 iff t1 at f = t2 at f );
theorem Th53: :: ABCMIZ_A:53
for C being initialized ConstructorSignature
for t1, t2 being expression of C
for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
proof
let C be initialized ConstructorSignature; ::_thesis: for t1, t2 being expression of C
for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
let t1, t2 be expression of C; ::_thesis: for f being valuation of C st f unifies t1,t2 holds
f unifies t2,t1
let f be valuation of C; ::_thesis: ( f unifies t1,t2 implies f unifies t2,t1 )
assume t1 at f = t2 at f ; :: according to ABCMIZ_A:def_24 ::_thesis: f unifies t2,t1
hence t2 at f = t1 at f ; :: according to ABCMIZ_A:def_24 ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
predt1,t2 are_unifiable means :: ABCMIZ_A:def 25
ex f being valuation of C st f unifies t1,t2;
reflexivity
for t1 being expression of C ex f being valuation of C st f unifies t1,t1
proof
let t be expression of C; ::_thesis: ex f being valuation of C st f unifies t,t
set f = the valuation of C;
take the valuation of C ; ::_thesis: the valuation of C unifies t,t
thus t at the valuation of C = t at the valuation of C ; :: according to ABCMIZ_A:def_24 ::_thesis: verum
end;
symmetry
for t1, t2 being expression of C st ex f being valuation of C st f unifies t1,t2 holds
ex f being valuation of C st f unifies t2,t1
proof
let t1, t2 be expression of C; ::_thesis: ( ex f being valuation of C st f unifies t1,t2 implies ex f being valuation of C st f unifies t2,t1 )
given f being valuation of C such that A1: f unifies t1,t2 ; ::_thesis: ex f being valuation of C st f unifies t2,t1
take f ; ::_thesis: f unifies t2,t1
thus t2 at f = t1 at f by A1, Def24; :: according to ABCMIZ_A:def_24 ::_thesis: verum
end;
end;
:: deftheorem defines are_unifiable ABCMIZ_A:def_25_:_
for C being initialized ConstructorSignature
for t1, t2 being expression of C holds
( t1,t2 are_unifiable iff ex f being valuation of C st f unifies t1,t2 );
definition
let C be initialized ConstructorSignature;
let t1, t2 be expression of C;
predt1,t2 are_weakly-unifiable means :: ABCMIZ_A:def 26
ex g being one-to-one irrelevant valuation of C st
( variables_in t2 c= dom g & t1,t2 at g are_unifiable );
reflexivity
for t1 being expression of C ex g being one-to-one irrelevant valuation of C st
( variables_in t1 c= dom g & t1,t1 at g are_unifiable )
proof
let t be expression of C; ::_thesis: ex g being one-to-one irrelevant valuation of C st
( variables_in t c= dom g & t,t at g are_unifiable )
take C idval (variables_in t) ; ::_thesis: ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable )
thus ( variables_in t c= dom (C idval (variables_in t)) & t,t at (C idval (variables_in t)) are_unifiable ) by ABCMIZ_1:131, ABCMIZ_1:137; ::_thesis: verum
end;
end;
:: deftheorem defines are_weakly-unifiable ABCMIZ_A:def_26_:_
for C being initialized ConstructorSignature
for t1, t2 being expression of C holds
( t1,t2 are_weakly-unifiable iff ex g being one-to-one irrelevant valuation of C st
( variables_in t2 c= dom g & t1,t2 at g are_unifiable ) );
theorem :: ABCMIZ_A:54
for C being initialized ConstructorSignature
for t1, t2 being expression of C st t1,t2 are_unifiable holds
t1,t2 are_weakly-unifiable
proof
let C be initialized ConstructorSignature; ::_thesis: for t1, t2 being expression of C st t1,t2 are_unifiable holds
t1,t2 are_weakly-unifiable
let t1, t2 be expression of C; ::_thesis: ( t1,t2 are_unifiable implies t1,t2 are_weakly-unifiable )
given f being valuation of C such that A1: f unifies t1,t2 ; :: according to ABCMIZ_A:def_25 ::_thesis: t1,t2 are_weakly-unifiable
take g = C idval (variables_in t2); :: according to ABCMIZ_A:def_26 ::_thesis: ( variables_in t2 c= dom g & t1,t2 at g are_unifiable )
thus variables_in t2 c= dom g by ABCMIZ_1:131; ::_thesis: t1,t2 at g are_unifiable
take f ; :: according to ABCMIZ_A:def_25 ::_thesis: f unifies t1,t2 at g
thus f unifies t1,t2 at g by A1, ABCMIZ_1:137; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
predt is_a_unification_of t1,t2 means :: ABCMIZ_A:def 27
ex f being valuation of C st
( f unifies t1,t2 & t = t1 at f );
end;
:: deftheorem defines is_a_unification_of ABCMIZ_A:def_27_:_
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_unification_of t1,t2 iff ex f being valuation of C st
( f unifies t1,t2 & t = t1 at f ) );
theorem :: ABCMIZ_A:55
for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
t is_a_unification_of t2,t1
proof
let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
t is_a_unification_of t2,t1
let t1, t2, t be expression of C; ::_thesis: ( t is_a_unification_of t1,t2 implies t is_a_unification_of t2,t1 )
given f being valuation of C such that A1: ( f unifies t1,t2 & t = t1 at f ) ; :: according to ABCMIZ_A:def_27 ::_thesis: t is_a_unification_of t2,t1
take f ; :: according to ABCMIZ_A:def_27 ::_thesis: ( f unifies t2,t1 & t = t2 at f )
thus ( f unifies t2,t1 & t = t2 at f ) by A1, Def24, Th53; ::_thesis: verum
end;
theorem :: ABCMIZ_A:56
for C being initialized ConstructorSignature
for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
( t matches_with t1 & t matches_with t2 )
proof
let C be initialized ConstructorSignature; ::_thesis: for t1, t2, t being expression of C st t is_a_unification_of t1,t2 holds
( t matches_with t1 & t matches_with t2 )
let t1, t2, t be expression of C; ::_thesis: ( t is_a_unification_of t1,t2 implies ( t matches_with t1 & t matches_with t2 ) )
given f being valuation of C such that A1: ( f unifies t1,t2 & t = t1 at f ) ; :: according to ABCMIZ_A:def_27 ::_thesis: ( t matches_with t1 & t matches_with t2 )
thus ex f being valuation of C st t = t1 at f by A1; :: according to ABCMIZ_A:def_21 ::_thesis: t matches_with t2
take f ; :: according to ABCMIZ_A:def_21 ::_thesis: t = t2 at f
thus t = t2 at f by A1, Def24; ::_thesis: verum
end;
definition
let C be initialized ConstructorSignature;
let t, t1, t2 be expression of C;
predt is_a_general-unification_of t1,t2 means :: ABCMIZ_A:def 28
( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds
u matches_with t ) );
end;
:: deftheorem defines is_a_general-unification_of ABCMIZ_A:def_28_:_
for C being initialized ConstructorSignature
for t, t1, t2 being expression of C holds
( t is_a_general-unification_of t1,t2 iff ( t is_a_unification_of t1,t2 & ( for u being expression of C st u is_a_unification_of t1,t2 holds
u matches_with t ) ) );
begin
theorem Th57: :: ABCMIZ_A:57
for n being Nat
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n
proof
set C = MaxConstrSign ;
let n be Nat; ::_thesis: for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s st len (the_arity_of m) = n
let s be SortSymbol of MaxConstrSign; ::_thesis: ex m being constructor OperSymbol of s st len (the_arity_of m) = n
deffunc H1( Nat) -> set = [{},$1];
consider l being FinSequence such that
A1: len l = n and
A2: for i being Nat st i in dom l holds
l . i = H1(i) from FINSEQ_1:sch_2();
A3: l is one-to-one
proof
let i, j be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not i in proj1 l or not j in proj1 l or not l . i = l . j or i = j )
assume A4: ( i in dom l & j in dom l & l . i = l . j ) ; ::_thesis: i = j
reconsider i = i, j = j as Nat by A4;
( l . i = H1(i) & l . i = H1(j) ) by A2, A4;
then i = H1(j) `2 by MCART_1:7;
hence i = j ; ::_thesis: verum
end;
rng l c= Vars
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng l or z in Vars )
assume z in rng l ; ::_thesis: z in Vars
then consider a being set such that
A5: ( a in dom l & z = l . a ) by FUNCT_1:def_3;
reconsider a = a as Nat by A5;
z = H1(a) by A2, A5;
hence z in Vars by ABCMIZ_1:25; ::_thesis: verum
end;
then reconsider l = l as one-to-one FinSequence of Vars by A3, FINSEQ_1:def_4;
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
let i be Nat; ::_thesis: 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 )
let x be variable; ::_thesis: ( i in dom l & x = l . i implies for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) )
assume ( i in dom l & x = l . i ) ; ::_thesis: for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j )
then x = H1(i) by A2;
hence for y being variable st y in vars x holds
ex j being Nat st
( j in dom l & j < i & y = l . j ) by MCART_1:7; ::_thesis: verum
end;
then reconsider l = l as quasi-loci by ABCMIZ_1:30;
set m = [s,[l,0]];
the carrier of MaxConstrSign = {a_Type,an_Adj,a_Term} by ABCMIZ_1:def_9;
then A6: [s,[l,0]] in Constructors by Th28;
then [s,[l,0]] in {*,non_op} \/ Constructors by XBOOLE_0:def_3;
then reconsider m = [s,[l,0]] as constructor OperSymbol of MaxConstrSign by A6, Th42, ABCMIZ_1:def_24;
the_result_sort_of m = m `1 by ABCMIZ_1:def_24
.= s by MCART_1:7 ;
then reconsider m = m as constructor OperSymbol of s by ABCMIZ_1:def_32;
take m ; ::_thesis: len (the_arity_of m) = n
thus len (the_arity_of m) = card ((m `2) `1) by ABCMIZ_1:def_24
.= card ([l,0] `1) by MCART_1:7
.= card l
.= n by A1 ; ::_thesis: verum
end;
theorem Th58: :: ABCMIZ_A:58
for l being quasi-loci
for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
proof
let l be quasi-loci; ::_thesis: for s being SortSymbol of MaxConstrSign
for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
set X = rng l;
set n = len l;
set C = MaxConstrSign ;
let s be SortSymbol of MaxConstrSign; ::_thesis: for m being constructor OperSymbol of s st len (the_arity_of m) = len l holds
variables_in (m -trm (args l)) = rng l
let m be constructor OperSymbol of s; ::_thesis: ( len (the_arity_of m) = len l implies variables_in (m -trm (args l)) = rng l )
assume A1: len (the_arity_of m) = len l ; ::_thesis: variables_in (m -trm (args l)) = rng l
set p = args l;
set Y = { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ;
A2: len (args l) = len (the_arity_of m) by A1, Def18;
then A3: variables_in (m -trm (args l)) = union { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } by ABCMIZ_1:90;
A4: dom (args l) = dom l by A1, A2, FINSEQ_3:29;
thus variables_in (m -trm (args l)) c= rng l :: according to XBOOLE_0:def_10 ::_thesis: rng l c= variables_in (m -trm (args l))
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in variables_in (m -trm (args l)) or s in rng l )
assume s in variables_in (m -trm (args l)) ; ::_thesis: s in rng l
then consider A being set such that
A5: ( s in A & A in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by A3, TARSKI:def_4;
consider t being quasi-term of MaxConstrSign such that
A6: ( A = variables_in t & t in rng (args l) ) by A5;
consider z being set such that
A7: ( z in dom (args l) & t = (args l) . z ) by A6, FUNCT_1:def_3;
reconsider z = z as Element of NAT by A7;
l . z = l /. z by A4, A7, PARTFUN1:def_6;
then A8: l /. z in rng l by A4, A7, FUNCT_1:def_3;
(args l) . z = (l /. z) -term MaxConstrSign by A4, A7, Def18;
then A = {(l /. z)} by A6, A7, ABCMIZ_1:86;
hence s in rng l by A5, A8, TARSKI:def_1; ::_thesis: verum
end;
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in rng l or s in variables_in (m -trm (args l)) )
assume s in rng l ; ::_thesis: s in variables_in (m -trm (args l))
then consider z being set such that
A9: ( z in dom l & s = l . z ) by FUNCT_1:def_3;
reconsider z = z as Element of NAT by A9;
set t = (l /. z) -term MaxConstrSign;
( (args l) . z = (l /. z) -term MaxConstrSign & l . z = l /. z ) by A9, Def18, PARTFUN1:def_6;
then ( variables_in ((l /. z) -term MaxConstrSign) = {s} & (l /. z) -term MaxConstrSign in rng (args l) ) by A4, A9, ABCMIZ_1:86, FUNCT_1:def_3;
then ( s in {s} & {s} in { (variables_in t) where t is quasi-term of MaxConstrSign : t in rng (args l) } ) by TARSKI:def_1;
hence s in variables_in (m -trm (args l)) by A3, TARSKI:def_4; ::_thesis: verum
end;
theorem Th59: :: ABCMIZ_A:59
for X being finite Subset of Vars st varcl X = X holds
for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
proof
let X be finite Subset of Vars; ::_thesis: ( varcl X = X implies for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X ) )
assume A1: varcl X = X ; ::_thesis: for s being SortSymbol of MaxConstrSign ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
then consider l being quasi-loci such that
A2: rng l = X by Th31;
set n = len l;
set C = MaxConstrSign ;
let s be SortSymbol of MaxConstrSign; ::_thesis: ex m being constructor OperSymbol of s ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
consider m being constructor OperSymbol of s such that
A3: len (the_arity_of m) = len l by Th57;
take m ; ::_thesis: ex p being FinSequence of QuasiTerms MaxConstrSign st
( len p = len (the_arity_of m) & vars (m -trm p) = X )
set p = args l;
take args l ; ::_thesis: ( len (args l) = len (the_arity_of m) & vars (m -trm (args l)) = X )
thus len (args l) = len (the_arity_of m) by A3, Def18; ::_thesis: vars (m -trm (args l)) = X
thus vars (m -trm (args l)) = X by A1, A2, A3, Th58; ::_thesis: verum
end;
definition
let d be PartFunc of Vars,QuasiTypes;
attrd is even means :Def29: :: ABCMIZ_A:def 29
for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x;
end;
:: deftheorem Def29 defines even ABCMIZ_A:def_29_:_
for d being PartFunc of Vars,QuasiTypes holds
( d is even iff for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x );
definition
let l be quasi-loci;
mode type-distribution of l -> PartFunc of Vars,QuasiTypes means :Def30: :: ABCMIZ_A:def 30
( dom it = rng l & it is even );
existence
ex b1 being PartFunc of Vars,QuasiTypes st
( dom b1 = rng l & b1 is even )
proof
defpred S1[ set , set ] means ex x being variable ex T being quasi-type st
( $1 = x & $2 = T & vars T = vars x );
A1: for z being set st z in rng l holds
ex y being set st S1[z,y]
proof
set C = MaxConstrSign ;
let z be set ; ::_thesis: ( z in rng l implies ex y being set st S1[z,y] )
assume z in rng l ; ::_thesis: ex y being set st S1[z,y]
then reconsider x = z as variable ;
varcl (vars x) = vars x by Th2;
then consider m being constructor OperSymbol of a_Type MaxConstrSign, p being FinSequence of QuasiTerms MaxConstrSign such that
A2: ( len p = len (the_arity_of m) & vars (m -trm p) = vars x ) by Th59;
( a_Type MaxConstrSign in the carrier of MaxConstrSign & the carrier of MaxConstrSign c= rng the ResultSort of MaxConstrSign ) by ABCMIZ_1:def_54;
then consider o being set such that
A3: ( o in dom the ResultSort of MaxConstrSign & a_Type MaxConstrSign = the ResultSort of MaxConstrSign . o ) by FUNCT_1:def_3;
reconsider o = o as OperSymbol of MaxConstrSign by A3;
the_result_sort_of o = a_Type MaxConstrSign by A3;
then the_result_sort_of m = a_Type MaxConstrSign by ABCMIZ_1:def_32;
then reconsider q = m -trm p as pure expression of MaxConstrSign , a_Type MaxConstrSign by A2, ABCMIZ_1:75;
set B = {} (QuasiAdjs MaxConstrSign);
reconsider T = ({} (QuasiAdjs MaxConstrSign)) ast q as quasi-type ;
take T ; ::_thesis: S1[z,T]
take x ; ::_thesis: ex T being quasi-type st
( z = x & T = T & vars T = vars x )
take T ; ::_thesis: ( z = x & T = T & vars T = vars x )
thus ( z = x & T = T & vars T = vars x ) by A2, ABCMIZ_1:106; ::_thesis: verum
end;
consider f being Function such that
A4: dom f = rng l and
A5: for z being set st z in rng l holds
S1[z,f . z] from CLASSES1:sch_1(A1);
rng f c= QuasiTypes
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in QuasiTypes )
assume y in rng f ; ::_thesis: y in QuasiTypes
then consider z being set such that
A6: ( z in dom f & y = f . z ) by FUNCT_1:def_3;
S1[z,y] by A4, A5, A6;
hence y in QuasiTypes by ABCMIZ_1:def_43; ::_thesis: verum
end;
then reconsider f = f as PartFunc of Vars,QuasiTypes by A4, RELSET_1:4;
take f ; ::_thesis: ( dom f = rng l & f is even )
thus dom f = rng l by A4; ::_thesis: f is even
let x be variable; :: according to ABCMIZ_A:def_29 ::_thesis: for T being quasi-type st x in dom f & T = f . x holds
vars T = vars x
let T be quasi-type; ::_thesis: ( x in dom f & T = f . x implies vars T = vars x )
assume ( x in dom f & T = f . x ) ; ::_thesis: vars T = vars x
then S1[x,T] by A4, A5;
hence vars T = vars x ; ::_thesis: verum
end;
end;
:: deftheorem Def30 defines type-distribution ABCMIZ_A:def_30_:_
for l being quasi-loci
for b2 being PartFunc of Vars,QuasiTypes holds
( b2 is type-distribution of l iff ( dom b2 = rng l & b2 is even ) );
theorem :: ABCMIZ_A:60
for l being empty quasi-loci holds {} is type-distribution of l
proof
let l be empty quasi-loci; ::_thesis: {} is type-distribution of l
reconsider d = {} as PartFunc of Vars,QuasiTypes by RELSET_1:12;
for x being variable
for T being quasi-type st x in dom d & T = d . x holds
vars T = vars x ;
then ( dom d = rng l & d is even ) by Def29;
hence {} is type-distribution of l by Def30; ::_thesis: verum
end;