:: CIRCTRM1 semantic presentation begin theorem :: CIRCTRM1:1 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "T")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "T")) ($#r1_hidden :::"="::: ) (Set (Var "t")))) "holds" (Bool (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "t"))))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); func "X" :::"-CircuitStr"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) equals :: CIRCTRM1:def 1 (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "(" ($#k9_trees_9 :::"Subtrees"::: ) "X" ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k12_trees_9 :::"-Subtrees"::: ) "X" ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_trees_9 :::"-ImmediateSubtrees"::: ) "X" ")" ) "," (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" "S") "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k12_trees_9 :::"-Subtrees"::: ) "X" ")" ) ")" ) "#)" ); end; :: deftheorem defines :::"-CircuitStr"::: CIRCTRM1:def 1 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#g1_msualg_1 :::"ManySortedSign"::: ) "(#" (Set "(" ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k12_trees_9 :::"-Subtrees"::: ) (Set (Var "X")) ")" ) "," (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k13_trees_9 :::"-ImmediateSubtrees"::: ) (Set (Var "X")) ")" ) "," (Set "(" ($#k6_funct_3 :::"incl"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k12_trees_9 :::"-Subtrees"::: ) (Set (Var "X")) ")" ) ")" ) "#)" ))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); cluster (Set "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ($#v1_circcomb :::"unsplit"::: ) ; end; theorem :: CIRCTRM1:2 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "is" ($#v11_struct_0 :::"void"::: ) ) "iff" (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#v1_zfmisc_1 :::"root"::: ) ) & (Bool (Bool "not" (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) "," (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" )) ")" )))) ; theorem :: CIRCTRM1:3 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V"))) "iff" (Bool (Bool "not" (Set (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "is" ($#v11_struct_0 :::"void"::: ) )) ")" )))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); cluster (Set "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v1_msualg_1 :::"strict"::: ) ; end; theorem :: CIRCTRM1:4 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set (Var "v")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V"))) ")" ) & (Bool "(" "for" (Set (Var "s")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )))) "holds" (Bool (Set (Var "s")) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V"))) ")" ) ")" )))) ; theorem :: CIRCTRM1:5 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) "iff" (Bool (Set (Var "t")) "is" ($#m2_msaterm :::"CompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V"))) ")" ))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); let "g" be ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Const "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ); cluster (Set ($#k1_msualg_1 :::"the_arity_of"::: ) "g") -> ($#v6_trees_3 :::"DTree-yielding"::: ) ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); cluster -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )); end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); cluster -> ($#v3_trees_2 :::"DecoratedTree-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )); end; theorem :: CIRCTRM1:6 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool "(" (Bool (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" (Set (Var "X1")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" (Set (Var "X2")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) & (Bool (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" (Set (Var "X1")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )) ($#r1_partfun1 :::"tolerates"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" (Set (Var "X2")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) ")" )))) ; registrationlet "X", "Y" be ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_xboole_0 :::"\/"::: ) "Y") -> ($#v3_trees_3 :::"constituted-DTrees"::: ) ; end; theorem :: CIRCTRM1:7 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set "(" (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X2")) ")" )))) ; theorem :: CIRCTRM1:8 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "C")) ($#k12_trees_9 :::"-Subtrees"::: ) (Set "(" (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C")) ($#k12_trees_9 :::"-Subtrees"::: ) (Set (Var "X1")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "C")) ($#k12_trees_9 :::"-Subtrees"::: ) (Set (Var "X2")) ")" ))))) ; theorem :: CIRCTRM1:9 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_trees_3 :::"constituted-DTrees"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X1")) "holds" (Bool (Set (Var "t")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" ) & (Bool "(" "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X2")) "holds" (Bool (Set (Var "t")) "is" ($#v1_finset_1 :::"finite"::: ) ) ")" )) "holds" (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "C")) ($#k13_trees_9 :::"-ImmediateSubtrees"::: ) (Set "(" (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "C")) ($#k13_trees_9 :::"-ImmediateSubtrees"::: ) (Set (Var "X1")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "C")) ($#k13_trees_9 :::"-ImmediateSubtrees"::: ) (Set (Var "X2")) ")" ))))) ; theorem :: CIRCTRM1:10 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "X2")) ")" ) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X1")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) ($#k2_circcomb :::"+*"::: ) (Set "(" (Set (Var "X2")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )))))) ; theorem :: CIRCTRM1:11 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X")))) & (Bool "ex" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "s")) ($#k4_tarski :::"]"::: ) ))))) ")" ) ")" ))))) ; theorem :: CIRCTRM1:12 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k4_trees_4 :::"-tree"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g")) ")" ))))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Const "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ); let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func :::"the_sort_of"::: "(" "v" "," "A" ")" -> ($#m1_hidden :::"set"::: ) means :: CIRCTRM1:def 2 (Bool "for" (Set (Var "u")) "being" ($#m1_dtconstr :::"Term":::) "of" "S" "," "V" "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) "v")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "u")) ")" )))); end; :: deftheorem defines :::"the_sort_of"::: CIRCTRM1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k2_circtrm1 :::"the_sort_of"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "u")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_msaterm :::"the_sort_of"::: ) (Set (Var "u")) ")" )))) ")" ))))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "v" be ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Const "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k2_circtrm1 :::"the_sort_of"::: ) "(" "v" "," "A" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); assume (Bool (Set (Const "X")) "is" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V"))) ; let "o" be ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Const "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ); let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func :::"the_action_of"::: "(" "o" "," "A" ")" -> ($#m1_hidden :::"Function":::) means :: CIRCTRM1:def 3 (Bool "for" (Set (Var "X9")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" "S" "," "V" "st" (Bool (Bool (Set (Var "X9")) ($#r1_hidden :::"="::: ) "X")) "holds" (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X9")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "st" (Bool (Bool (Set (Var "o9")) ($#r1_hidden :::"="::: ) "o")) "holds" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "A") ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "o9")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ))))); end; :: deftheorem defines :::"the_action_of"::: CIRCTRM1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "st" (Bool (Bool (Set (Var "X")) "is" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")))) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_circtrm1 :::"the_action_of"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" )) "iff" (Bool "for" (Set (Var "X9")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "X9")) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool "for" (Set (Var "o9")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X9")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "st" (Bool (Bool (Set (Var "o9")) ($#r1_hidden :::"="::: ) (Set (Var "o")))) "holds" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "o9")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ")" ))))) ")" ))))))); scheme :: CIRCTRM1:sch 1 MSFuncEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), F3() -> bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set F2 "(" ")" ) "," (Set F3 "(" ")" ) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "holds" (Bool P1[(Set (Var "i")) "," (Set (Var "a")) "," (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))])))) provided (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F2 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set F3 "(" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "st" (Bool P1[(Set (Var "i")) "," (Set (Var "a")) "," (Set (Var "b"))])))) proof end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "A" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func "X" :::"-CircuitSorts"::: "A" -> ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )) means :: CIRCTRM1:def 4 (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k2_circtrm1 :::"the_sort_of"::: ) "(" (Set (Var "v")) "," "A" ")" ))); end; :: deftheorem defines :::"-CircuitSorts"::: CIRCTRM1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_circtrm1 :::"-CircuitSorts"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k2_circtrm1 :::"the_sort_of"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))) ")" )))))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set "X" ($#k4_circtrm1 :::"-CircuitSorts"::: ) "A") -> bbbadV2_RELAT_1() ; end; theorem :: CIRCTRM1:13 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_circtrm1 :::"-CircuitSorts"::: ) (Set (Var "A")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ))))))))) ; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func "X" :::"-CircuitCharact"::: "A" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" "X" ($#k4_circtrm1 :::"-CircuitSorts"::: ) "A" ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) "," (Set (Set "(" "X" ($#k4_circtrm1 :::"-CircuitSorts"::: ) "A" ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) means :: CIRCTRM1:def 5 (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_circtrm1 :::"the_action_of"::: ) "(" (Set (Var "g")) "," "A" ")" ))); end; :: deftheorem defines :::"-CircuitCharact"::: CIRCTRM1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "b5")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set "(" (Set "(" (Set (Var "X")) ($#k4_circtrm1 :::"-CircuitSorts"::: ) (Set (Var "A")) ")" ) ($#k6_finseq_2 :::"#"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u1_msualg_1 :::"Arity"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) "," (Set (Set "(" (Set (Var "X")) ($#k4_circtrm1 :::"-CircuitSorts"::: ) (Set (Var "A")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "the" ($#u2_msualg_1 :::"ResultSort"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ))) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k5_circtrm1 :::"-CircuitCharact"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" )))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k3_circtrm1 :::"the_action_of"::: ) "(" (Set (Var "g")) "," (Set (Var "A")) ")" ))) ")" )))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); func "X" :::"-Circuit"::: "A" -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ) equals :: CIRCTRM1:def 6 (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" "X" ($#k4_circtrm1 :::"-CircuitSorts"::: ) "A" ")" ) "," (Set "(" "X" ($#k5_circtrm1 :::"-CircuitCharact"::: ) "A" ")" ) "#)" ); end; :: deftheorem defines :::"-Circuit"::: CIRCTRM1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#g3_msualg_1 :::"MSAlgebra"::: ) "(#" (Set "(" (Set (Var "X")) ($#k4_circtrm1 :::"-CircuitSorts"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "X")) ($#k5_circtrm1 :::"-CircuitCharact"::: ) (Set (Var "A")) ")" ) "#)" )))))); theorem :: CIRCTRM1:14 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set ($#k2_circtrm1 :::"the_sort_of"::: ) "(" (Set (Var "v")) "," (Set (Var "A")) ")" ))))))) ; theorem :: CIRCTRM1:15 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "g")) "," (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_circtrm1 :::"the_action_of"::: ) "(" (Set (Var "g")) "," (Set (Var "A")) ")" ))))))) ; theorem :: CIRCTRM1:16 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set "(" (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ")" ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) ))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "g")) "," (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" )))))))) ; theorem :: CIRCTRM1:17 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) "holds" (Bool (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) "is" ($#v4_msafree2 :::"finite-yielding"::: ) ))))) ; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set "X" ($#k6_circtrm1 :::"-Circuit"::: ) "A") -> ($#v3_msualg_1 :::"strict"::: ) ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ; end; theorem :: CIRCTRM1:18 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set (Var "X1")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) ($#r2_circcomb :::"tolerates"::: ) (Set (Set (Var "X2")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")))))))) ; theorem :: CIRCTRM1:19 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "X1")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "X2")) ")" ) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "X1")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) ($#k3_circcomb :::"+*"::: ) (Set "(" (Set (Var "X2")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ))))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" be ($#m4_msaterm :::"Variables"::: ) "of" (Set (Const "A")); let "t" be ($#m1_hidden :::"DecoratedTree":::); assume (Bool (Set (Const "t")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Const "S")) "," (Set (Const "V"))) ; let "f" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Const "A"))); func "t" :::"@"::: "(" "f" "," "A" ")" -> ($#m1_hidden :::"set"::: ) means :: CIRCTRM1:def 7 (Bool "ex" (Set (Var "t9")) "being" ($#m1_dtconstr :::"c-Term":::) "of" "A" "," "V" "st" (Bool "(" (Bool (Set (Var "t9")) ($#r1_hidden :::"="::: ) "t") & (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "t9")) ($#k9_msaterm :::"@"::: ) "f")) ")" )); end; :: deftheorem defines :::"@"::: CIRCTRM1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "t")) "being" ($#m1_hidden :::"DecoratedTree":::) "st" (Bool (Bool (Set (Var "t")) "is" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) (Bool "for" (Set (Var "b6")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" )) "iff" (Bool "ex" (Set (Var "t9")) "being" ($#m1_dtconstr :::"c-Term":::) "of" (Set (Var "A")) "," (Set (Var "V")) "st" (Bool "(" (Bool (Set (Var "t9")) ($#r1_hidden :::"="::: ) (Set (Var "t"))) & (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "t9")) ($#k9_msaterm :::"@"::: ) (Set (Var "f")))) ")" )) ")" ))))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Const "S")) "," (Set (Const "V")); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "s" be ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Const "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Const "A")) ")" ); mode :::"CompatibleValuation"::: "of" "s" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "V" "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "A") means :: CIRCTRM1:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" "S" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set "V" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "st" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) "X"))) "holds" (Bool (Set (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ")" ))))); end; :: deftheorem defines :::"CompatibleValuation"::: CIRCTRM1:def 8 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "b6")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "V")) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "holds" (Bool "(" (Bool (Set (Var "b6")) "is" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set (Var "V")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "st" (Bool (Bool (Set ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_trees_4 :::"root-tree"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "v")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ")" ))))) ")" ))))))); theorem :: CIRCTRM1:20 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Var "f")) "is" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ))))))))) ; registrationlet "x" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "p" be ($#m1_trees_4 :::"FinSequence"::: ) "of" (Set (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V"))); cluster (Set "x" ($#k4_trees_4 :::"-tree"::: ) "p") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: CIRCTRM1:21 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "t"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" )) ")" )))))))) ; theorem :: CIRCTRM1:22 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool "(" "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool "(" "not" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X")))) "or" "not" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "o")) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k4_tarski :::"]"::: ) )) "or" "not" (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ")" )) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "f")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "t"))) & (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "f")) "," (Set (Var "A")) ")" )) ")" )))))))) ; begin definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "f", "g" be ($#m1_hidden :::"Function":::); pred "S1" "," "S2" :::"are_equivalent_wrt"::: "f" "," "g" means :: CIRCTRM1:def 9 (Bool "(" (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "g" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "f" "," "g" ($#r3_pua2mss1 :::"form_morphism_between"::: ) "S1" "," "S2") & (Bool (Set "f" ($#k2_funct_1 :::"""::: ) ) "," (Set "g" ($#k2_funct_1 :::"""::: ) ) ($#r3_pua2mss1 :::"form_morphism_between"::: ) "S2" "," "S1") ")" ); end; :: deftheorem defines :::"are_equivalent_wrt"::: CIRCTRM1:def 9 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) & (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "," (Set (Set (Var "g")) ($#k2_funct_1 :::"""::: ) ) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S2")) "," (Set (Var "S1"))) ")" ) ")" ))); theorem :: CIRCTRM1:23 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "(" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S1"))))) & (Bool (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relat_1 :::".:"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S1"))))) ")" ))) ; theorem :: CIRCTRM1:24 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S2")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S2")))) ")" ))) ; theorem :: CIRCTRM1:25 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool (Set (Var "S")) "," (Set (Var "S")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))))) ; theorem :: CIRCTRM1:26 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set (Var "S2")) "," (Set (Var "S1")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "," (Set (Set (Var "g")) ($#k2_funct_1 :::"""::: ) )))) ; theorem :: CIRCTRM1:27 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set (Var "f2")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f1")) "," (Set (Var "g1"))) & (Bool (Set (Var "S2")) "," (Set (Var "S3")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f2")) "," (Set (Var "g2")))) "holds" (Bool (Set (Var "S1")) "," (Set (Var "S3")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1"))) "," (Set (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1")))))) ; theorem :: CIRCTRM1:28 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")))) & (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))) ")" ))) ; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; pred "S1" "," "S2" :::"are_equivalent"::: means :: CIRCTRM1:def 10 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool "S1" "," "S2" ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))); reflexivity (Bool "for" (Set (Var "S1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "S1")) "," (Set (Var "S1")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))))) ; symmetry (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))))) "holds" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "S2")) "," (Set (Var "S1")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))))) ; end; :: deftheorem defines :::"are_equivalent"::: CIRCTRM1:def 10 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "holds" (Bool "(" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r2_circtrm1 :::"are_equivalent"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) ")" )); theorem :: CIRCTRM1:29 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) "st" (Bool (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r2_circtrm1 :::"are_equivalent"::: ) ) & (Bool (Set (Var "S2")) "," (Set (Var "S3")) ($#r2_circtrm1 :::"are_equivalent"::: ) )) "holds" (Bool (Set (Var "S1")) "," (Set (Var "S3")) ($#r2_circtrm1 :::"are_equivalent"::: ) )) ; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "f" be ($#m1_hidden :::"Function":::); pred "f" :::"preserves_inputs_of"::: "S1" "," "S2" means :: CIRCTRM1:def 11 (Bool (Set "f" ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) "S1" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) "S2")); end; :: deftheorem defines :::"preserves_inputs_of"::: CIRCTRM1:def 11 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) "iff" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "S2")))) ")" ))); theorem :: CIRCTRM1:30 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "is" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S2")))))) ; theorem :: CIRCTRM1:31 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S1")) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) "is" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "S2")))))) ; theorem :: CIRCTRM1:32 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S2")))))) ; theorem :: CIRCTRM1:33 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2")))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Var "v1")) ($#r2_hidden :::"in"::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "S1"))))) "holds" (Bool "for" (Set (Var "v2")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "v2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "v1"))))) "holds" (Bool (Set ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k4_msafree2 :::"action_at"::: ) (Set (Var "v1")) ")" ))))))) ; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "f", "g" be ($#m1_hidden :::"Function":::); let "C1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S1")); let "C2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); pred "f" "," "g" :::"form_embedding_of"::: "C1" "," "C2" means :: CIRCTRM1:def 12 (Bool "(" (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "g" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "f" "," "g" ($#r3_pua2mss1 :::"form_morphism_between"::: ) "S1" "," "S2") & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "C1") ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" "C2") ($#k3_relat_1 :::"*"::: ) "f")) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "C1") ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" "C2") ($#k3_relat_1 :::"*"::: ) "g")) ")" ); end; :: deftheorem defines :::"form_embedding_of"::: CIRCTRM1:def 12 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r3_pua2mss1 :::"form_morphism_between"::: ) (Set (Var "S1")) "," (Set (Var "S2"))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C2"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "C2"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) ")" ) ")" ))))); theorem :: CIRCTRM1:34 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S")))) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C")) "," (Set (Var "C"))))) ; theorem :: CIRCTRM1:35 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set (Var "f2")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "C3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S3")) "st" (Bool (Bool (Set (Var "f1")) "," (Set (Var "g1")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Var "f2")) "," (Set (Var "g2")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C2")) "," (Set (Var "C3")))) "holds" (Bool (Set (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1"))) "," (Set (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1"))) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C3")))))))) ; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "f", "g" be ($#m1_hidden :::"Function":::); let "C1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S1")); let "C2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); pred "C1" "," "C2" :::"are_similar_wrt"::: "f" "," "g" means :: CIRCTRM1:def 13 (Bool "(" (Bool "f" "," "g" ($#r4_circtrm1 :::"form_embedding_of"::: ) "C1" "," "C2") & (Bool (Set "f" ($#k2_funct_1 :::"""::: ) ) "," (Set "g" ($#k2_funct_1 :::"""::: ) ) ($#r4_circtrm1 :::"form_embedding_of"::: ) "C2" "," "C1") ")" ); end; :: deftheorem defines :::"are_similar_wrt"::: CIRCTRM1:def 13 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))) "iff" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "," (Set (Set (Var "g")) ($#k2_funct_1 :::"""::: ) ) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C2")) "," (Set (Var "C1"))) ")" ) ")" ))))); theorem :: CIRCTRM1:36 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))))))) ; theorem :: CIRCTRM1:37 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))) "iff" (Bool "(" (Bool (Set (Var "S1")) "," (Set (Var "S2")) ($#r1_circtrm1 :::"are_equivalent_wrt"::: ) (Set (Var "f")) "," (Set (Var "g"))) & (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "C2"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "C1"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u4_msualg_1 :::"Charact"::: ) "of" (Set (Var "C2"))) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) ")" ) ")" ))))) ; theorem :: CIRCTRM1:38 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "holds" (Bool (Set (Var "C")) "," (Set (Var "C")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S")))) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))))))) ; theorem :: CIRCTRM1:39 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set (Var "C2")) "," (Set (Var "C1")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "," (Set (Set (Var "g")) ($#k2_funct_1 :::"""::: ) )))))) ; theorem :: CIRCTRM1:40 (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set (Var "f2")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) (Bool "for" (Set (Var "C3")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S3")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f1")) "," (Set (Var "g1"))) & (Bool (Set (Var "C2")) "," (Set (Var "C3")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f2")) "," (Set (Var "g2")))) "holds" (Bool (Set (Var "C1")) "," (Set (Var "C3")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f1"))) "," (Set (Set (Var "g2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1"))))))))) ; definitionlet "S1", "S2" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "C1" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S1")); let "C2" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S2")); pred "C1" "," "C2" :::"are_similar"::: means :: CIRCTRM1:def 14 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "C1" "," "C2" ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))); end; :: deftheorem defines :::"are_similar"::: CIRCTRM1:def 14 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S2")) "holds" (Bool "(" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r6_circtrm1 :::"are_similar"::: ) ) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) ")" )))); theorem :: CIRCTRM1:41 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2")))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G2")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "G2")))) ")" ))))) ; theorem :: CIRCTRM1:42 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2")))) "holds" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o1"))))) "holds" (Bool (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o2")) "," (Set (Var "C2")) ")" ) ($#r1_funct_2 :::"="::: ) (Set ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o1")) "," (Set (Var "C1")) ")" )))))))) ; theorem :: CIRCTRM1:43 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2")))) "holds" (Bool "for" (Set (Var "o1")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "o2")) "being" ($#m1_subset_1 :::"Gate":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "o2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "o1"))))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "o2")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "o1")) ($#k3_circuit1 :::"depends_on_in"::: ) (Set (Var "s1")))))))))))) ; theorem :: CIRCTRM1:44 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "holds" (Bool (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")))))))) ; theorem :: CIRCTRM1:45 (Bool "for" (Set (Var "G2")) "," (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2")))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) "st" (Bool (Bool (Set (Var "v")) ($#r2_hidden :::"in"::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G1"))))) "holds" (Bool (Set (Var "s2")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "v")))) ")" )) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))))))) ; theorem :: CIRCTRM1:46 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))))))) ; theorem :: CIRCTRM1:47 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))))))))) ; theorem :: CIRCTRM1:48 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) & (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) )) "holds" (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) ))))))) ; theorem :: CIRCTRM1:49 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Var "C1")) "," (Set (Var "C2"))) & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "G1")) "," (Set (Var "G2")))) "holds" (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "v1"))) "iff" (Bool (Set (Var "s2")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "v1")))) ")" )))))))) ; theorem :: CIRCTRM1:50 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "holds" (Bool (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")))))))) ; theorem :: CIRCTRM1:51 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))) "iff" (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s1")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ))) ")" ))))))) ; theorem :: CIRCTRM1:52 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_msafree2 :::"InputVertices"::: ) (Set (Var "G2")))) & (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "G1")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_msafree2 :::"InnerVertices"::: ) (Set (Var "G2")))) ")" ))))) ; theorem :: CIRCTRM1:53 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Var "G1")) "," (Set (Var "G2"))))))) ; theorem :: CIRCTRM1:54 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k6_circuit2 :::"Following"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k6_circuit2 :::"Following"::: ) (Set (Var "s2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))))))) ; theorem :: CIRCTRM1:55 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s1")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s2")) "," (Set (Var "n")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))))))))) ; theorem :: CIRCTRM1:56 (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "s1")) "is" ($#v1_circuit2 :::"stable"::: ) ) "iff" (Bool (Set (Var "s2")) "is" ($#v1_circuit2 :::"stable"::: ) ) ")" ))))))) ; theorem :: CIRCTRM1:57 (Bool "for" (Set (Var "G2")) "," (Set (Var "G1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "C1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G1")) (Bool "for" (Set (Var "C2")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G2")) "st" (Bool (Bool (Set (Var "C1")) "," (Set (Var "C2")) ($#r5_circtrm1 :::"are_similar_wrt"::: ) (Set (Var "f")) "," (Set (Var "g")))) "holds" (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C2")) "st" (Bool (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "v1")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G1")) "holds" (Bool "(" (Bool (Set (Var "s1")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "v1"))) "iff" (Bool (Set (Var "s2")) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "v1")))) ")" )))))))) ; begin definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "C" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "G")); pred "C" :::"calculates"::: "X" "," "A" means :: CIRCTRM1:def 15 (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set "X" ($#k6_circtrm1 :::"-Circuit"::: ) "A") "," "C") & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "," "G") ")" )); pred "X" "," "A" :::"specifies"::: "C" means :: CIRCTRM1:def 16 (Bool "C" "," (Set "X" ($#k6_circtrm1 :::"-Circuit"::: ) "A") ($#r6_circtrm1 :::"are_similar"::: ) ); end; :: deftheorem defines :::"calculates"::: CIRCTRM1:def 15 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A"))) "iff" (Bool "ex" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) "," (Set (Var "C"))) & (Bool (Set (Var "f")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "," (Set (Var "G"))) ")" )) ")" ))))))); :: deftheorem defines :::"specifies"::: CIRCTRM1:def 16 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "X")) "," (Set (Var "A")) ($#r8_circtrm1 :::"specifies"::: ) (Set (Var "C"))) "iff" (Bool (Set (Var "C")) "," (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) ($#r6_circtrm1 :::"are_similar"::: ) ) ")" ))))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "C" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "G")); assume (Bool (Set (Const "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Const "X")) "," (Set (Const "A"))) ; mode :::"SortMap"::: "of" "X" "," "A" "," "C" -> ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) means :: CIRCTRM1:def 17 (Bool "(" (Bool it ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set "X" ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "," "G") & (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool it "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set "X" ($#k6_circtrm1 :::"-Circuit"::: ) "A") "," "C")) ")" ); end; :: deftheorem defines :::"SortMap"::: CIRCTRM1:def 17 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A")))) "holds" (Bool "for" (Set (Var "b7")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b7")) "is" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C"))) "iff" (Bool "(" (Bool (Set (Var "b7")) ($#r3_circtrm1 :::"preserves_inputs_of"::: ) (Set (Set (Var "X")) ($#k1_circtrm1 :::"-CircuitStr"::: ) ) "," (Set (Var "G"))) & (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Var "b7")) "," (Set (Var "g")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) "," (Set (Var "C")))) ")" ) ")" )))))))); definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "V" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); let "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Const "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Const "V")) ")" ); let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "C" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Const "G")); assume (Bool (Set (Const "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Const "X")) "," (Set (Const "A"))) ; let "f" be ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Const "X")) "," (Set (Const "A")) "," (Set (Const "C")); mode :::"OperMap"::: "of" "X" "," "A" "," "C" "," "f" -> ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) means :: CIRCTRM1:def 18 (Bool "f" "," it ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set "X" ($#k6_circtrm1 :::"-Circuit"::: ) "A") "," "C"); end; :: deftheorem defines :::"OperMap"::: CIRCTRM1:def 18 : (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "V")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set (Var "S")) ($#k1_msaterm :::"-Terms"::: ) (Set (Var "V")) ")" ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) (Bool "for" (Set (Var "b8")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b8")) "is" ($#m3_circtrm1 :::"OperMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "f"))) "iff" (Bool (Set (Var "f")) "," (Set (Var "b8")) ($#r4_circtrm1 :::"form_embedding_of"::: ) (Set (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A"))) "," (Set (Var "C"))) ")" ))))))))); theorem :: CIRCTRM1:58 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "A")) ($#r8_circtrm1 :::"specifies"::: ) (Set (Var "C")))) "holds" (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A"))))))))) ; theorem :: CIRCTRM1:59 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s9")) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "h")) "," (Set (Var "A")) ")" ))) ")" ) ")" )))))))))) ; theorem :: CIRCTRM1:60 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "C")) ($#r7_circtrm1 :::"calculates"::: ) (Set (Var "X")) "," (Set (Var "A")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "v"))) & (Bool "ex" (Set (Var "f")) "being" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) "st" (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s9")) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "h")) "," (Set (Var "A")) ")" ))))) ")" )))))))))) ; theorem :: CIRCTRM1:61 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "A")) ($#r8_circtrm1 :::"specifies"::: ) (Set (Var "C")))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) & (Bool "(" "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s9")) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "h")) "," (Set (Var "A")) ")" ))) ")" ) ")" )))))))))) ; theorem :: CIRCTRM1:62 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m4_msaterm :::"Variables"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "X")) "being" ($#m3_msaterm :::"SetWithCompoundTerm"::: ) "of" (Set (Var "S")) "," (Set (Var "V")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#v2_msafree2 :::"Circuit-like"::: ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"Circuit":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "X")) "," (Set (Var "A")) ($#r8_circtrm1 :::"specifies"::: ) (Set (Var "C")))) "holds" (Bool "for" (Set (Var "t")) "being" ($#m1_dtconstr :::"Term":::) "of" (Set (Var "S")) "," (Set (Var "V")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_trees_9 :::"Subtrees"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vertex":::) "of" (Set (Var "G")) "st" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ) ($#r1_facirc_1 :::"is_stable_at"::: ) (Set (Var "v"))) & (Bool "ex" (Set (Var "f")) "being" ($#m2_circtrm1 :::"SortMap"::: ) "of" (Set (Var "X")) "," (Set (Var "A")) "," (Set (Var "C")) "st" (Bool "for" (Set (Var "s9")) "being" ($#m1_subset_1 :::"State":::) "of" (Set "(" (Set (Var "X")) ($#k6_circtrm1 :::"-Circuit"::: ) (Set (Var "A")) ")" ) "st" (Bool (Bool (Set (Var "s9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "for" (Set (Var "h")) "being" ($#m1_circtrm1 :::"CompatibleValuation"::: ) "of" (Set (Var "s9")) "holds" (Bool (Set (Set "(" ($#k5_facirc_1 :::"Following"::: ) "(" (Set (Var "s")) "," (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set "(" ($#k6_trees_1 :::"height"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "t")) ")" ) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "v"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k7_circtrm1 :::"@"::: ) "(" (Set (Var "h")) "," (Set (Var "A")) ")" ))))) ")" )))))))))) ;