:: NORMSP_0  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"N-Str":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"N-Str":::(# :::"carrier":::, :::"normF"::: #) ->    ($#l1_normsp_0 :::"N-Str"::: )  ; sel  :::"normF"::: "c1" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_normsp_0 :::"strict"::: )    for    ($#l1_normsp_0 :::"N-Str"::: )  ; 
end; definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )  ; let "x" be   ($#m1_subset_1 :::"Element":::) "of" (Set (Const "X")); func :::"||.":::"x":::".||"::: ->   ($#m1_subset_1 :::"Real":::) equals :: NORMSP_0:def 1 (Set (Set  "the"  ($#u1_normsp_0 :::"normF"::: )  "of" "X")  ($#k3_funct_2 :::"."::: )  "x"); end; 






:: deftheorem    defines :::"||."::: NORMSP_0:def 1 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )    (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X")) "holds"  (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_normsp_0 :::"normF"::: )  "of" (Set (Var "X")))  ($#k3_funct_2 :::"."::: )  (Set (Var "x")))))); 
 


definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )  ; let "f" be (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "X")))  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"Function":::); func :::"||.":::"f":::".||"::: ->   ($#m1_hidden :::"Function":::) means :: NORMSP_0:def 2 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "e")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"||."::: NORMSP_0:def 2 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )    (Bool  "for" (Set (Var "f")) "being" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b1")))  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k2_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k2_normsp_0 :::".||"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "e")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "e"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "e")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "e")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))  ")" )  ")" )  ")" )))); 
 registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )  ; let "f" be (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "X")))  ($#v5_relat_1 :::"-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set  ($#k2_normsp_0 :::"||."::: ) "f" ($#k2_normsp_0 :::".||"::: ) ) -> (Set   ($#k1_numbers :::"REAL"::: )  )  ($#v5_relat_1 :::"-valued"::: )   ; 
end; definitionlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "X"))); :: original: :::"||."::: redefine func :::"||.":::"f":::".||"::: ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ) means :: NORMSP_0:def 3 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "f")) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "C"  "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  (Set (Var "c")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))  ")" )  ")" ); end; 







:: deftheorem    defines :::"||."::: NORMSP_0:def 3 :  (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "X")))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_normsp_0 :::"||."::: ) (Set (Var "f")) ($#k3_normsp_0 :::".||"::: ) )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C"))  "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b4"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "c")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))  ")" )  ")" )  ")" ))))); 
 definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )  ; let "s" be   ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"||."::: redefine func :::"||.":::"s":::".||"::: ->   ($#m1_subset_1 :::"Real_Sequence":::) means :: NORMSP_0:def 4 (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" "s"  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) ))); end; 






:: deftheorem    defines :::"||."::: NORMSP_0:def 4 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_normsp_0 :::"N-Str"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Real_Sequence":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_normsp_0 :::"||."::: ) (Set (Var "s")) ($#k4_normsp_0 :::".||"::: ) )) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m2_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "(" (Set (Var "s"))  ($#k3_funct_2 :::"."::: )  (Set (Var "n")) ")" ) ($#k1_normsp_0 :::".||"::: ) )))  ")" )))); 
 definitionattr "c1" is  :::"strict"::: ; struct  :::"N-ZeroStr":::  ->    ($#l1_normsp_0 :::"N-Str"::: )   ","    ($#l2_struct_0 :::"ZeroStr"::: )  ; aggr :::"N-ZeroStr":::(# :::"carrier":::, :::"ZeroF":::, :::"normF"::: #) ->    ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_normsp_0 :::"strict"::: )    for    ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; 
end; 





definitionlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; attr "X" is  :::"discerning":::  means :: NORMSP_0:def 5 (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" "X"  "st" (Bool (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  "X"))); attr "X" is  :::"reflexive":::  means :: NORMSP_0:def 6 (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  "X" ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); end; 








:: deftheorem    defines :::"discerning"::: NORMSP_0:def 5 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_normsp_0 :::"N-ZeroStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v3_normsp_0 :::"discerning"::: )  ) "iff" (Bool  "for" (Set (Var "x")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "X"))  "st" (Bool (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set (Var "x")) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_struct_0 :::"0."::: )  (Set (Var "X")))))  ")" )); 
 
:: deftheorem    defines :::"reflexive"::: NORMSP_0:def 6 :  (Bool  "for" (Set (Var "X")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_normsp_0 :::"N-ZeroStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "X")) "is"   ($#v4_normsp_0 :::"reflexive"::: )  ) "iff" (Bool (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  (Set (Var "X")) ")" ) ($#k1_normsp_0 :::".||"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_normsp_0 :::"strict"::: )     ($#v3_normsp_0 :::"discerning"::: )     ($#v4_normsp_0 :::"reflexive"::: )    for    ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; 
end; registrationlet "X" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_normsp_0 :::"reflexive"::: )     ($#l2_normsp_0 :::"N-ZeroStr"::: )  ; 
cluster (Set  ($#k1_normsp_0 :::"||."::: ) (Set  "("  ($#k4_struct_0 :::"0."::: )  "X" ")" ) ($#k1_normsp_0 :::".||"::: ) ) ->   ($#v1_xboole_0 :::"zero"::: )   ; 
end;