environ
vocabularies HIDDEN, MSAFREE2, STRUCT_0, XBOOLE_0, MSUALG_1, RELAT_1, PBOOLE, MSAFREE, FUNCOP_1, FUNCT_1, TREES_3, FINSEQ_1, SUBSET_1, TREES_4, MSUALG_3, MARGREL1, FINSEQ_4, TARSKI, DTCONSTR, NAT_1, NUMBERS, TREES_2, CARD_3, PARTFUN1, ZFMISC_1, TDGROUP, CIRCUIT1, FSM_1, FUNCT_4, GLIB_000, UNIALG_2, MSATERM, PRELAMB, REALSET1, CARD_1, XXREAL_0, ARYTM_3, FUNCT_6, TREES_A, FINSET_1, CIRCUIT2;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, XXREAL_0, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FINSET_1, TREES_2, TREES_3, TREES_4, CARD_3, FUNCT_6, LANG1, DTCONSTR, PBOOLE, FUNCOP_1, XXREAL_2, STRUCT_0, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, MSATERM;
definitions PBOOLE;
theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, RELAT_1, GRFUNC_1, FUNCT_1, FUNCT_2, FUNCT_4, TREES_3, TREES_4, DTCONSTR, FUNCT_6, ZFMISC_1, CARD_3, MSATERM, PARTFUN2, FUNCOP_1, PBOOLE, PRALG_1, MSUALG_1, MSUALG_2, MSUALG_3, MSAFREE, PRE_CIRC, MSAFREE2, CIRCUIT1, TREES_1, EXTENS_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, XXREAL_0, PARTFUN1, XXREAL_2, CARD_1, XTUPLE_0;
schemes NAT_1, FINSEQ_1, PRE_CIRC, PBOOLE;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSET_1, XREAL_0, MEMBERED, FINSEQ_1, CARD_3, TREES_3, PRE_CIRC, STRUCT_0, MSUALG_1, MSUALG_3, MSAFREE, MSAFREE2, CIRCUIT1, XXREAL_2, CARD_1, RELSET_1, PBOOLE, NAT_1;
constructors HIDDEN, PRALG_1, MSUALG_3, MSATERM, CIRCUIT1, SEQ_4, RELSET_1, FUNCT_4;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET;
equalities MSAFREE2;
expansions PBOOLE, MSAFREE2;
Lm1:
for x being set holds not x in x
;
definition
let IIG be non
empty non
void Circuit-like monotonic ManySortedSign ;
let A be
non-empty Circuit of
IIG;
let iv be
InputValues of
A;
existence
ex b1 being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) st
for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen (v, the Sorts of A)) ) )
uniqueness
for b1, b2 being ManySortedFunction of FreeGen the Sorts of A, the Sorts of (FreeEnv A) st ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b1 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b1 . v = id (FreeGen (v, the Sorts of A)) ) ) ) & ( for v being Vertex of IIG holds
( ( v in InputVertices IIG implies b2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(iv . v),v]) ) & ( v in SortsWithConstants IIG implies b2 . v = (FreeGen (v, the Sorts of A)) --> (root-tree [(action_at v), the carrier of IIG]) ) & ( v in (InnerVertices IIG) \ (SortsWithConstants IIG) implies b2 . v = id (FreeGen (v, the Sorts of A)) ) ) ) holds
b1 = b2
end;
:: Computations
::---------------------------------------------------------------------------