:: FINSEQOP semantic presentation begin theorem :: FINSEQOP:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k13_funct_3 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "f")) ($#k13_funct_3 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k13_funct_3 :::"<:"::: ) (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k13_funct_3 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FINSEQOP:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k15_funct_3 :::"[:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "f")) ($#k15_funct_3 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k15_funct_3 :::":]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FINSEQOP:3 (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FINSEQOP:4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FINSEQOP:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "x")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FINSEQOP:6 (Bool "for" (Set (Var "X")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_funct_3 :::"<:"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x2")) ")" ) ($#k14_funct_3 :::":>"::: ) ) ($#r1_funct_2 :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) )))) ; theorem :: FINSEQOP:7 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "," (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x2")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ")" ))))) ; definitionlet "D", "D9", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "E")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "p9" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D9")); :: original: :::".:"::: redefine func "F" :::".:"::: "(" "p" "," "p9" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "E"; end; definitionlet "D", "D9", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "E")); let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "d9" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D9")); :: original: :::"[:]"::: redefine func "F" :::"[:]"::: "(" "p" "," "d9" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "E"; end; definitionlet "D", "D9", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "E")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); let "p9" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D9")); :: original: :::"[;]"::: redefine func "F" :::"[;]"::: "(" "d" "," "p9" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "E"; end; definitionlet "D", "E" be ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "D")); let "h" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "E")); :: original: :::"*"::: redefine func "h" :::"*"::: "p" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" "E"; end; theorem :: FINSEQOP:8 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; theorem :: FINSEQOP:9 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "p")) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "q")) ")" )))))) ; theorem :: FINSEQOP:10 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "T9")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set "(" (Set (Var "T9")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d9")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T")) "," (Set (Var "T9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))))))) ; theorem :: FINSEQOP:11 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "T9")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) (Bool "for" (Set (Var "S")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "j")) "," (Set (Var "D")) (Bool "for" (Set (Var "S9")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "j")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "T")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "S")) ")" ) "," (Set "(" (Set (Var "T9")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "S9")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T")) "," (Set (Var "T9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "S")) "," (Set (Var "S9")) ")" ")" )))))))))) ; theorem :: FINSEQOP:12 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p9")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "p9")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d9")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQOP:13 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p9")) "," (Set (Var "q9")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "p9")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q9")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "p9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "q9")) ")" ")" ))))))) ; theorem :: FINSEQOP:14 (Bool "for" (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "d")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) "," (Set (Var "d9")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" ) ($#k12_finseq_1 :::"*>"::: ) )))))))) ; theorem :: FINSEQOP:15 (Bool "for" (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "p")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "q")) ")" ) "," (Set (Var "d9")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "p")) "," (Set (Var "d9")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "q")) "," (Set (Var "d9")) ")" ")" ))))))) ; theorem :: FINSEQOP:16 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ))))))) ; theorem :: FINSEQOP:17 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d9")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" )))))))) ; theorem :: FINSEQOP:18 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d9")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" )))))))) ; theorem :: FINSEQOP:19 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "d9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D9")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) "," (Set (Var "d9")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d9")) ")" ")" )))))))) ; theorem :: FINSEQOP:20 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T9")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) "," (Set (Var "T9")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T9")) ")" ))))))) ; theorem :: FINSEQOP:21 (Bool "for" (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k3_funcop_1 :::".:"::: ) "(" (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d")) ")" ))))))) ; theorem :: FINSEQOP:22 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T9")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T9")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k5_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D9")) ")" ) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "T9"))))))))) ; theorem :: FINSEQOP:23 (Bool "for" (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k4_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "T"))))))))) ; theorem :: FINSEQOP:24 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "f9")) ")" )))))) ; theorem :: FINSEQOP:25 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f9")) ")" ) ")" )))))) ; theorem :: FINSEQOP:26 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T1")) ")" ) "," (Set (Var "T2")) ")" ))))))) ; theorem :: FINSEQOP:27 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set "(" (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T2")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:28 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "," (Set (Var "T3")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" ) "," (Set (Var "T3")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T2")) "," (Set (Var "T3")) ")" ")" ) ")" )))))) ; theorem :: FINSEQOP:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d1")) "," (Set (Var "T")) ")" ")" ) "," (Set (Var "d2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d1")) "," (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d2")) ")" ")" ) ")" ))))))) ; theorem :: FINSEQOP:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T1")) "," (Set (Var "d")) ")" ")" ) "," (Set (Var "T2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T2")) ")" ")" ) ")" ))))))) ; theorem :: FINSEQOP:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d1")) "," (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d2")) "," (Set (Var "T")) ")" ")" ) ")" ))))))) ; theorem :: FINSEQOP:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d1")) ")" ")" ) "," (Set (Var "d2")) ")" ))))))) ; theorem :: FINSEQOP:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T2")) "," (Set (Var "T1")) ")" )))))) ; theorem :: FINSEQOP:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d")) ")" ))))))) ; theorem :: FINSEQOP:35 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "G")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d1")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d2")) "," (Set (Var "f")) ")" ")" ) ")" )))))) ; theorem :: FINSEQOP:36 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "G")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d1")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d2")) ")" ")" ) ")" )))))) ; theorem :: FINSEQOP:37 (Bool "for" (Set (Var "C")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "H")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f9")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:38 (Bool "for" (Set (Var "C")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "f")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "H")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:39 (Bool "for" (Set (Var "C")) "," (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "H")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:40 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f9")) ")" ) ")" )))))) ; theorem :: FINSEQOP:41 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "f")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:42 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "d")) ")" ")" )) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:43 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))) ")" )))) ; theorem :: FINSEQOP:44 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))) ; theorem :: FINSEQOP:45 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "f")))))) ; theorem :: FINSEQOP:46 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d1")) "," (Set (Var "T")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d2")) "," (Set (Var "T")) ")" ")" ) ")" ))))))) ; theorem :: FINSEQOP:47 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "G")))) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d1")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d2")) ")" ")" ) ")" ))))))) ; theorem :: FINSEQOP:48 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "H")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "T1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "T2")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:49 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "H")) ($#k3_finseqop :::"[;]"::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) ")" ))))))))) ; theorem :: FINSEQOP:50 (Bool "for" (Set (Var "E")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "E")) "st" (Bool (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "H")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "h")) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) "," (Set "(" (Set (Var "h")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" ))))))))) ; theorem :: FINSEQOP:51 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "T1")) ")" ) "," (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "T2")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:52 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "d")) "," (Set (Var "T")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:53 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set "(" (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set (Var "d")) ")" ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:54 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "u")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ))) "holds" (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:55 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "G")) "," (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "u")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ))) "holds" (Bool (Set (Var "u")) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:56 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "T"))) & (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T")) "," (Set "(" (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "T"))) ")" ))))) ; theorem :: FINSEQOP:57 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k3_finseqop :::"[;]"::: ) "(" (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "T"))))))) ; theorem :: FINSEQOP:58 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "F")) ($#k2_finseqop :::"[:]"::: ) "(" (Set (Var "T")) "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Var "T"))))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "u" be ($#m1_subset_1 :::"UnOp":::) "of" (Set (Const "D")); let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); pred "u" :::"is_an_inverseOp_wrt"::: "F" means :: FINSEQOP:def 1 (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "holds" (Bool "(" (Bool (Set "F" ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" "u" ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "F")) & (Bool (Set "F" ($#k5_binop_1 :::"."::: ) "(" (Set "(" "u" ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) "F")) ")" )); end; :: deftheorem defines :::"is_an_inverseOp_wrt"::: FINSEQOP:def 1 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "u")) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set (Var "F"))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) ")" )) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); attr "F" is :::"having_an_inverseOp"::: means :: FINSEQOP:def 2 (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" "D" "st" (Bool (Set (Var "u")) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) "F")); end; :: deftheorem defines :::"having_an_inverseOp"::: FINSEQOP:def 2 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) "iff" (Bool "ex" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Set (Var "u")) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set (Var "F")))) ")" ))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); assume that (Bool (Set (Const "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) and (Bool (Set (Const "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) and (Bool (Set (Const "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) ; func :::"the_inverseOp_wrt"::: "F" -> ($#m1_subset_1 :::"UnOp":::) "of" "D" means :: FINSEQOP:def 3 (Bool it ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) "F"); end; :: deftheorem defines :::"the_inverseOp_wrt"::: FINSEQOP:def 3 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")))) "iff" (Bool (Set (Var "b3")) ($#r1_finseqop :::"is_an_inverseOp_wrt"::: ) (Set (Var "F"))) ")" )))); theorem :: FINSEQOP:59 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) ")" )))) ; theorem :: FINSEQOP:60 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")))) & (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d1"))) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) ")" )))) ; theorem :: FINSEQOP:61 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))))) ; theorem :: FINSEQOP:62 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "d")))))) ; theorem :: FINSEQOP:63 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F"))) ($#r7_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))))) ; theorem :: FINSEQOP:64 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "," (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool "(" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d2")) ")" )) "or" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d")) ")" )) ")" )) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set (Var "d2")))))) ; theorem :: FINSEQOP:65 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool "(" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) "or" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d1")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d2"))) ")" )) "holds" (Bool (Set (Var "d1")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:66 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "e")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "e")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ))))) ; theorem :: FINSEQOP:67 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "u")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set (Var "d2")) ")" )) & (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) ")" ))))) ; theorem :: FINSEQOP:68 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "u")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F"))) & (Bool (Set (Var "G")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "G")) ")" ) ")" ) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "u")))))) ; theorem :: FINSEQOP:69 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "d")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:70 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "d")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:71 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ))) ")" )))) ; theorem :: FINSEQOP:72 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f9")))) & (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Var "f9"))) ")" )))) ; theorem :: FINSEQOP:73 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T")) "," (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set "(" (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T")) ")" ) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ))) ")" ))))) ; theorem :: FINSEQOP:74 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )))) "holds" (Bool "(" (Bool (Set (Var "T1")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T2")))) & (Bool (Set (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ($#k4_finseqop :::"*"::: ) (Set (Var "T1"))) ($#r2_relset_1 :::"="::: ) (Set (Var "T2"))) ")" ))))) ; theorem :: FINSEQOP:75 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "e")) "," (Set (Var "f")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "C")) ($#k8_funcop_1 :::"-->"::: ) (Set (Var "e")))))))) ; theorem :: FINSEQOP:76 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")))) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k3_finseqop :::"[;]"::: ) "(" (Set (Var "e")) "," (Set (Var "T")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "i")) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "e"))))))))) ; definitionlet "F", "f", "g" be ($#m1_hidden :::"Function":::); func "F" :::"*"::: "(" "f" "," "g" ")" -> ($#m1_hidden :::"Function":::) equals :: FINSEQOP:def 4 (Set "F" ($#k3_relat_1 :::"*"::: ) (Set ($#k15_funct_3 :::"[:"::: ) "f" "," "g" ($#k15_funct_3 :::":]"::: ) )); end; :: deftheorem defines :::"*"::: FINSEQOP:def 4 : (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set ($#k15_funct_3 :::"[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k15_funct_3 :::":]"::: ) )))); theorem :: FINSEQOP:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )))) ; theorem :: FINSEQOP:78 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")) ")" ) ")" )))) ; theorem :: FINSEQOP:79 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "C")) "," (Set (Var "C9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C9")) "," (Set (Var "D9")) "holds" (Bool (Set (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "C9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E"))))))) ; theorem :: FINSEQOP:80 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "," (Set (Var "u9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "u")) "," (Set (Var "u9")) ")" ) "is" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); let "f", "f9" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "D")); :: original: :::"*"::: redefine func "F" :::"*"::: "(" "f" "," "f9" ")" -> ($#m1_subset_1 :::"BinOp":::) "of" "D"; end; theorem :: FINSEQOP:81 (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "," (Set (Var "E")) "," (Set (Var "C")) "," (Set (Var "C9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C9")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C9")) "," (Set (Var "D9")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k6_finseqop :::"*"::: ) "(" (Set (Var "f")) "," (Set (Var "g")) ")" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "c9")) ")" ) ")" )))))))) ; theorem :: FINSEQOP:82 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d2")) ")" ) ")" )) & (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d1")) ")" ) "," (Set (Var "d2")) ")" )) ")" ))))) ; theorem :: FINSEQOP:83 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "f9")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set (Var "f9")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "F")) ($#k6_funcop_1 :::".:"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "u")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f9")) ")" ) ")" )))))) ; theorem :: FINSEQOP:84 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#m2_finseq_1 :::"Tuple":::) "of" (Set (Var "i")) "," (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" ) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k1_finseqop :::".:"::: ) "(" (Set (Var "T1")) "," (Set "(" (Set (Var "u")) ($#k4_finseqop :::"*"::: ) (Set (Var "T2")) ")" ) ")" ))))))) ; theorem :: FINSEQOP:85 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "u")) ($#r2_funct_2 :::"="::: ) (Set ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F"))))) "holds" (Bool "(" (Bool (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" )) & (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set (Var "u")) "," (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ))) ")" ))))) ; theorem :: FINSEQOP:86 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: FINSEQOP:87 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "d")))))) ; theorem :: FINSEQOP:88 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"UnOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set (Var "u")) ")" ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k3_funct_2 :::"."::: ) (Set (Var "d")))))))) ; theorem :: FINSEQOP:89 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_finseqop :::"having_an_inverseOp"::: ) ) & (Bool (Set (Var "G")) ($#r8_binop_1 :::"="::: ) (Set (Set (Var "F")) ($#k7_finseqop :::"*"::: ) "(" (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "D")) ")" ) "," (Set "(" ($#k5_finseqop :::"the_inverseOp_wrt"::: ) (Set (Var "F")) ")" ) ")" ))) "holds" (Bool "for" (Set (Var "d1")) "," (Set (Var "d2")) "," (Set (Var "d3")) "," (Set (Var "d4")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d2")) ")" ")" ) "," (Set "(" (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d3")) "," (Set (Var "d4")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d1")) "," (Set (Var "d3")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "d2")) "," (Set (Var "d4")) ")" ")" ) ")" ))))) ;