environ
vocabularies HIDDEN, MSUALG_1, SUBSET_1, STRUCT_0, NUMBERS, XBOOLE_0, CARD_3, FINSEQ_1, FUNCOP_1, FINSEQ_2, PBOOLE, FUNCT_4, RELAT_1, PARTFUN1, FUNCT_1, TARSKI, MSAFREE2, FINSET_1, GLIB_000, MARGREL1, CIRCUIT1, FSM_1, CIRCUIT2, MCART_1, NAT_1, CARD_1, LATTICES, XBOOLEAN, CIRCCOMB;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, MCART_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FINSET_1, FUNCT_2, FUNCOP_1, PARTFUN1, FUNCT_4, CARD_3, MARGREL1, PBOOLE, STRUCT_0, MSUALG_1, MSAFREE2, CIRCUIT1, CIRCUIT2;
definitions TARSKI, PARTFUN1, FINSET_1, MSAFREE2, STRUCT_0, XBOOLE_0, FUNCOP_1, PBOOLE;
theorems TARSKI, ZFMISC_1, FINSEQ_1, FINSEQ_2, MSUALG_1, FUNCT_1, FUNCT_2, FUNCT_4, PBOOLE, GRFUNC_1, FUNCOP_1, PARTFUN1, RELAT_1, MSAFREE2, CIRCUIT1, CIRCUIT2, CARD_3, MONOID_1, RELSET_1, XBOOLE_0, XBOOLE_1, CARD_1, FINSEQ_3, XTUPLE_0, XREGULAR;
schemes FUNCT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, FINSEQ_1, MARGREL1, CARD_3, PBOOLE, STRUCT_0, MSUALG_1, MSUALG_2, MSAFREE2, FUNCT_4, RELSET_1, FINSEQ_2, XTUPLE_0;
constructors HIDDEN, MARGREL1, CIRCUIT1, CIRCUIT2, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities TARSKI, MSUALG_1, MSAFREE2, FUNCOP_1, MARGREL1;
expansions TARSKI, PARTFUN1, MSUALG_1, XBOOLE_0;
definition
let f be
object ;
let p be
FinSequence;
let x be
object ;
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
object ;
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;
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 A1:
(
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;
:: 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;