:: Many Sorted Algebras
:: by Andrzej Trybulec
::
:: Received April 21, 1994
:: Copyright (c) 1994 Association of Mizar Users
:: deftheorem MSUALG_1:def 1 :
canceled;
:: deftheorem MSUALG_1:def 2 :
canceled;
:: deftheorem MSUALG_1:def 3 :
canceled;
:: deftheorem MSUALG_1:def 4 :
canceled;
:: deftheorem MSUALG_1:def 5 :
canceled;
:: deftheorem defines the_arity_of MSUALG_1:def 6 :
:: deftheorem defines the_result_sort_of MSUALG_1:def 7 :
:: deftheorem Def8 defines non-empty MSUALG_1:def 8 :
:: deftheorem defines Args MSUALG_1:def 9 :
:: deftheorem defines Result MSUALG_1:def 10 :
:: deftheorem defines Den MSUALG_1:def 11 :
theorem :: MSUALG_1:1
canceled;
theorem :: MSUALG_1:2
canceled;
theorem :: MSUALG_1:3
canceled;
theorem :: MSUALG_1:4
canceled;
theorem :: MSUALG_1:5
canceled;
theorem :: MSUALG_1:6
Lm1:
for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of D * ,D holds dom h = (arity h) -tuples_on D
theorem Th7: :: MSUALG_1:7
theorem Th8: :: MSUALG_1:8
theorem Th9: :: MSUALG_1:9
:: deftheorem Def12 defines segmental MSUALG_1:def 12 :
theorem Th10: :: MSUALG_1:10
reconsider z = 0 as Element of {0 } by TARSKI:def 1;
Lm2:
for A being Universal_Algebra
for f being Function of dom (signature A),{0 } * holds
( not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is empty & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is trivial & not ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0 },(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
:: deftheorem Def13 defines MSSign MSUALG_1:def 13 :
:: deftheorem defines MSSorts MSUALG_1:def 14 :
:: deftheorem defines MSCharact MSUALG_1:def 15 :
:: deftheorem defines MSAlg MSUALG_1:def 16 :
:: deftheorem Def17 defines the_sort_of MSUALG_1:def 17 :
theorem Th11: :: MSUALG_1:11
theorem Th12: :: MSUALG_1:12
theorem Th13: :: MSUALG_1:13
theorem Th14: :: MSUALG_1:14
:: deftheorem defines the_charact_of MSUALG_1:def 18 :
:: deftheorem defines 1-Alg MSUALG_1:def 19 :
theorem :: MSUALG_1:15
theorem :: MSUALG_1:16