:: PRGCOR_2  semantic presentation begin  






definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "p" be   ($#m1_hidden :::"XFinSequence":::) "of" ; let "q" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "D")); pred "p" :::"is_an_xrep_of"::: "q" means :: PRGCOR_2:def 1 (Bool  "("  (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  "D") & (Bool (Set "p"  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "q")) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  "q")  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  "p")) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "q"))) "holds"  (Bool (Set "p"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "q"  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_an_xrep_of"::: PRGCOR_2:def 1 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r1_prgcor_2 :::"is_an_xrep_of"::: )  (Set (Var "q"))) "iff" (Bool  "("  (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "D"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))) & (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q")))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))))  ")" )  ")" )  ")" )))); 
 
theorem :: PRGCOR_2:1 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "D"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Var "p"))  ($#r1_prgcor_2 :::"is_an_xrep_of"::: )  (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "p")))))) ; 
 definitionlet "x", "y", "a", "b", "c" be    ($#m1_hidden :::"set"::: )  ; func  :::"IFLGT":::  "(" "x" "," "y" "," "a" "," "b" "," "c" ")"  ->    ($#m1_hidden :::"set"::: )   equals :: PRGCOR_2:def 2 "a" if (Bool "x"  ($#r2_hidden :::"in"::: )  "y") "b" if (Bool "x"  ($#r1_hidden :::"="::: )  "y")  otherwise "c"; end; 









:: deftheorem    defines :::"IFLGT"::: PRGCOR_2:def 2 :  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) "implies" (Bool (Set   ($#k1_prgcor_2 :::"IFLGT"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "a")))  ")"  &  "("  (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y")))) "implies" (Bool (Set   ($#k1_prgcor_2 :::"IFLGT"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "b")))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "y")))) & (Bool (Bool  "not" (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) "implies" (Bool (Set   ($#k1_prgcor_2 :::"IFLGT"::: )   "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "c")))  ")"   ")" )); 
 
theorem :: PRGCOR_2:2 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "q")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Var "D"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k5_numbers :::"NAT"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Var "D"))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "q"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Var "p"))  ($#r1_prgcor_2 :::"is_an_xrep_of"::: )  (Set (Var "q")))  ")" ))))) ; 
 definitionlet "a", "b" be   ($#m1_hidden :::"XFinSequence":::) "of" ; assume that  
(Bool (Set (Set (Const "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::))
 and  
(Bool (Set (Set (Const "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Const "a"))))
 ; func  :::"inner_prd_prg":::  "(" "a" "," "b" ")"  ->   ($#m1_subset_1 :::"Real":::) means :: PRGCOR_2:def 3 (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  "a")) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" "a"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" "b"  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))))  ")"  & (Bool it  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" ))); end; 







:: deftheorem    defines :::"inner_prd_prg"::: PRGCOR_2:def 3 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a"))))) "holds"  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_prgcor_2 :::"inner_prd_prg"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"XFinSequence":::) "of" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a")))) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set  "(" (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" ) ")" ))))  ")"  & (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "n"))))  ")" )))  ")" ))); 
 
theorem :: PRGCOR_2:3 (Bool  "for" (Set (Var "a")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "s")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" )) "holds"  (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "a")) ")" ))))) ; 
 
theorem :: PRGCOR_2:4 (Bool  "for" (Set (Var "a")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  ) (Bool  "ex" (Set (Var "s")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st"  (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "a")) ")" )  ($#k2_nat_1 :::"+"::: )  (Num 1))) & (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )) & (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a"))))) "holds"  (Bool (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" ) ")" )))  ")" ) & (Bool (Set   ($#k18_rvsum_1 :::"Sum"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "s"))  ($#k1_seq_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "a")) ")" )))  ")" ))) ; 
 
theorem :: PRGCOR_2:5 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k1_numbers :::"REAL"::: )  )  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b")))) & (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::">"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "a"))))) "holds"  (Bool (Set  ($#k23_rvsum_1 :::"|("::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k23_rvsum_1 :::")|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k2_prgcor_2 :::"inner_prd_prg"::: )   "(" (Set  "("  ($#k11_afinsq_1 :::"FS2XFS*"::: )   "(" (Set (Var "a")) "," (Set (Var "n")) ")"  ")" ) "," (Set  "("  ($#k11_afinsq_1 :::"FS2XFS*"::: )   "(" (Set (Var "b")) "," (Set (Var "n")) ")"  ")" ) ")" )))) ; 
 definitionlet "b", "c" be   ($#m1_hidden :::"XFinSequence":::) "of" ; let "a" be   ($#m1_subset_1 :::"Real":::); let "m" be   ($#m1_hidden :::"Integer":::); pred "m" :::"scalar_prd_prg"::: "c" "," "a" "," "b" means :: PRGCOR_2:def 4 (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "c")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "b")  ($#r1_hidden :::"="::: )  "m") & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set "a"  ($#k8_real_1 :::"*"::: )  (Set  "(" "b"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" ); end; 







:: deftheorem    defines :::"scalar_prd_prg"::: PRGCOR_2:def 4 :  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r2_prgcor_2 :::"scalar_prd_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k8_real_1 :::"*"::: )  (Set  "(" (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" )  ")" )))); 
 
