:: MIDSP_3 semantic presentation begin theorem :: MIDSP_3:1 (Bool "for" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k"))))) "holds" (Bool "ex" (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D"))(Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))) ($#r1_hidden :::"="::: ) (Set (Var "j"))) & (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Var "k"))) & (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) ")" )))))) ; theorem :: MIDSP_3:2 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool "ex" (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ))) ; theorem :: MIDSP_3:3 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "D")) "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 "D")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "q")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "c")) ($#k12_finseq_1 :::"*>"::: ) ) ")" ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "r")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "q")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1)))) "holds" (Bool "(" (Bool "(" "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "q"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) & (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "l")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "i")) ")" ))) ")" ) ")" ))))) ; theorem :: MIDSP_3:4 (Bool "for" (Set (Var "l")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) "or" (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1))) "or" (Bool (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) ")" )) ; theorem :: MIDSP_3:5 (Bool "for" (Set (Var "l")) "," (Set (Var "n")) "," (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "not" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) ")" ))) "holds" (Bool "(" (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"+*"::: redefine func "p" :::"+*"::: "(" "i" "," "d" ")" -> ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "D"); end; begin definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); attr "c2" is :::"strict"::: ; struct :::"ReperAlgebraStr"::: "over" "n" -> ($#l1_midsp_1 :::"MidStr"::: ) ; aggr :::"ReperAlgebraStr":::(# :::"carrier":::, :::"MIDPOINT":::, :::"reper"::: #) -> ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" "n"; sel :::"reper"::: "c2" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2") ")" ) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c2"); end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "m" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "A")); let "r" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Const "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "A")) ")" ) "," (Set (Const "A")); cluster (Set ($#g1_midsp_3 :::"ReperAlgebraStr"::: ) "(#" "A" "," "m" "," "r" "#)" ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) for ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" "n"; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) for ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set "n" ($#k2_nat_1 :::"+"::: ) (Num 2)); end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode Tuple of "i" "," "RAS" is ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "RAS")); end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); :: original: :::"<*"::: redefine func :::"<*":::"a":::"*>"::: -> ($#m2_finseq_2 :::"Tuple":::) "of" (Num 1) "," "RAS"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "i", "j" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "p" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set (Const "i")) "," (Set (Const "RAS")); let "q" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set (Const "j")) "," (Set (Const "RAS")); :: original: :::"^"::: redefine func "p" :::"^"::: "q" -> ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "i" ($#k2_nat_1 :::"+"::: ) "j" ")" ) "," "RAS"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); let "p" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "RAS")); func :::"*'"::: "(" "a" "," "p" ")" -> ($#m1_subset_1 :::"Point":::) "of" "RAS" equals :: MIDSP_3:def 1 (Set (Set "the" ($#u1_midsp_3 :::"reper"::: ) "of" "RAS") ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k2_midsp_3 :::"<*"::: ) "a" ($#k2_midsp_3 :::"*>"::: ) ) ($#k3_midsp_3 :::"^"::: ) "p" ")" )); end; :: deftheorem defines :::"*'"::: MIDSP_3:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_midsp_3 :::"reper"::: ) "of" (Set (Var "RAS"))) ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k2_midsp_3 :::"<*"::: ) (Set (Var "a")) ($#k2_midsp_3 :::"*>"::: ) ) ($#k3_midsp_3 :::"^"::: ) (Set (Var "p")) ")" ))))))); theorem :: MIDSP_3:6 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" ))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"Nat"::: "of" "n" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: MIDSP_3:def 2 (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) it) & (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set "n" ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ); end; :: deftheorem defines :::"Nat"::: MIDSP_3:def 2 : (Bool "for" (Set (Var "n")) "," (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n"))) "iff" (Bool "(" (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b2"))) & (Bool (Set (Var "b2")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1))) ")" ) ")" )); theorem :: MIDSP_3:7 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "i")) "is" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n"))) "iff" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) ; theorem :: MIDSP_3:8 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) "is" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")))) ; theorem :: MIDSP_3:9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" )) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "q")))))) ; theorem :: MIDSP_3:10 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "l")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "d")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Var "d")))))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Const "D"))); let "m" be ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Const "n")); :: original: :::"."::: redefine func "p" :::"."::: "m" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); attr "RAS" is :::"being_invariance"::: means :: MIDSP_3:def 3 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" "n" "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "q")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "p")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "b")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ))))); end; :: deftheorem defines :::"being_invariance"::: MIDSP_3:def 3 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "RAS")) "is" ($#v2_midsp_3 :::"being_invariance"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "q")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set "(" (Set (Var "p")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "b")) "," (Set (Var "q")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "b")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ))))) ")" ))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "p" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "RAS")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); :: original: :::"+*"::: redefine func "p" :::"+*"::: "(" "i" "," "a" ")" -> ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS"; end; definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); pred "RAS" :::"has_property_of_zero_in"::: "i" means :: MIDSP_3:def 4 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" "i" "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"has_property_of_zero_in"::: MIDSP_3:def 4 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r1_midsp_3 :::"has_property_of_zero_in"::: ) (Set (Var "i"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "a")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a"))))) ")" ))); definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); pred "RAS" :::"is_semi_additive_in"::: "i" means :: MIDSP_3:def 5 (Bool "for" (Set (Var "a")) "," (Set (Var "pii")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) "i") ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "pii")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ))))); end; :: deftheorem defines :::"is_semi_additive_in"::: MIDSP_3:def 5 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r2_midsp_3 :::"is_semi_additive_in"::: ) (Set (Var "i"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "pii")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "pii")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ))))) ")" ))); theorem :: MIDSP_3:11 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "RAS")) ($#r2_midsp_3 :::"is_semi_additive_in"::: ) (Set (Var "m")))) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "d")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool (Set (Var "q")) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "d")) ")" ))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set "(" (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "d")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "q")) ")" ")" )))))))) ; definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); pred "RAS" :::"is_additive_in"::: "i" means :: MIDSP_3:def 6 (Bool "for" (Set (Var "a")) "," (Set (Var "pii")) "," (Set (Var "p9i")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) "i") ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" "i" "," (Set "(" (Set (Var "pii")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "p9i")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" "i" "," (Set (Var "p9i")) ")" ")" ) ")" ")" ))))); end; :: deftheorem defines :::"is_additive_in"::: MIDSP_3:def 6 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r3_midsp_3 :::"is_additive_in"::: ) (Set (Var "i"))) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "pii")) "," (Set (Var "p9i")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set "(" (Set (Var "pii")) ($#k3_midsp_1 :::"@"::: ) (Set (Var "p9i")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ) ($#k3_midsp_1 :::"@"::: ) (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "p9i")) ")" ")" ) ")" ")" ))))) ")" ))); definitionlet "n", "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); pred "RAS" :::"is_alternative_in"::: "i" means :: MIDSP_3:def 7 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" (Bool "for" (Set (Var "pii")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) "i") ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set "(" "i" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "pii")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))); end; :: deftheorem defines :::"is_alternative_in"::: MIDSP_3:def 7 : (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r4_midsp_3 :::"is_alternative_in"::: ) (Set (Var "i"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "pii")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) "st" (Bool (Bool (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "pii")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "pii")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))) ")" ))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "RAS")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode Tuple of "i" "," "W" is ($#m2_finseq_2 :::"Element"::: ) "of" (Set "i" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "the" ($#u1_midsp_2 :::"algebra"::: ) "of" "W"))); end; theorem :: MIDSP_3:12 (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "v")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool "(" "for" (Set (Var "l")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "x")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "i")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "v")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "l")))) ")" ) ")" )))))) ; theorem :: MIDSP_3:13 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "l")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "l")) ($#r1_hidden :::"="::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "v")) ")" ")" ) ($#k5_midsp_3 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" ) & (Bool "(" "for" (Set (Var "l")) "," (Set (Var "i")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "l")) ($#r1_hidden :::"<>"::: ) (Set (Var "i")))) "holds" (Bool (Set (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "i")) "," (Set (Var "v")) ")" ")" ) ($#k5_midsp_3 :::"."::: ) (Set (Var "l"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "l")))) ")" ) ")" )))))) ; theorem :: MIDSP_3:14 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool "(" "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")))) ")" )) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))))) ; scheme :: MIDSP_3:sch 1 SeqLambdaD9{ F1() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ), F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "z")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set F1 "(" ")" ) ($#k2_nat_1 :::"+"::: ) (Num 1))) & (Bool "(" "for" (Set (Var "j")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "z")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "j")) ")" )) ")" ) ")" )) proof end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "RAS")); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); let "x" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "W")); func "(" "a" "," "x" ")" :::"."::: "W" -> ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "RAS" means :: MIDSP_3:def 8 (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" "n" "holds" (Bool (Set it ($#k5_midsp_3 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "(" "a" "," (Set "(" "x" ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ($#k10_midsp_2 :::"."::: ) "W"))); end; :: deftheorem defines :::"."::: MIDSP_3:def 8 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W")))) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "b6")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))))) ")" ))))))); definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "RAS")); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); let "p" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "RAS")); func "W" :::"."::: "(" "a" "," "p" ")" -> ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," "W" means :: MIDSP_3:def 9 (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" "n" "holds" (Bool (Set it ($#k5_midsp_3 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set "W" ($#k9_midsp_2 :::"."::: ) "(" "a" "," (Set "(" "p" ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ))); end; :: deftheorem defines :::"."::: MIDSP_3:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "b6")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" )) "iff" (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) "holds" (Bool (Set (Set (Var "b6")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ))) ")" ))))))); theorem :: MIDSP_3:15 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) ")" ))))))) ; theorem :: MIDSP_3:16 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x")))))))) ; theorem :: MIDSP_3:17 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set "(" (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ")" ) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "p")))))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "RAS")); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "RAS")); let "x" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "W")); func :::"Phi"::: "(" "a" "," "x" ")" -> ($#m1_subset_1 :::"Vector":::) "of" "W" equals :: MIDSP_3:def 10 (Set "W" ($#k9_midsp_2 :::"."::: ) "(" "a" "," (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" "a" "," (Set "(" "(" "a" "," "x" ")" ($#k7_midsp_3 :::"."::: ) "W" ")" ) ")" ")" ) ")" ); end; :: deftheorem defines :::"Phi"::: MIDSP_3:def 10 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set "(" "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W")) ")" ) ")" ")" ) ")" ))))))); theorem :: MIDSP_3:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool "(" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) "iff" (Bool (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) ")" )))))))) ; theorem :: MIDSP_3:19 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "holds" (Bool "(" (Bool (Set (Var "RAS")) "is" ($#v2_midsp_3 :::"being_invariance"::: ) ) "iff" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" )))) ")" )))) ; theorem :: MIDSP_3:20 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Num 1) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) ; theorem :: MIDSP_3:21 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Num 1) "is" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")))) ; begin definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); mode :::"ReperAlgebra"::: "of" "n" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set "n" ($#k2_nat_1 :::"+"::: ) (Num 2)) means :: MIDSP_3:def 11 (Bool it "is" ($#v2_midsp_3 :::"being_invariance"::: ) ); end; :: deftheorem defines :::"ReperAlgebra"::: MIDSP_3:def 11 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_midsp_1 :::"MidSp-like"::: ) ($#l1_midsp_3 :::"ReperAlgebraStr"::: ) "over" (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 2)) "holds" (Bool "(" (Bool (Set (Var "b2")) "is" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n"))) "iff" (Bool (Set (Var "b2")) "is" ($#v2_midsp_3 :::"being_invariance"::: ) ) ")" ))); theorem :: MIDSP_3:22 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "b")) "," (Set (Var "x")) ")" ))))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "RAS" be ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Const "n")); let "W" be ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Const "RAS")); let "x" be ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Const "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Const "W")); func :::"Phi"::: "x" -> ($#m1_subset_1 :::"Vector":::) "of" "W" means :: MIDSP_3:def 12 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" "RAS" "holds" (Bool it ($#r1_hidden :::"="::: ) (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," "x" ")" ))); end; :: deftheorem defines :::"Phi"::: MIDSP_3:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k10_midsp_3 :::"Phi"::: ) (Set (Var "x")))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) "holds" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k9_midsp_3 :::"Phi"::: ) "(" (Set (Var "a")) "," (Set (Var "x")) ")" ))) ")" )))))); theorem :: MIDSP_3:23 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v"))) & (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b")))))))))) ; theorem :: MIDSP_3:24 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set "(" (Set (Var "a")) "," (Set (Var "v")) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set ($#k4_midsp_3 :::"*'"::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "v")))))))))) ; theorem :: MIDSP_3:25 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "W")) ($#k9_midsp_2 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "v")))) "holds" (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "b")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "v")) ")" )))))))))) ; theorem :: MIDSP_3:26 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set "(" (Set (Var "a")) "," (Set (Var "v")) ")" ($#k10_midsp_2 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "v")) ")" ")" ) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "b")) ")" )))))))))) ; theorem :: MIDSP_3:27 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r1_midsp_3 :::"has_property_of_zero_in"::: ) (Set (Var "m"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set "(" ($#k11_midsp_2 :::"0."::: ) (Set (Var "W")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_midsp_2 :::"0."::: ) (Set (Var "W"))))) ")" ))))) ; theorem :: MIDSP_3:28 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r2_midsp_3 :::"is_semi_additive_in"::: ) (Set (Var "m"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set "(" ($#k1_midsp_2 :::"Double"::: ) (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_midsp_2 :::"Double"::: ) (Set "(" ($#k10_midsp_3 :::"Phi"::: ) (Set (Var "x")) ")" )))) ")" ))))) ; theorem :: MIDSP_3:29 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) "st" (Bool (Bool (Set (Var "RAS")) ($#r1_midsp_3 :::"has_property_of_zero_in"::: ) (Set (Var "m"))) & (Bool (Set (Var "RAS")) ($#r3_midsp_3 :::"is_additive_in"::: ) (Set (Var "m")))) "holds" (Bool (Set (Var "RAS")) ($#r2_midsp_3 :::"is_semi_additive_in"::: ) (Set (Var "m")))))) ; theorem :: MIDSP_3:30 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "st" (Bool (Bool (Set (Var "RAS")) ($#r1_midsp_3 :::"has_property_of_zero_in"::: ) (Set (Var "m")))) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r3_midsp_3 :::"is_additive_in"::: ) (Set (Var "m"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) (Bool "for" (Set (Var "v")) "being" ($#m1_subset_1 :::"Vector":::) "of" (Set (Var "W")) "holds" (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set "(" (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set (Var "v")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_midsp_3 :::"Phi"::: ) (Set (Var "x")) ")" ) ($#k1_algstr_0 :::"+"::: ) (Set "(" ($#k10_midsp_3 :::"Phi"::: ) (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set (Var "m")) "," (Set (Var "v")) ")" ")" ) ")" ))))) ")" ))))) ; theorem :: MIDSP_3:31 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "p")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set (Set (Var "W")) ($#k8_midsp_3 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ))))))))) ; theorem :: MIDSP_3:32 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "p")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "RAS")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "st" (Bool (Bool (Set "(" (Set (Var "a")) "," (Set (Var "x")) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))) & (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ")" ) ")" ($#k7_midsp_3 :::"."::: ) (Set (Var "W"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k6_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "p")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ))))))))) ; theorem :: MIDSP_3:33 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "m")) "being" ($#m1_midsp_3 :::"Nat"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "RAS")) "being" ($#m2_midsp_3 :::"ReperAlgebra"::: ) "of" (Set (Var "n")) (Bool "for" (Set (Var "W")) "being" ($#l1_midsp_2 :::"ATLAS":::) "of" (Set (Var "RAS")) "st" (Bool (Bool (Set (Var "m")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n")))) "holds" (Bool "(" (Bool (Set (Var "RAS")) ($#r4_midsp_3 :::"is_alternative_in"::: ) (Set (Var "m"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_2 :::"Tuple":::) "of" (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set (Var "W")) "holds" (Bool (Set ($#k10_midsp_3 :::"Phi"::: ) (Set "(" (Set (Var "x")) ($#k1_midsp_3 :::"+*"::: ) "(" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) "," (Set "(" (Set (Var "x")) ($#k5_midsp_3 :::"."::: ) (Set (Var "m")) ")" ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k11_midsp_2 :::"0."::: ) (Set (Var "W"))))) ")" ))))) ;