begin
begin
begin
definition
let f be
set ;
let p be
FinSequence;
let x be
set ;
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x )
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {x} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = x & the carrier of b2 = (rng p) \/ {x} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = x holds
b1 = b2
end;
definition
let f be
set ;
let p be
FinSequence;
existence
ex b1 being non void strict ManySortedSign st
( the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] )
uniqueness
for b1, b2 being non void strict ManySortedSign st the carrier of b1 = (rng p) \/ {[p,f]} & the carrier' of b1 = {[p,f]} & the Arity of b1 . [p,f] = p & the ResultSort of b1 . [p,f] = [p,f] & the carrier of b2 = (rng p) \/ {[p,f]} & the carrier' of b2 = {[p,f]} & the Arity of b2 . [p,f] = p & the ResultSort of b2 . [p,f] = [p,f] holds
b1 = b2
end;
begin
begin
definition
let n be
Nat;
let X,
Y be non
empty set ;
let f be
Function of
(n -tuples_on X),
Y;
let p be
FinSeqLen of
n;
let x be
set ;
assume B1:
(
x in rng p implies
X = Y )
;
existence
ex b1 being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st
( the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f )
uniqueness
for b1, b2 being strict non-empty MSAlgebra over 1GateCircStr (p,f,x) st the Sorts of b1 = ((rng p) --> X) +* (x .--> Y) & the Charact of b1 . [p,f] = f & the Sorts of b2 = ((rng p) --> X) +* (x .--> Y) & the Charact of b2 . [p,f] = f holds
b1 = b2
end;
definition
let n be
Nat;
let X be non
empty set ;
let f be
Function of
(n -tuples_on X),
X;
let p be
FinSeqLen of
n;
existence
ex b1 being strict non-empty MSAlgebra over 1GateCircStr (p,f) st
( the Sorts of b1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b1 . [p,f] = f )
uniqueness
for b1, b2 being strict non-empty MSAlgebra over 1GateCircStr (p,f) st the Sorts of b1 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b1 . [p,f] = f & the Sorts of b2 = the carrier of (1GateCircStr (p,f)) --> X & the Charact of b2 . [p,f] = f holds
b1 = b2
end;
begin
:: for S1,S2 being monotonic (non void ManySortedSign) st
:: InputVertices S1 misses InnerVertices S2 or
:: InputVertices S2 misses InnerVertices S1
:: holds S1+*S2 is monotonic;