theorem :: PRGCOR_2:6 (Bool  "for" (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Real":::)  (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st" (Bool (Set (Var "m"))  ($#r2_prgcor_2 :::"scalar_prd_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool  "("   "for" (Set (Var "c")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "m"))  ($#r2_prgcor_2 :::"scalar_prd_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "a"))  ($#k10_rvsum_1 :::"*"::: )  (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "b")) ")" )))  ")" )  ")" )))) ; 
 definitionlet "b", "c" be   ($#m1_hidden :::"XFinSequence":::) "of" ; let "m" be   ($#m1_hidden :::"Integer":::); pred "m" :::"vector_minus_prg"::: "c" "," "b" means :: PRGCOR_2:def 5 (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "c")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "b")  ($#r1_hidden :::"="::: )  "m") & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" "b"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" ); end; 






:: deftheorem    defines :::"vector_minus_prg"::: PRGCOR_2:def 5 :  (Bool  "for" (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r3_prgcor_2 :::"vector_minus_prg"::: )  (Set (Var "c")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" )  ")" ))); 
 
theorem :: PRGCOR_2:7 (Bool  "for" (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st" (Bool (Set (Var "m"))  ($#r3_prgcor_2 :::"vector_minus_prg"::: )  (Set (Var "c")) "," (Set (Var "b")))) & (Bool  "("   "for" (Set (Var "c")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "m"))  ($#r3_prgcor_2 :::"vector_minus_prg"::: )  (Set (Var "c")) "," (Set (Var "b")))) "holds"  (Bool (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_rvsum_1 :::"-"::: )  (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "b")) ")" )))  ")" )  ")" ))) ; 
 definitionlet "a", "b", "c" be   ($#m1_hidden :::"XFinSequence":::) "of" ; let "m" be   ($#m1_hidden :::"Integer":::); pred "m" :::"vector_add_prg"::: "c" "," "a" "," "b" means :: PRGCOR_2:def 6 (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "c")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "a")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "b")  ($#r1_hidden :::"="::: )  "m") & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "a"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" "b"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" ); end; 







:: deftheorem    defines :::"vector_add_prg"::: PRGCOR_2:def 6 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r4_prgcor_2 :::"vector_add_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k7_real_1 :::"+"::: )  (Set  "(" (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" )  ")" ))); 
 
theorem :: PRGCOR_2:8 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st" (Bool (Set (Var "m"))  ($#r4_prgcor_2 :::"vector_add_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool  "("   "for" (Set (Var "c")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "m"))  ($#r4_prgcor_2 :::"vector_add_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "a")) ")" )  ($#k4_rvsum_1 :::"+"::: )  (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "b")) ")" )))  ")" )  ")" ))) ; 
 definitionlet "a", "b", "c" be   ($#m1_hidden :::"XFinSequence":::) "of" ; let "m" be   ($#m1_hidden :::"Integer":::); pred "m" :::"vector_sub_prg"::: "c" "," "a" "," "b" means :: PRGCOR_2:def 7 (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "c")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "a")  ($#r1_hidden :::"="::: )  "m") & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  "b")  ($#r1_hidden :::"="::: )  "m") & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set "b"  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set "c"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "a"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" "b"  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" ); end; 







:: deftheorem    defines :::"vector_sub_prg"::: PRGCOR_2:def 7 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Integer":::) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r5_prgcor_2 :::"vector_sub_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b"))) "iff" (Bool  "("  (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Integer":::) "st"  (Bool  "("  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) &  "("  (Bool (Bool (Set (Var "n"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "i"))) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set (Var "c"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" )  ($#k9_real_1 :::"-"::: )  (Set  "(" (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set (Var "i")) ")" ))))  ")"   ")" ))  ")" )  ")" ))); 
 
theorem :: PRGCOR_2:9 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   (Bool  "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_hidden :::"Nat":::)) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set   ($#k1_afinsq_1 :::"len"::: )  (Set (Var "b")))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool (Set (Set (Var "a"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))) & (Bool (Set (Set (Var "b"))  ($#k1_seq_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "m")))) "holds"  (Bool  "("  (Bool  "ex" (Set (Var "c")) "being"   ($#m1_hidden :::"XFinSequence":::) "of"  "st" (Bool (Set (Var "m"))  ($#r5_prgcor_2 :::"vector_sub_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) & (Bool  "("   "for" (Set (Var "c")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_hidden :::"XFinSequence":::) "of"   "st" (Bool (Bool (Set (Var "m"))  ($#r5_prgcor_2 :::"vector_sub_prg"::: )  (Set (Var "c")) "," (Set (Var "a")) "," (Set (Var "b")))) "holds"  (Bool (Set   ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "a")) ")" )  ($#k8_rvsum_1 :::"-"::: )  (Set  "("  ($#k12_afinsq_1 :::"XFS2FS*"::: )  (Set (Var "b")) ")" )))  ")" )  ")" ))) ;