:: STRUCT_0 semantic presentation
begin
definition
attrc1 is strict ;
struct 1-sorted -> ;
aggr1-sorted(# carrier #) -> 1-sorted ;
sel carrier c1 -> set ;
end;
definition
let S be 1-sorted ;
attrS is empty means :Def1: :: STRUCT_0:def 1
the carrier of S is empty ;
end;
:: deftheorem Def1 defines empty STRUCT_0:def_1_:_
for S being 1-sorted holds
( S is empty iff the carrier of S is empty );
registration
cluster strict empty for 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is empty )
proof
take T = 1-sorted(# {} #); ::_thesis: ( T is strict & T is empty )
thus T is strict ; ::_thesis: T is empty
thus the carrier of T is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
registration
cluster strict non empty for 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & not b1 is empty )
proof
take 1-sorted(# {{}} #) ; ::_thesis: ( 1-sorted(# {{}} #) is strict & not 1-sorted(# {{}} #) is empty )
thus 1-sorted(# {{}} #) is strict ; ::_thesis: not 1-sorted(# {{}} #) is empty
thus not the carrier of 1-sorted(# {{}} #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
registration
let S be empty 1-sorted ;
cluster the carrier of S -> empty ;
coherence
the carrier of S is empty by Def1;
end;
registration
let S be non empty 1-sorted ;
cluster the carrier of S -> non empty ;
coherence
not the carrier of S is empty by Def1;
end;
definition
let S be 1-sorted ;
mode Element of S is Element of the carrier of S;
mode Subset of S is Subset of the carrier of S;
mode Subset-Family of S is Subset-Family of the carrier of S;
end;
definition
let S be 1-sorted ;
let X be set ;
mode Function of S,X is Function of the carrier of S,X;
mode Function of X,S is Function of X, the carrier of S;
end;
definition
let S, T be 1-sorted ;
mode Function of S,T is Function of the carrier of S, the carrier of T;
end;
definition
let T be 1-sorted ;
func {} T -> Subset of T equals :: STRUCT_0:def 2
{} ;
coherence
{} is Subset of T
proof
{} = {} the carrier of T ;
hence {} is Subset of T ; ::_thesis: verum
end;
func [#] T -> Subset of T equals :: STRUCT_0:def 3
the carrier of T;
coherence
the carrier of T is Subset of T
proof
the carrier of T = [#] the carrier of T ;
hence the carrier of T is Subset of T ; ::_thesis: verum
end;
end;
:: deftheorem defines {} STRUCT_0:def_2_:_
for T being 1-sorted holds {} T = {} ;
:: deftheorem defines [#] STRUCT_0:def_3_:_
for T being 1-sorted holds [#] T = the carrier of T;
registration
let T be 1-sorted ;
cluster {} T -> empty ;
coherence
{} T is empty ;
end;
registration
let T be empty 1-sorted ;
cluster [#] T -> empty ;
coherence
[#] T is empty ;
end;
registration
let T be non empty 1-sorted ;
cluster [#] T -> non empty ;
coherence
not [#] T is empty ;
end;
registration
let S be non empty 1-sorted ;
cluster non empty for Element of bool the carrier of S;
existence
not for b1 being Subset of S holds b1 is empty
proof
take [#] S ; ::_thesis: not [#] S is empty
thus not [#] S is empty ; ::_thesis: verum
end;
end;
definition
let S be 1-sorted ;
mode FinSequence of S is FinSequence of the carrier of S;
end;
definition
let S be 1-sorted ;
mode ManySortedSet of S is ManySortedSet of the carrier of S;
end;
definition
let S be 1-sorted ;
func id S -> Function of S,S equals :: STRUCT_0:def 4
id the carrier of S;
coherence
id the carrier of S is Function of S,S ;
end;
:: deftheorem defines id STRUCT_0:def_4_:_
for S being 1-sorted holds id S = id the carrier of S;
definition
let S be 1-sorted ;
mode sequence of S is sequence of the carrier of S;
end;
definition
let S be 1-sorted ;
let X be set ;
mode PartFunc of S,X is PartFunc of the carrier of S,X;
mode PartFunc of X,S is PartFunc of X, the carrier of S;
end;
definition
let S, T be 1-sorted ;
mode PartFunc of S,T is PartFunc of the carrier of S, the carrier of T;
end;
definition
let S be 1-sorted ;
let x be set ;
predx in S means :: STRUCT_0:def 5
x in the carrier of S;
end;
:: deftheorem defines in STRUCT_0:def_5_:_
for S being 1-sorted
for x being set holds
( x in S iff x in the carrier of S );
definition
attrc1 is strict ;
struct ZeroStr -> 1-sorted ;
aggrZeroStr(# carrier, ZeroF #) -> ZeroStr ;
sel ZeroF c1 -> Element of the carrier of c1;
end;
registration
cluster non empty strict for ZeroStr ;
existence
ex b1 being ZeroStr st
( b1 is strict & not b1 is empty )
proof
set A = the non empty set ;
set a = the Element of the non empty set ;
take ZeroStr(# the non empty set , the Element of the non empty set #) ; ::_thesis: ( ZeroStr(# the non empty set , the Element of the non empty set #) is strict & not ZeroStr(# the non empty set , the Element of the non empty set #) is empty )
thus ZeroStr(# the non empty set , the Element of the non empty set #) is strict ; ::_thesis: not ZeroStr(# the non empty set , the Element of the non empty set #) is empty
thus not the carrier of ZeroStr(# the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;
definition
attrc1 is strict ;
struct OneStr -> 1-sorted ;
aggrOneStr(# carrier, OneF #) -> OneStr ;
sel OneF c1 -> Element of the carrier of c1;
end;
definition
attrc1 is strict ;
struct ZeroOneStr -> ZeroStr , OneStr ;
aggrZeroOneStr(# carrier, ZeroF, OneF #) -> ZeroOneStr ;
end;
definition
let S be ZeroStr ;
func 0. S -> Element of S equals :: STRUCT_0:def 6
the ZeroF of S;
coherence
the ZeroF of S is Element of S ;
end;
:: deftheorem defines 0. STRUCT_0:def_6_:_
for S being ZeroStr holds 0. S = the ZeroF of S;
definition
let S be OneStr ;
func 1. S -> Element of S equals :: STRUCT_0:def 7
the OneF of S;
coherence
the OneF of S is Element of S ;
end;
:: deftheorem defines 1. STRUCT_0:def_7_:_
for S being OneStr holds 1. S = the OneF of S;
definition
let S be ZeroOneStr ;
attrS is degenerated means :Def8: :: STRUCT_0:def 8
0. S = 1. S;
end;
:: deftheorem Def8 defines degenerated STRUCT_0:def_8_:_
for S being ZeroOneStr holds
( S is degenerated iff 0. S = 1. S );
definition
let IT be 1-sorted ;
attrIT is trivial means :Def9: :: STRUCT_0:def 9
the carrier of IT is trivial ;
end;
:: deftheorem Def9 defines trivial STRUCT_0:def_9_:_
for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );
registration
cluster empty -> trivial for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is empty holds
b1 is trivial
proof
let S be 1-sorted ; ::_thesis: ( S is empty implies S is trivial )
assume the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is trivial
hence the carrier of S is trivial ; :: according to STRUCT_0:def_9 ::_thesis: verum
end;
cluster non trivial -> non empty for 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty ;
end;
definition
let S be 1-sorted ;
redefine attr S is trivial means :Def10: :: STRUCT_0:def 10
for x, y being Element of S holds x = y;
compatibility
( S is trivial iff for x, y being Element of S holds x = y )
proof
set I = the carrier of S;
percases ( not the carrier of S is empty or the carrier of S is empty ) ;
supposeA1: not the carrier of S is empty ; ::_thesis: ( S is trivial iff for x, y being Element of S holds x = y )
thus ( S is trivial implies for x, y being Element of the carrier of S holds x = y ) ::_thesis: ( ( for x, y being Element of S holds x = y ) implies S is trivial )
proof
assume A2: the carrier of S is trivial ; :: according to STRUCT_0:def_9 ::_thesis: for x, y being Element of the carrier of S holds x = y
let x, y be Element of the carrier of S; ::_thesis: x = y
thus x = y by A2, A1, ZFMISC_1:def_10; ::_thesis: verum
end;
assume A3: for x, y being Element of the carrier of S holds x = y ; ::_thesis: S is trivial
let x, y be set ; :: according to ZFMISC_1:def_10,STRUCT_0:def_9 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or x = y )
thus ( not x in the carrier of S or not y in the carrier of S or x = y ) by A3; ::_thesis: verum
end;
supposeA4: the carrier of S is empty ; ::_thesis: ( S is trivial iff for x, y being Element of S holds x = y )
for x, y being Element of the carrier of S holds x = y
proof
let x, y be Element of the carrier of S; ::_thesis: x = y
thus x = {} by A4, SUBSET_1:def_1
.= y by A4, SUBSET_1:def_1 ; ::_thesis: verum
end;
hence ( S is trivial iff for x, y being Element of S holds x = y ) by A4; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def10 defines trivial STRUCT_0:def_10_:_
for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y );
registration
cluster non degenerated -> non trivial for ZeroOneStr ;
coherence
for b1 being ZeroOneStr st not b1 is degenerated holds
not b1 is trivial
proof
let L be ZeroOneStr ; ::_thesis: ( not L is degenerated implies not L is trivial )
assume A1: not L is degenerated ; ::_thesis: not L is trivial
assume L is trivial ; ::_thesis: contradiction
then 0. L = 1. L by Def10;
hence contradiction by A1, Def8; ::_thesis: verum
end;
end;
registration
cluster strict non empty trivial for 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is trivial & not b1 is empty & b1 is strict )
proof
take 1-sorted(# 1 #) ; ::_thesis: ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict )
thus ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict ) by Def9, CARD_1:49; ::_thesis: verum
end;
cluster strict non trivial for 1-sorted ;
existence
ex b1 being 1-sorted st
( not b1 is trivial & b1 is strict )
proof
take Y = 1-sorted(# 2 #); ::_thesis: ( not Y is trivial & Y is strict )
reconsider x = 0 , y = 1 as Element of Y by CARD_1:50, TARSKI:def_2;
x <> y ;
hence ( not Y is trivial & Y is strict ) by Def10; ::_thesis: verum
end;
end;
registration
let S be non trivial 1-sorted ;
cluster the carrier of S -> non trivial ;
coherence
not the carrier of S is trivial by Def9;
end;
registration
let S be trivial 1-sorted ;
cluster the carrier of S -> trivial ;
coherence
the carrier of S is trivial by Def9;
end;
begin
definition
let S be 1-sorted ;
attrS is finite means :Def11: :: STRUCT_0:def 11
the carrier of S is finite ;
end;
:: deftheorem Def11 defines finite STRUCT_0:def_11_:_
for S being 1-sorted holds
( S is finite iff the carrier of S is finite );
registration
cluster strict non empty finite for 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is finite & not b1 is empty )
proof
take 1-sorted(# {{}} #) ; ::_thesis: ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty )
thus ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty ) by Def11; ::_thesis: verum
end;
end;
registration
let S be finite 1-sorted ;
cluster the carrier of S -> finite ;
coherence
the carrier of S is finite by Def11;
end;
registration
cluster empty -> empty finite for 1-sorted ;
coherence
for b1 being empty 1-sorted holds b1 is finite
proof
let S be empty 1-sorted ; ::_thesis: S is finite
thus the carrier of S is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;
notation
let S be 1-sorted ;
antonym infinite S for finite ;
end;
registration
cluster strict infinite for 1-sorted ;
existence
ex b1 being 1-sorted st
( b1 is strict & b1 is infinite )
proof
take A = 1-sorted(# the infinite set #); ::_thesis: ( A is strict & A is infinite )
thus A is strict ; ::_thesis: A is infinite
thus the carrier of A is infinite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;
registration
let S be infinite 1-sorted ;
cluster the carrier of S -> infinite ;
coherence
not the carrier of S is finite by Def11;
end;
registration
cluster infinite -> non empty infinite for 1-sorted ;
coherence
for b1 being infinite 1-sorted holds not b1 is empty ;
end;
registration
cluster trivial -> finite for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is trivial holds
b1 is finite
proof
let S be 1-sorted ; ::_thesis: ( S is trivial implies S is finite )
assume S is trivial ; ::_thesis: S is finite
then reconsider C = the carrier of S as trivial set ;
C is finite ;
hence the carrier of S is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;
registration
cluster infinite -> non trivial for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is infinite holds
not b1 is trivial ;
end;
definition
let S be ZeroStr ;
let x be Element of S;
attrx is zero means :Def12: :: STRUCT_0:def 12
x = 0. S;
end;
:: deftheorem Def12 defines zero STRUCT_0:def_12_:_
for S being ZeroStr
for x being Element of S holds
( x is zero iff x = 0. S );
registration
let S be ZeroStr ;
cluster 0. S -> zero ;
coherence
0. S is zero by Def12;
end;
registration
cluster strict non degenerated for ZeroOneStr ;
existence
ex b1 being ZeroOneStr st
( b1 is strict & not b1 is degenerated )
proof
take S = ZeroOneStr(# 2,(In (0,2)),(In (1,2)) #); ::_thesis: ( S is strict & not S is degenerated )
0 in 2 by CARD_1:50, TARSKI:def_2;
then ( 1 in 2 & In (0,2) = 0 ) by CARD_1:50, FUNCT_7:def_1, TARSKI:def_2;
then 0. S <> 1. S by FUNCT_7:def_1;
hence ( S is strict & not S is degenerated ) by Def8; ::_thesis: verum
end;
end;
registration
let S be non degenerated ZeroOneStr ;
cluster 1. S -> non zero ;
coherence
not 1. S is zero
proof
0. S <> 1. S by Def8;
hence not 1. S is zero by Def12; ::_thesis: verum
end;
end;
definition
let S be 1-sorted ;
mode Cover of S is Cover of the carrier of S;
end;
registration
let S be 1-sorted ;
cluster [#] S -> non proper ;
coherence
not [#] S is proper
proof
thus [#] S = the carrier of S ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;
begin
definition
attrc1 is strict ;
struct 2-sorted -> 1-sorted ;
aggr2-sorted(# carrier, carrier' #) -> 2-sorted ;
sel carrier' c1 -> set ;
end;
definition
let S be 2-sorted ;
attrS is void means :Def13: :: STRUCT_0:def 13
the carrier' of S is empty ;
end;
:: deftheorem Def13 defines void STRUCT_0:def_13_:_
for S being 2-sorted holds
( S is void iff the carrier' of S is empty );
registration
cluster empty strict void for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void )
proof
take S = 2-sorted(# {},{} #); ::_thesis: ( S is strict & S is empty & S is void )
thus S is strict ; ::_thesis: ( S is empty & S is void )
thus the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is void
thus the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;
registration
let S be void 2-sorted ;
cluster the carrier' of S -> empty ;
coherence
the carrier' of S is empty by Def13;
end;
registration
cluster non empty strict non void for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void )
proof
take S = 2-sorted(# 1,1 #); ::_thesis: ( S is strict & not S is empty & not S is void )
thus S is strict ; ::_thesis: ( not S is empty & not S is void )
thus not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: not S is void
thus not the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;
registration
let S be non void 2-sorted ;
cluster the carrier' of S -> non empty ;
coherence
not the carrier' of S is empty by Def13;
end;
definition
let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;
funcX --> y -> Function of X,Y equals :: STRUCT_0:def 14
the carrier of X --> y;
coherence
the carrier of X --> y is Function of X,Y ;
end;
:: deftheorem defines --> STRUCT_0:def_14_:_
for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;
registration
let S be ZeroStr ;
cluster zero for Element of the carrier of S;
existence
ex b1 being Element of S st b1 is zero
proof
take 0. S ; ::_thesis: 0. S is zero
thus 0. S = 0. S ; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
end;
registration
cluster strict non trivial for ZeroStr ;
existence
ex b1 being ZeroStr st
( b1 is strict & not b1 is trivial )
proof
take ZeroStr(# 2,(In (0,2)) #) ; ::_thesis: ( ZeroStr(# 2,(In (0,2)) #) is strict & not ZeroStr(# 2,(In (0,2)) #) is trivial )
( 0 in 2 & 1 in 2 ) by CARD_1:50, TARSKI:def_2;
hence ( ZeroStr(# 2,(In (0,2)) #) is strict & not ZeroStr(# 2,(In (0,2)) #) is trivial ) by Def10; ::_thesis: verum
end;
end;
registration
let S be non trivial ZeroStr ;
cluster non zero for Element of the carrier of S;
existence
not for b1 being Element of S holds b1 is zero
proof
consider x, y being Element of S such that
A1: x <> y by Def10;
percases ( x <> 0. S or y <> 0. S ) by A1;
supposeA2: x <> 0. S ; ::_thesis: not for b1 being Element of S holds b1 is zero
take x ; ::_thesis: not x is zero
thus x <> 0. S by A2; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
supposeA3: y <> 0. S ; ::_thesis: not for b1 being Element of S holds b1 is zero
take y ; ::_thesis: not y is zero
thus y <> 0. S by A3; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
end;
end;
end;
definition
let X be set ;
let S be ZeroStr ;
let R be Relation of X, the carrier of S;
attrR is non-zero means :: STRUCT_0:def 15
not 0. S in rng R;
end;
:: deftheorem defines non-zero STRUCT_0:def_15_:_
for X being set
for S being ZeroStr
for R being Relation of X, the carrier of S holds
( R is non-zero iff not 0. S in rng R );
definition
let S be 1-sorted ;
func card S -> Cardinal equals :: STRUCT_0:def 16
card the carrier of S;
coherence
card the carrier of S is Cardinal ;
end;
:: deftheorem defines card STRUCT_0:def_16_:_
for S being 1-sorted holds card S = card the carrier of S;
definition
let S be 1-sorted ;
mode UnOp of S is UnOp of the carrier of S;
mode BinOp of S is BinOp of the carrier of S;
end;
definition
let S be ZeroStr ;
func NonZero S -> Subset of S equals :: STRUCT_0:def 17
([#] S) \ {(0. S)};
coherence
([#] S) \ {(0. S)} is Subset of S ;
end;
:: deftheorem defines NonZero STRUCT_0:def_17_:_
for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};
theorem :: STRUCT_0:1
for S being non empty ZeroStr
for u being Element of S holds
( u in NonZero S iff not u is zero )
proof
let S be non empty ZeroStr ; ::_thesis: for u being Element of S holds
( u in NonZero S iff not u is zero )
let u be Element of S; ::_thesis: ( u in NonZero S iff not u is zero )
thus ( u in NonZero S implies not u is zero ) ::_thesis: ( not u is zero implies u in NonZero S )
proof
assume u in NonZero S ; ::_thesis: not u is zero
then u <> 0. S by ZFMISC_1:56;
hence not u is zero by Def12; ::_thesis: verum
end;
thus ( not u is zero implies u in NonZero S ) by ZFMISC_1:56; ::_thesis: verum
end;
definition
let V be non empty ZeroStr ;
redefine attr V is trivial means :Def18: :: STRUCT_0:def 18
for u being Element of V holds u = 0. V;
compatibility
( V is trivial iff for u being Element of V holds u = 0. V )
proof
thus ( V is trivial implies for a being Element of V holds a = 0. V ) by Def10; ::_thesis: ( ( for u being Element of V holds u = 0. V ) implies V is trivial )
assume A1: for a being Element of V holds a = 0. V ; ::_thesis: V is trivial
let a, b be Element of V; :: according to STRUCT_0:def_10 ::_thesis: a = b
thus a = 0. V by A1
.= b by A1 ; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines trivial STRUCT_0:def_18_:_
for V being non empty ZeroStr holds
( V is trivial iff for u being Element of V holds u = 0. V );
registration
let V be non trivial ZeroStr ;
cluster NonZero V -> non empty ;
coherence
not NonZero V is empty
proof
ex u being Element of V st u <> 0. V by Def18;
hence not NonZero V is empty by ZFMISC_1:56; ::_thesis: verum
end;
end;
registration
cluster non empty trivial for ZeroStr ;
existence
ex b1 being ZeroStr st
( b1 is trivial & not b1 is empty )
proof
take ZeroStr(# 1,(In (0,1)) #) ; ::_thesis: ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty )
thus ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty ) by CARD_1:49; ::_thesis: verum
end;
end;
registration
let S be non empty trivial ZeroStr ;
cluster NonZero S -> empty ;
coherence
NonZero S is empty
proof
assume not NonZero S is empty ; ::_thesis: contradiction
then consider x being Element of S such that
A1: x in NonZero S by SUBSET_1:4;
not x in {(0. S)} by A1, XBOOLE_0:def_5;
then x <> 0. S by TARSKI:def_1;
hence contradiction by Def18; ::_thesis: verum
end;
end;
registration
let S be non empty 1-sorted ;
cluster non empty trivial for Element of bool the carrier of S;
existence
ex b1 being Subset of S st
( not b1 is empty & b1 is trivial )
proof
{ the Element of S} is Subset of S ;
hence ex b1 being Subset of S st
( not b1 is empty & b1 is trivial ) ; ::_thesis: verum
end;
end;
theorem :: STRUCT_0:2
for F being non degenerated ZeroOneStr holds 1. F in NonZero F
proof
let F be non degenerated ZeroOneStr ; ::_thesis: 1. F in NonZero F
not 1. F in {(0. F)} by TARSKI:def_1;
hence 1. F in NonZero F by XBOOLE_0:def_5; ::_thesis: verum
end;
registration
let S be finite 1-sorted ;
cluster card S -> natural ;
coherence
card S is natural ;
end;
registration
let S be non empty finite 1-sorted ;
cluster card S -> non zero for Nat;
coherence
for b1 being Nat st b1 = card S holds
not b1 is empty ;
end;
registration
let T be non trivial 1-sorted ;
cluster non trivial for Element of bool the carrier of T;
existence
not for b1 being Subset of T holds b1 is trivial
proof
consider x, y being Element of T such that
A1: x <> y by Def10;
reconsider A = {x,y} as Subset of T ;
take A ; ::_thesis: not A is trivial
take x ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st
( x in A & b1 in A & not x = b1 )
take y ; ::_thesis: ( x in A & y in A & not x = y )
thus x in A by TARSKI:def_2; ::_thesis: ( y in A & not x = y )
thus y in A by TARSKI:def_2; ::_thesis: not x = y
thus not x = y by A1; ::_thesis: verum
end;
end;
theorem :: STRUCT_0:3
for S being ZeroStr holds not 0. S in NonZero S
proof
let S be ZeroStr ; ::_thesis: not 0. S in NonZero S
assume 0. S in NonZero S ; ::_thesis: contradiction
then not 0. S in {(0. S)} by XBOOLE_0:def_5;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
theorem :: STRUCT_0:4
for S being non empty ZeroStr holds the carrier of S = {(0. S)} \/ (NonZero S) by XBOOLE_1:45;
definition
let C be set ;
let X be 1-sorted ;
attrX is C -element means :Def19: :: STRUCT_0:def 19
the carrier of X is C -element ;
end;
:: deftheorem Def19 defines -element STRUCT_0:def_19_:_
for C being set
for X being 1-sorted holds
( X is C -element iff the carrier of X is C -element );
registration
let C be Cardinal;
clusterC -element for 1-sorted ;
existence
ex b1 being 1-sorted st b1 is C -element
proof
take X = 1-sorted(# the C -element set #); ::_thesis: X is C -element
thus the carrier of X is C -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;
registration
let C be Cardinal;
let X be C -element 1-sorted ;
cluster the carrier of X -> C -element ;
coherence
the carrier of X is C -element by Def19;
end;
registration
cluster empty -> 0 -element for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is empty holds
b1 is 0 -element
proof
let S be 1-sorted ; ::_thesis: ( S is empty implies S is 0 -element )
assume S is empty ; ::_thesis: S is 0 -element
hence the carrier of S is 0 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster 0 -element -> empty for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is 0 -element holds
b1 is empty
proof
let S be 1-sorted ; ::_thesis: ( S is 0 -element implies S is empty )
assume S is 0 -element ; ::_thesis: S is empty
hence the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
cluster non empty trivial -> 1 -element for 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is empty & b1 is trivial holds
b1 is 1 -element
proof
let S be 1-sorted ; ::_thesis: ( not S is empty & S is trivial implies S is 1 -element )
assume A1: not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not S is trivial or S is 1 -element )
assume S is trivial ; ::_thesis: S is 1 -element
hence the carrier of S is 1 -element by A1; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster1 -element -> non empty trivial for 1-sorted ;
coherence
for b1 being 1-sorted st b1 is 1 -element holds
( not b1 is empty & b1 is trivial )
proof
let S be 1-sorted ; ::_thesis: ( S is 1 -element implies ( not S is empty & S is trivial ) )
assume A2: S is 1 -element ; ::_thesis: ( not S is empty & S is trivial )
hence not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is trivial
the carrier of S is trivial by A2;
hence S is trivial ; ::_thesis: verum
end;
end;
definition
let S be 2-sorted ;
attrS is feasible means :Def20: :: STRUCT_0:def 20
( the carrier of S is empty implies the carrier' of S is empty );
end;
:: deftheorem Def20 defines feasible STRUCT_0:def_20_:_
for S being 2-sorted holds
( S is feasible iff ( the carrier of S is empty implies the carrier' of S is empty ) );
registration
cluster non empty -> feasible for 2-sorted ;
coherence
for b1 being 2-sorted st not b1 is empty holds
b1 is feasible
proof
let S be 2-sorted ; ::_thesis: ( not S is empty implies S is feasible )
assume not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is feasible
hence S is feasible by Def20; ::_thesis: verum
end;
cluster void -> feasible for 2-sorted ;
coherence
for b1 being 2-sorted st b1 is void holds
b1 is feasible
proof
let S be 2-sorted ; ::_thesis: ( S is void implies S is feasible )
assume the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: S is feasible
hence S is feasible by Def20; ::_thesis: verum
end;
cluster empty feasible -> void for 2-sorted ;
coherence
for b1 being 2-sorted st b1 is empty & b1 is feasible holds
b1 is void
proof
let S be 2-sorted ; ::_thesis: ( S is empty & S is feasible implies S is void )
assume ( the carrier of S is empty & S is feasible ) ; :: according to STRUCT_0:def_1 ::_thesis: S is void
hence the carrier' of S is empty by Def20; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
cluster non void feasible -> non empty for 2-sorted ;
coherence
for b1 being 2-sorted st not b1 is void & b1 is feasible holds
not b1 is empty ;
end;
definition
let S be 2-sorted ;
attrS is trivial' means :Def21: :: STRUCT_0:def 21
the carrier' of S is trivial ;
end;
:: deftheorem Def21 defines trivial' STRUCT_0:def_21_:_
for S being 2-sorted holds
( S is trivial' iff the carrier' of S is trivial );
registration
cluster non empty trivial strict non void trivial' for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void & b1 is trivial & b1 is trivial' )
proof
take S = 2-sorted(# 1,1 #); ::_thesis: ( S is strict & not S is empty & not S is void & S is trivial & S is trivial' )
thus S is strict ; ::_thesis: ( not S is empty & not S is void & S is trivial & S is trivial' )
thus not S is empty ; ::_thesis: ( not S is void & S is trivial & S is trivial' )
thus not S is void ; ::_thesis: ( S is trivial & S is trivial' )
thus S is trivial by CARD_1:49; ::_thesis: S is trivial'
thus the carrier' of S is trivial by CARD_1:49; :: according to STRUCT_0:def_21 ::_thesis: verum
end;
end;
registration
let S be trivial' 2-sorted ;
cluster the carrier' of S -> trivial ;
coherence
the carrier' of S is trivial by Def21;
end;
registration
cluster non trivial' for 2-sorted ;
existence
not for b1 being 2-sorted holds b1 is trivial'
proof
take S = 2-sorted(# 1,{0,1} #); ::_thesis: not S is trivial'
( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def_2;
hence not S is trivial' by ZFMISC_1:def_10; ::_thesis: verum
end;
end;
registration
let S be non trivial' 2-sorted ;
cluster the carrier' of S -> non trivial ;
coherence
not the carrier' of S is trivial by Def21;
end;
registration
cluster void -> trivial' for 2-sorted ;
coherence
for b1 being 2-sorted st b1 is void holds
b1 is trivial'
proof
let S be 2-sorted ; ::_thesis: ( S is void implies S is trivial' )
assume the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: S is trivial'
hence the carrier' of S is trivial ; :: according to STRUCT_0:def_21 ::_thesis: verum
end;
cluster non trivial -> non empty for 1-sorted ;
coherence
for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty ;
end;