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 :
theorem Lem0:
:: deftheorem defines loci_of ABCMIZ_A:def 2 :
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 :
:: deftheorem defines QuasiTerms ABCMIZ_A:def 4 :
:: deftheorem defines QuasiTypes ABCMIZ_A:def 5 :
:: deftheorem defines set-constr ABCMIZ_A:def 6 :
theorem
theorem ThCs:
theorem Th23:
theorem Th24:
theorem ThLoci:
theorem ThA1:
:: deftheorem defines subexpression ABCMIZ_A:def 7 :
:: deftheorem defines constrs ABCMIZ_A:def 8 :
:: deftheorem MCON defines main-constr ABCMIZ_A:def 9 :
:: deftheorem defines args ABCMIZ_A:def 10 :
theorem ThS0:
theorem
theorem ThM1:
:: deftheorem CONSTR defines constructor ABCMIZ_A:def 11 :
theorem
begin
:: deftheorem ARdef defines arity-rich ABCMIZ_A:def 12 :
:: deftheorem Ndef defines nullary ABCMIZ_A:def 13 :
:: deftheorem Udef defines unary ABCMIZ_A:def 14 :
:: deftheorem Bdef defines binary ABCMIZ_A:def 15 :
theorem ThDiff:
theorem ThInit:
theorem Th43a:
:: deftheorem defines @ ABCMIZ_A:def 16 :
theorem
:: deftheorem defines set-type ABCMIZ_A:def 17 :
theorem
:: deftheorem ARGSL defines args ABCMIZ_A:def 18 :
:: deftheorem defines base_exp_of ABCMIZ_A:def 19 :
theorem ThCc:
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines constrs ABCMIZ_A:def 20 :
theorem
theorem
begin
:: deftheorem defines matches_with ABCMIZ_A:def 21 :
theorem
:: deftheorem defines matches_with ABCMIZ_A:def 22 :
theorem
:: deftheorem defines matches_with ABCMIZ_A:def 23 :
theorem
:: deftheorem U1 defines unifies ABCMIZ_A:def 24 :
theorem U2:
:: deftheorem defines are_unifiable ABCMIZ_A:def 25 :
:: deftheorem defines are_weakly-unifiable ABCMIZ_A:def 26 :
theorem
:: deftheorem defines is_a_unification_of ABCMIZ_A:def 27 :
theorem
theorem
:: deftheorem defines is_a_general-unification_of ABCMIZ_A:def 28 :
begin
theorem Th61:
theorem Th63:
theorem Th62:
:: deftheorem EV defines even ABCMIZ_A:def 29 :
:: deftheorem TD defines type-distribution ABCMIZ_A:def 30 :
theorem