:: MIDSP_2 semantic presentation begin definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"Double"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "G" equals :: MIDSP_2:def 1 (Set "x" ($#k1_algstr_0 :::"+"::: ) "x"); end; :: deftheorem defines :::"Double"::: MIDSP_2:def 1 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_algstr_0 :::"+"::: ) (Set (Var "x")))))); definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); attr "w" is :::"associating"::: means :: MIDSP_2:def 2 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "iff" (Bool (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" )) ")" )); end; :: deftheorem defines :::"associating"::: MIDSP_2:def 2 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) ) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" )) ")" )) ")" )))); theorem :: MIDSP_2:1 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))))) ; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); pred "w" :::"is_atlas_of"::: "S" "," "G" means :: MIDSP_2:def 3 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "G" (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" "st" (Bool (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" "st" (Bool (Bool (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" "holds" (Bool (Set (Set "(" "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"is_atlas_of"::: MIDSP_2:def 3 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool "(" (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G"))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" ) ")" ) ")" )))); definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "S")); let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); assume (Bool (Set (Const "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Const "S")) "," (Set (Const "G"))) ; func "(" "a" "," "x" ")" :::"."::: "w" -> ($#m1_subset_1 :::"Element"::: ) "of" "S" means :: MIDSP_2:def 4 (Bool (Set "w" ($#k2_binop_1 :::"."::: ) "(" "a" "," it ")" ) ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"."::: MIDSP_2:def 4 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k2_midsp_2 :::"."::: ) (Set (Var "w")))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b6")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))))))); theorem :: MIDSP_2:2 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G")))))))) ; theorem :: MIDSP_2:3 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G"))) & (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))))))) ; theorem :: MIDSP_2:4 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" ))))))) ; theorem :: MIDSP_2:5 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G"))) & (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "holds" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" )))))) ; theorem :: MIDSP_2:6 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))))) ; theorem :: MIDSP_2:7 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G"))) & (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))))))) ; theorem :: MIDSP_2:8 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool (Set (Set (Var "p")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "p")))))))) ; theorem :: MIDSP_2:9 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool "ex" (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "r")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Var "q")))))))) ; theorem :: MIDSP_2:10 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "z")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "z")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "y")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "t")) ")" ))))) ; theorem :: MIDSP_2:11 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k1_midsp_2 :::"Double"::: ) (Set (Var "y")) ")" ))))) ; theorem :: MIDSP_2:12 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" ($#k4_algstr_0 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x")) ")" ))))) ; theorem :: MIDSP_2:13 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" )) ")" ))))) ; theorem :: MIDSP_2:14 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b9")) "," (Set (Var "c")) "," (Set (Var "c9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" )) & (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b9")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b9")) "," (Set (Var "c9")) ")" ))) "holds" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "c9")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "b9")) ")" ")" ))))))) ; registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster (Set ($#k15_midsp_1 :::"vectgroup"::: ) "M") -> ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ; end; theorem :: MIDSP_2:15 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "a")) "is" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) "iff" (Bool (Set (Var "a")) "is" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M"))) ")" ) ")" ) & (Bool (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_1 :::"ID"::: ) (Set (Var "M")))) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_midsp_1 :::"Vector"::: ) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "y")))) "holds" (Bool (Set (Set (Var "a")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k7_midsp_1 :::"+"::: ) (Set (Var "y"))))) ")" ) ")" )) ; definitionlet "IT" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; attr "IT" is :::"midpoint_operator"::: means :: MIDSP_2:def 5 (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" "IT" "st" (Bool (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT"))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) "IT")) ")" ) ")" ); end; :: deftheorem defines :::"midpoint_operator"::: MIDSP_2:def 5 : (Bool "for" (Set (Var "IT")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v2_midsp_2 :::"midpoint_operator"::: ) ) "iff" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ")" ) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "IT")) "st" (Bool (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "IT")))) ")" ) ")" ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_2 :::"midpoint_operator"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v12_vectsp_1 :::"Fanoian"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v8_algstr_0 :::"strict"::: ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) for ($#l2_algstr_0 :::"addLoopStr"::: ) ; end; theorem :: MIDSP_2:16 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G")))))) ; theorem :: MIDSP_2:17 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v12_vectsp_1 :::"Fanoian"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "st" (Bool (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; definitionlet "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "G")); func :::"Half"::: "x" -> ($#m1_subset_1 :::"Element":::) "of" "G" means :: MIDSP_2:def 6 (Bool (Set ($#k1_midsp_2 :::"Double"::: ) it) ($#r1_hidden :::"="::: ) "x"); end; :: deftheorem defines :::"Half"::: MIDSP_2:def 6 : (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_midsp_2 :::"Half"::: ) (Set (Var "x")))) "iff" (Bool (Set ($#k1_midsp_2 :::"Double"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))); theorem :: MIDSP_2:18 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "G")) "holds" (Bool "(" (Bool (Set ($#k3_midsp_2 :::"Half"::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set (Var "G")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set (Var "G")))) & (Bool (Set ($#k3_midsp_2 :::"Half"::: ) (Set "(" (Set (Var "x")) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_midsp_2 :::"Half"::: ) (Set (Var "x")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" ($#k3_midsp_2 :::"Half"::: ) (Set (Var "y")) ")" ))) & "(" (Bool (Bool (Set ($#k3_midsp_2 :::"Half"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_midsp_2 :::"Half"::: ) (Set (Var "y"))))) "implies" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" & (Bool (Set ($#k3_midsp_2 :::"Half"::: ) (Set "(" ($#k1_midsp_2 :::"Double"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ))) ; theorem :: MIDSP_2:19 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "c")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c")) ")" ) ($#k1_midsp_1 :::"@"::: ) (Set "(" (Set (Var "b")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "d")) ")" ))))))) ; theorem :: MIDSP_2:20 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool (Set (Var "M")) "is" ($#l1_midsp_1 :::"MidSp":::))))) ; registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster (Set ($#k15_midsp_1 :::"vectgroup"::: ) "M") -> ($#v2_midsp_2 :::"midpoint_operator"::: ) ; end; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "p", "q" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); func :::"vector"::: "(" "p" "," "q" ")" -> ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) "M" ")" ) equals :: MIDSP_2:def 7 (Set ($#k8_midsp_1 :::"vect"::: ) "(" "p" "," "q" ")" ); end; :: deftheorem defines :::"vector"::: MIDSP_2:def 7 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k4_midsp_2 :::"vector"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" )))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); func :::"vect"::: "M" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) "M" ")" )) means :: MIDSP_2:def 8 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" "M" "holds" (Bool (Set it ($#k2_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))); end; :: deftheorem defines :::"vect"::: MIDSP_2:def 8 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_midsp_2 :::"vect"::: ) (Set (Var "M")))) "iff" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "b2")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ))) ")" ))); theorem :: MIDSP_2:21 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) "holds" (Bool (Set ($#k5_midsp_2 :::"vect"::: ) (Set (Var "M"))) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set ($#k15_midsp_1 :::"vectgroup"::: ) (Set (Var "M"))))) ; theorem :: MIDSP_2:22 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "p")) "," (Set (Var "q")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" )) "iff" (Bool (Set (Set (Var "p")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "r")))) ")" ))) ; theorem :: MIDSP_2:23 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "r"))) "iff" (Bool (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k8_midsp_1 :::"vect"::: ) "(" (Set (Var "r")) "," (Set (Var "q")) ")" )) ")" ))) ; theorem :: MIDSP_2:24 canceled; registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster (Set ($#k5_midsp_2 :::"vect"::: ) "M") -> ($#v1_midsp_2 :::"associating"::: ) ; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); assume (Bool (Set (Const "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Const "S")) "," (Set (Const "G"))) ; func :::"@"::: "w" -> ($#m1_subset_1 :::"BinOp":::) "of" "S" means :: MIDSP_2:def 9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "S" "holds" (Bool (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set "w" ($#k2_binop_1 :::"."::: ) "(" (Set "(" it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "b")) ")" ))); end; :: deftheorem defines :::"@"::: MIDSP_2:def 9 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k6_midsp_2 :::"@"::: ) (Set (Var "w")))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "b4")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "b")) ")" ))) ")" ))))); theorem :: MIDSP_2:25 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_midsp_2 :::"@"::: ) (Set (Var "w")) ")" ) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "c"))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" )) ")" ))))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "D")); cluster (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" "D" "," "M" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); func :::"Atlas"::: "w" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" "S" "," (Set "(" ($#k6_midsp_2 :::"@"::: ) "w" ")" ) "#)" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" "S" "," (Set "(" ($#k6_midsp_2 :::"@"::: ) "w" ")" ) "#)" )) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "G") equals :: MIDSP_2:def 10 "w"; end; :: deftheorem defines :::"Atlas"::: MIDSP_2:def 10 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "holds" (Bool (Set ($#k7_midsp_2 :::"Atlas"::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set (Var "w")))))); theorem :: MIDSP_2:26 (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k7_midsp_2 :::"Atlas"::: ) (Set (Var "w"))) "is" ($#v1_midsp_2 :::"associating"::: ) )))) ; definitionlet "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "G" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; let "w" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "G"))); assume (Bool (Set (Const "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Const "S")) "," (Set (Const "G"))) ; func :::"MidSp."::: "w" -> ($#v1_midsp_1 :::"strict"::: ) ($#l1_midsp_1 :::"MidSp":::) equals :: MIDSP_2:def 11 (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" "S" "," (Set "(" ($#k6_midsp_2 :::"@"::: ) "w" ")" ) "#)" ); end; :: deftheorem defines :::"MidSp."::: MIDSP_2:def 11 : (Bool "for" (Set (Var "S")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "S")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set (Var "S")) "," (Set (Var "G")))) "holds" (Bool (Set ($#k8_midsp_2 :::"MidSp."::: ) (Set (Var "w"))) ($#r1_hidden :::"="::: ) (Set ($#g1_midsp_1 :::"MidStr"::: ) "(#" (Set (Var "S")) "," (Set "(" ($#k6_midsp_2 :::"@"::: ) (Set (Var "w")) ")" ) "#)" ))))); theorem :: MIDSP_2:27 (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) "holds" (Bool "(" (Bool (Set (Var "M")) "is" ($#l1_midsp_1 :::"MidSp":::)) "iff" (Bool "ex" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "ex" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) "st" (Bool "(" (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) ) ")" ))) ")" )) ; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; attr "c2" is :::"strict"::: ; struct :::"AtlasStr"::: "over" "M" -> ; aggr :::"AtlasStr":::(# :::"algebra":::, :::"function"::: #) -> ($#l1_midsp_2 :::"AtlasStr"::: ) "over" "M"; sel :::"algebra"::: "c2" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l2_algstr_0 :::"addLoopStr"::: ) ; sel :::"function"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "c2")); end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; let "IT" be ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Const "M")); attr "IT" is :::"ATLAS-like"::: means :: MIDSP_2:def 12 (Bool "(" (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT") "is" ($#v2_midsp_2 :::"midpoint_operator"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT") "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT") "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT") "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT") "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" "IT") "is" ($#v1_midsp_2 :::"associating"::: ) ) & (Bool (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" "IT") ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "M") "," (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "IT")) ")" ); end; :: deftheorem defines :::"ATLAS-like"::: MIDSP_2:def 12 : (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "IT")) "being" ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Var "IT")) "is" ($#v4_midsp_2 :::"ATLAS-like"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT"))) "is" ($#v2_midsp_2 :::"midpoint_operator"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT"))) "is" ($#v3_rlvect_1 :::"add-associative"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT"))) "is" ($#v4_rlvect_1 :::"right_zeroed"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT"))) "is" ($#v13_algstr_0 :::"right_complementable"::: ) ) & (Bool (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT"))) "is" ($#v2_rlvect_1 :::"Abelian"::: ) ) & (Bool (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" (Set (Var "IT"))) "is" ($#v1_midsp_2 :::"associating"::: ) ) & (Bool (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" (Set (Var "IT"))) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "IT")))) ")" ) ")" ))); registrationlet "M" be ($#l1_midsp_1 :::"MidSp":::); cluster ($#v4_midsp_2 :::"ATLAS-like"::: ) for ($#l1_midsp_2 :::"AtlasStr"::: ) "over" "M"; end; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); mode ATLAS of "M" is ($#v4_midsp_2 :::"ATLAS-like"::: ) ($#l1_midsp_2 :::"AtlasStr"::: ) "over" "M"; end; definitionlet "M" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) ; let "W" be ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Const "M")); mode Vector of "W" is ($#m1_subset_1 :::"Element":::) "of" (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "W"); end; definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "W" be ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Const "M")); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); func "W" :::"."::: "(" "a" "," "b" ")" -> ($#m1_subset_1 :::"Element":::) "of" (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "W") equals :: MIDSP_2:def 13 (Set (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" "W") ($#k2_binop_1 :::"."::: ) "(" "a" "," "b" ")" ); end; :: deftheorem defines :::"."::: MIDSP_2:def 13 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Var "M")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" (Set (Var "W"))) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ))))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "W" be ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Const "M")); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "M")); let "x" be ($#m1_subset_1 :::"Vector":::) "of" (Set (Const "W")); func "(" "a" "," "x" ")" :::"."::: "W" -> ($#m1_subset_1 :::"Point":::) "of" "M" equals :: MIDSP_2:def 14 (Set "(" "a" "," "x" ")" ($#k2_midsp_2 :::"."::: ) (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" "W")); end; :: deftheorem defines :::"."::: MIDSP_2:def 14 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"AtlasStr"::: ) "over" (Set (Var "M")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k2_midsp_2 :::"."::: ) (Set "the" ($#u2_midsp_2 :::"function"::: ) "of" (Set (Var "W"))))))))); definitionlet "M" be ($#l1_midsp_1 :::"MidSp":::); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "M")); func :::"0."::: "W" -> ($#m1_subset_1 :::"Vector":::) "of" "W" equals :: MIDSP_2:def 15 (Set ($#k4_struct_0 :::"0."::: ) (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "W")); end; :: deftheorem defines :::"0."::: MIDSP_2:def 15 : (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) "holds" (Bool (Set ($#k11_midsp_2 :::"0."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" (Set (Var "W"))))))); theorem :: MIDSP_2:28 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "b2")))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b1")) ")" ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b2")) ")" ")" ))) ")" ))))) ; theorem :: MIDSP_2:29 (Bool "for" (Set (Var "G")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v13_algstr_0 :::"right_complementable"::: ) ($#v2_rlvect_1 :::"Abelian"::: ) ($#v3_rlvect_1 :::"add-associative"::: ) ($#v4_rlvect_1 :::"right_zeroed"::: ) ($#v2_midsp_2 :::"midpoint_operator"::: ) ($#l2_algstr_0 :::"addLoopStr"::: ) (Bool "for" (Set (Var "M")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_midsp_1 :::"MidStr"::: ) (Bool "for" (Set (Var "w")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "G"))) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Var "w")) ($#r1_midsp_2 :::"is_atlas_of"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "M"))) "," (Set (Var "G"))) & (Bool (Set (Var "w")) "is" ($#v1_midsp_2 :::"associating"::: ) )) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k1_midsp_1 :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" (Set (Var "w")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" ))))) ; theorem :: MIDSP_2:30 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b2")))) "iff" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b1")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b2")) ")" ")" ))) ")" )))) ; theorem :: MIDSP_2:31 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a")) "," (Set (Var "c")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ))) ")" )))) ; theorem :: MIDSP_2:32 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "ex" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ))) "holds" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" ) & (Bool "(" "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" )) ")" ) ")" ))) ; theorem :: MIDSP_2:33 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_midsp_2 :::"0."::: ) (Set (Var "W")))) & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k11_midsp_2 :::"0."::: ) (Set (Var "W"))))) "implies" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_algstr_0 :::"-"::: ) (Set "(" (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ")" ))) & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ))) "implies" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "d")) "," (Set (Var "c")) ")" )) ")" & (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "ex" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "st" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ")" ) & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "b")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "a")) ")" ))) "implies" (Bool (Set (Var "b")) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "c")))) "implies" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ))) "implies" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" & "(" (Bool (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d"))))) "implies" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" )) ")" & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "b")) ")" ))) "implies" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d")))) ")" & "(" (Bool (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "implies" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) ")" & "(" (Bool (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "implies" (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" ")" ))))) ; theorem :: MIDSP_2:34 (Bool "for" (Set (Var "M")) "being" ($#l1_midsp_1 :::"MidSp":::) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "M")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "M")) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set "(" ($#k11_midsp_2 :::"0."::: ) (Set (Var "W")) ")" ) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ;