begin
theorem Lem5:
scheme
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
P1:
for
x,
y being
set st
x in F1() &
y in F1() &
P1[
x,
y] holds
not
P1[
y,
x]
and P2:
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]
scheme
FiniteC{
F1()
-> finite set ,
P1[
set ] } :
provided
P:
for
A being
Subset of
F1() st ( for
B being
set st
B c< A holds
P1[
B] ) holds
P1[
A]
scheme
Numeration{
F1()
-> finite set ,
P1[
set ,
set ] } :
provided
P1:
for
x,
y being
set st
x in F1() &
y in F1() &
P1[
x,
y] holds
not
P1[
y,
x]
and P2:
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]
theorem Th00:
theorem CompoundDef:
begin
:: deftheorem StandardizedDef 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 Lem0:
:: 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 ;
theorem
theorem
theorem Lem1:
theorem Lem2:
theorem
theorem Lem3:
theorem Th49:
theorem Th46:
theorem Th47:
theorem Th50:
theorem
theorem
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
theorem Th55:
theorem Th56:
theorem
theorem Th57:
theorem
theorem
begin
set MC = MaxConstrSign ;
:: 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 ;
:: deftheorem defines set-constr ABCMIZ_A:def 6 :
set-constr = [a_Type ,[{} ,0 ]];
theorem
theorem ThCs:
theorem Th23:
theorem Th24:
theorem ThLoci:
theorem ThA1:
:: 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 MCON 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 ThS0:
theorem
theorem ThM1:
:: deftheorem CONSTR 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 ) );
theorem
begin
:: deftheorem ARdef 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 not { o where o is OperSymbol of C : ( the_result_sort_of o = s & len (the_arity_of o) = n ) } is finite );
:: deftheorem Ndef 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 Udef 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 Bdef 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 ThDiff:
theorem ThInit:
theorem Th43a:
:: deftheorem defines @ ABCMIZ_A:def 16 :
for c being Element of Constructors holds @ c = c;
theorem
:: deftheorem defines set-type ABCMIZ_A:def 17 :
set-type = ({} (QuasiAdjs MaxConstrSign )) ast ((@ set-constr ) term );
theorem
:: deftheorem ARGSL 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 ) ) );
:: 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 ThCc:
theorem
theorem
theorem
theorem
theorem
:: 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
theorem
begin
:: 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
:: 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
:: 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
:: deftheorem U1 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 U2:
:: 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 );
:: 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
:: 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
theorem
:: 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 Th61:
theorem Th63:
theorem Th62:
:: deftheorem EV 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 );
:: deftheorem TD 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