:: STRUCT_0 semantic presentation

definition
attr a1 is strict;
struct 1-sorted -> ;
aggr 1-sorted(# carrier #) -> 1-sorted ;
sel carrier c1 -> set ;
end;

definition
attr a1 is strict;
struct ZeroStr -> 1-sorted ;
aggr ZeroStr(# carrier, Zero #) -> ZeroStr ;
sel Zero c1 -> Element of the carrier of a1;
end;

definition
let c1 be 1-sorted ;
attr a1 is empty means :Def1: :: STRUCT_0:def 1
the carrier of a1 is empty;
end;

:: deftheorem Def1 defines empty STRUCT_0:def 1 :
for b1 being 1-sorted holds
( b1 is empty iff the carrier of b1 is empty );

registration
cluster non empty 1-sorted ;
existence
not for b1 being 1-sorted holds b1 is empty
proof end;
end;

registration
cluster non empty ZeroStr ;
existence
not for b1 being ZeroStr holds b1 is empty
proof end;
end;

registration
let c1 be non empty 1-sorted ;
cluster the carrier of a1 -> non empty ;
coherence
not the carrier of c1 is empty by Def1;
end;

definition
let c1 be 1-sorted ;
mode Element of a1 is Element of the carrier of a1;
mode Subset of a1 is Subset of the carrier of a1;
mode Subset-Family of a1 is Subset-Family of the carrier of a1;
end;

registration
let c1 be non empty 1-sorted ;
cluster non empty Element of bool the carrier of a1;
existence
not for b1 being Subset of c1 holds b1 is empty
proof end;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be Element of c1;
redefine func { as {c2} -> Subset of a1;
coherence
{c2} is Subset of c1 by SUBSET_1:55;
end;

definition
let c1 be non empty 1-sorted ;
let c2, c3 be Element of c1;
redefine func { as {c2,c3} -> Subset of a1;
coherence
{c2,c3} is Subset of c1 by SUBSET_1:56;
end;

definition
let c1 be non empty 1-sorted ;
let c2 be non empty Subset of c1;
redefine mode Element as Element of c2 -> Element of a1;
coherence
for b1 being Element of c2 holds b1 is Element of c1
proof end;
end;

definition
let c1 be 1-sorted ;
let c2 be set ;
mode Function of a1,a2 is Function of the carrier of a1,a2;
mode Function of a2,a1 is Function of a2,the carrier of a1;
end;

definition
let c1, c2 be 1-sorted ;
mode Function of a1,a2 is Function of the carrier of a1,the carrier of a2;
end;

definition
let c1 be 1-sorted ;
mode FinSequence of a1 is FinSequence of the carrier of a1;
end;