:: ALGSEQ_1  semantic presentation begin  










theorem :: ALGSEQ_1:1 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")))) "iff" (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "n")))  ")" )) ; 
 
theorem :: ALGSEQ_1:2 (Bool  "("  (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) & (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Num 2))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k2_tarski :::"}"::: ) ))  ")" ) ; 
 
theorem :: ALGSEQ_1:3 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "holds"  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k7_card_1 :::"Segm"::: )  (Set  "(" (Set (Var "n"))  ($#k1_nat_1 :::"+"::: )  (Num 1) ")" )))) ; 
 
theorem :: ALGSEQ_1:4 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m"))) "iff" (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "m"))))  ")" )) ; 
 
theorem :: ALGSEQ_1:5 (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "m"))))) "holds"  (Bool (Set (Var "n"))  ($#r1_hidden :::"="::: )  (Set (Var "m")))) ; 
 
theorem :: ALGSEQ_1:6 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool  "("  (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" ))) & (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")) ")" )))  ")" )) ; 
 
theorem :: ALGSEQ_1:7 (Bool  "for" (Set (Var "k")) "," (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool  "("  (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" ))) "or" (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "n")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "("  ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")) ")" )))  ")" )) "holds"  (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) ; 
 


definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "F" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "R")); attr "F" is  :::"finite-Support":::  means :: ALGSEQ_1:def 1 (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "n")))) "holds"  (Bool (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "R")))); end; 





:: deftheorem    defines :::"finite-Support"::: ALGSEQ_1:def 1 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "F")) "is"   ($#v1_algseq_1 :::"finite-Support"::: )  ) "iff" (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::) "st"  (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 "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))))))  ")" ))); 
 registrationlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FUNCT_2((Set   ($#k5_numbers :::"NAT"::: )  ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R"))   ($#v1_algseq_1 :::"finite-Support"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1((Set  ($#k5_numbers :::"NAT"::: ) ) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "R"))))); 
end; definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; mode AlgSequence of "R" is   ($#v1_algseq_1 :::"finite-Support"::: )    ($#m1_subset_1 :::"sequence":::) "of" "R"; end; 



definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "p" be   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Const "R")); let "k" be   ($#m1_hidden :::"Nat":::); pred "k" :::"is_at_least_length_of"::: "p" means :: ALGSEQ_1:def 2 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  "k")) "holds"  (Bool (Set "p"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "R"))); end; 






:: deftheorem    defines :::"is_at_least_length_of"::: ALGSEQ_1:def 2 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r1_algseq_1 :::"is_at_least_length_of"::: )  (Set (Var "p"))) "iff" (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))))  ")" )))); 
 definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "p" be   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Const "R")); func  :::"len"::: "p" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) means :: ALGSEQ_1:def 3 (Bool  "("  (Bool it  ($#r1_algseq_1 :::"is_at_least_length_of"::: )  "p") & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_algseq_1 :::"is_at_least_length_of"::: )  "p")) "holds"  (Bool it  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )  ")" ); end; 






:: deftheorem    defines :::"len"::: ALGSEQ_1:def 3 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b3")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))) "iff" (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_algseq_1 :::"is_at_least_length_of"::: )  (Set (Var "p"))) & (Bool  "("   "for" (Set (Var "m")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "m"))  ($#r1_algseq_1 :::"is_at_least_length_of"::: )  (Set (Var "p")))) "holds"  (Bool (Set (Var "b3"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "m")))  ")" )  ")" )  ")" )))); 
 
theorem :: ALGSEQ_1:8 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))))))) ; 
 
theorem :: ALGSEQ_1:9 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set (Var "k")))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))))  ")" )) "holds"  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Set (Var "k")))))) ; 
 
theorem :: ALGSEQ_1:10 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "k"))  ($#k1_nat_1 :::"+"::: )  (Num 1)))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R"))))))) ; 
 definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "p" be   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Const "R")); func  :::"support"::: "p" ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  ($#k5_numbers :::"NAT"::: ) ) equals :: ALGSEQ_1:def 4 (Set   ($#k7_card_1 :::"Segm"::: )  (Set  "("  ($#k1_algseq_1 :::"len"::: )  "p" ")" )); end; 






:: deftheorem    defines :::"support"::: ALGSEQ_1:def 4 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"  (Bool (Set   ($#k2_algseq_1 :::"support"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k7_card_1 :::"Segm"::: )  (Set  "("  ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")) ")" ))))); 
 
theorem :: ALGSEQ_1:11 (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "k"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))) "iff" (Bool (Set   ($#k7_card_1 :::"Segm"::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_algseq_1 :::"support"::: )  (Set (Var "p"))))  ")" )))) ; 
 scheme  :: ALGSEQ_1:sch 1 AlgSeqLambdaF{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  , F2() ->   ($#m1_hidden :::"Nat":::), F3(  ($#m1_hidden :::"Nat":::)) ->   ($#m1_subset_1 :::"Element":::) "of" (Set F1 "("  ")" ) } : 
(Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::"<="::: )  (Set F2 "("  ")" )) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set F2 "("  ")" ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set F3 "(" (Set (Var "k")) ")" ))  ")" )  ")" ))
 proof 


end; 
theorem :: ALGSEQ_1:12 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R"))  "st" (Bool (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "q")))) & (Bool  "("   "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k1_funct_1 :::"."::: )  (Set (Var "k"))))  ")" )) "holds"  (Bool (Set (Var "p"))  ($#r2_funct_2 :::"="::: )  (Set (Var "q"))))) ; 
 
theorem :: ALGSEQ_1:13 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    "st" (Bool (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "R")))  ($#r1_hidden :::"<>"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::) (Bool  "ex" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "st" (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "k")))))) ; 
 


definitionlet "R" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "R")); func :::"<%":::"x":::"%>"::: ->   ($#m1_subset_1 :::"AlgSequence":::) "of" "R" means :: ALGSEQ_1:def 5 (Bool  "("  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  it)  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  "x")  ")" ); end; 






:: deftheorem    defines :::"<%"::: ALGSEQ_1:def 5 :  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "R"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_algseq_1 :::"<%"::: ) (Set (Var "x")) ($#k3_algseq_1 :::"%>"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_xxreal_0 :::"<="::: )  (Num 1)) & (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )  ")" )))); 
 
theorem :: ALGSEQ_1:14 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_funct_2 :::"="::: )  (Set  ($#k3_algseq_1 :::"<%"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) "iff" (Bool (Set   ($#k1_algseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" ))) ; 
 
theorem :: ALGSEQ_1:15 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_funct_2 :::"="::: )  (Set  ($#k3_algseq_1 :::"<%"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) "iff" (Bool (Set   ($#k2_algseq_1 :::"support"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" ))) ; 
 
theorem :: ALGSEQ_1:16 (Bool  "for" (Set (Var "i")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )   "holds"  (Bool (Set (Set  ($#k3_algseq_1 :::"<%"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "R")))))) ; 
 
theorem :: ALGSEQ_1:17 (Bool  "for" (Set (Var "R")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_struct_0 :::"ZeroStr"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"AlgSequence":::) "of" (Set (Var "R")) "holds"   (Bool  "("  (Bool (Set (Var "p"))  ($#r2_funct_2 :::"="::: )  (Set  ($#k3_algseq_1 :::"<%"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k3_algseq_1 :::"%>"::: ) )) "iff" (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "R")) ")" ) ($#k1_tarski :::"}"::: ) ))  ")" ))) ;