:: ALGSPEC1  semantic presentation begin  
theorem :: ALGSPEC1:1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "h"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "h"))))) ; 
 
theorem :: ALGSPEC1:2 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g"))) & (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "h")) ")" )  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "h"))))) ; 
 
theorem :: ALGSPEC1:3 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "h")))) & (Bool (Set (Set (Var "g"))  ($#k7_relat_1 :::".:"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "h")) ")" ))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "h")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g"))))) ; 
 
theorem :: ALGSPEC1:4 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "f2"))) & (Bool (Set (Var "g1"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "g2")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g1")))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Set (Var "f2"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g2"))))) ; 
 
theorem :: ALGSPEC1:5 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "X2"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y1")) "," (Set (Var "Y2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_relset_1 :::"c="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k12_lang1 :::"*"::: )  )  ($#r1_relset_1 :::"c="::: )  (Set (Set (Var "g"))  ($#k12_lang1 :::"*"::: )  ))))) ; 
 
theorem :: ALGSPEC1:6 (Bool  "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X1")) "," (Set (Var "X2"))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y1")) "," (Set (Var "Y2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k12_lang1 :::"*"::: )  )  ($#r1_partfun1 :::"tolerates"::: )  (Set (Set (Var "g"))  ($#k12_lang1 :::"*"::: )  ))))) ; 
 definitionlet "X" be    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_hidden :::"Function":::); func "X" :::"-indexing"::: "f" ->   ($#m1_hidden :::"ManySortedSet":::) "of" "X" equals :: ALGSPEC1:def 1 (Set (Set  "("  ($#k6_partfun1 :::"id"::: )  "X" ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" "f"  ($#k5_relat_1 :::"|"::: )  "X" ")" )); end; 






:: deftheorem    defines :::"-indexing"::: ALGSPEC1:def 1 :  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))))); 
 
theorem :: ALGSPEC1:7 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" ) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "f"))  ($#k7_relat_1 :::".:"::: )  (Set (Var "X")) ")" ))))) ; 
 
theorem :: ALGSPEC1:8 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "X")) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))))) ; 
 
theorem :: ALGSPEC1:9 (Bool  "for" (Set (Var "X")) "," (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "holds"  (Bool  "("   "("  (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "implies" (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x"))))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))))) "implies" (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")"   ")" ))) ; 
 
theorem :: ALGSPEC1:10 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: ALGSPEC1:11 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))))) ; 
 
theorem :: ALGSPEC1:12 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" ))  ($#r6_pboole :::"="::: )  (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))))) ; 
 
theorem :: ALGSPEC1:13 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r6_pboole :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X")))))) ; 
 
theorem :: ALGSPEC1:14 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set  ($#k1_xboole_0 :::"{}"::: ) ))  ($#r6_pboole :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set (Var "X"))))) ; 
 
theorem :: ALGSPEC1:15 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))))) ; 
 
theorem :: ALGSPEC1:16 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  ($#k1_xboole_0 :::"{}"::: ) )  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: ALGSPEC1:17 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "(" (Set (Var "Y"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))))) ; 
 
theorem :: ALGSPEC1:18 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r6_pboole :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set  "(" (Set (Var "Y"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: ALGSPEC1:19 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Set (Var "Y"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))))) ; 
 
theorem :: ALGSPEC1:20 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "(" (Set (Var "Y"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: ALGSPEC1:21 (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set (Var "X")))) "holds"  (Bool (Set (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set (Var "X")) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "g")))))) ; 
 
theorem :: ALGSPEC1:22 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set  "(" (Set (Var "X"))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))))) ; 
 definitionlet "f" be   ($#m1_hidden :::"Function":::); mode  :::"rng-retract":::  "of" "f" ->   ($#m1_hidden :::"Function":::) means :: ALGSPEC1:def 2 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "f")) & (Bool (Set "f"  ($#k3_relat_1 :::"*"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  "f" ")" )))  ")" ); end; 





:: deftheorem    defines :::"rng-retract"::: ALGSPEC1:def 2 :  (Bool  "for" (Set (Var "f")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )); 
 
theorem :: ALGSPEC1:23 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "g")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f")) "holds"  (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))))) ; 
 
theorem :: ALGSPEC1:24 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "g")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "x")))  ")" )))) ; 
 
theorem :: ALGSPEC1:25 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ) "is"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f")))) ; 
 
theorem :: ALGSPEC1:26 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool  "for" (Set (Var "g")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f")) "holds"  (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )))) ; 
 
theorem :: ALGSPEC1:27 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "f2")))) "holds"  (Bool  "for" (Set (Var "g1")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f1"))  (Bool  "for" (Set (Var "g2")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f2")) "holds"  (Bool (Set (Set (Var "g1"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g2"))) "is"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Set (Var "f1"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f2"))))))) ; 
 
theorem :: ALGSPEC1:28 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_tarski :::"c="::: )  (Set (Var "f2")))) "holds"  (Bool  "for" (Set (Var "g1")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f1")) (Bool  "ex" (Set (Var "g2")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Var "f2")) "st" (Bool (Set (Var "g1"))  ($#r1_tarski :::"c="::: )  (Set (Var "g2")))))) ; 
 begin  definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "f", "g" be   ($#m1_hidden :::"Function":::); pred "f" "," "g" :::"form_a_replacement_in"::: "S" means :: ALGSPEC1:def 3 (Bool  "for" (Set (Var "o1")) "," (Set (Var "o2")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S"  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "g" ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "g" ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "f" ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "f" ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o2")) ")" ))) & (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "f" ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") ")" )  ($#k1_funct_4 :::"+*"::: )  "f" ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o2")) ")" )))  ")" )); end; 






:: deftheorem    defines :::"form_a_replacement_in"::: ALGSPEC1:def 3 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))) "iff" (Bool  "for" (Set (Var "o1")) "," (Set (Var "o2")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o2")) ")" ))) & (Bool (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o2")) ")" )))  ")" ))  ")" ))); 
 
theorem :: ALGSPEC1:29 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))) "iff" (Bool  "for" (Set (Var "o1")) "," (Set (Var "o2")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o1")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o2"))))) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o2")) ")" ))) & (Bool (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o2")) ")" )))  ")" ))  ")" ))) ; 
 
theorem :: ALGSPEC1:30 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))) "iff" (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f"))) "," (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))  ")" ))) ; 
 








theorem :: ALGSPEC1:31 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Var "S9")))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))))) ; 
 
theorem :: ALGSPEC1:32 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Var "f")) "," (Set   ($#k1_xboole_0 :::"{}"::: )  )  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))))) ; 
 
theorem :: ALGSPEC1:33 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))))) ; 
 
theorem :: ALGSPEC1:34 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")))  ($#r1_xboole_0 :::"misses"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))))) ; 
 registrationlet "X" be    ($#m1_hidden :::"set"::: )  ; let "Y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "a" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set  "(" (Set (Const "X"))  ($#k3_finseq_2 :::"*"::: )  ")" ); let "r" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "Y")) "," (Set (Const "X")); 
cluster (Set   ($#g1_msualg_1 :::"ManySortedSign"::: )  "(#"  "X" "," "Y" "," "a" "," "r" "#)" ) ->  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )  ; 
end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "f", "g" be   ($#m1_hidden :::"Function":::); assume 
(Bool (Set (Const "f")) "," (Set (Const "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Const "S")))
 ; func "S" :::"with-replacement":::  "(" "f" "," "g" ")"  ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )   means :: ALGSPEC1:def 4 (Bool  "("  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#k1_algspec1 :::"-indexing"::: )  "f") "," (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S")  ($#k1_algspec1 :::"-indexing"::: )  "g")  ($#r3_pua2mss1 :::"form_morphism_between"::: )  "S" "," it) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#k1_algspec1 :::"-indexing"::: )  "f" ")" ))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S")  ($#k1_algspec1 :::"-indexing"::: )  "g" ")" )))  ")" ); end; 








:: deftheorem    defines :::"with-replacement"::: ALGSPEC1:def 4 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )) "iff" (Bool  "("  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f"))) "," (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Var "b4"))) & (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")) ")" )))  ")" )  ")" )))); 
 
theorem :: ALGSPEC1:35 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2")))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S1")) "," (Set (Var "S2")))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k12_lang1 :::"*"::: )  ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S1"))))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S2")))  ($#k3_relat_1 :::"*"::: )  (Set (Var "g"))))))) ; 
 
theorem :: ALGSPEC1:36 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))))) ; 
 
theorem :: ALGSPEC1:37 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "f9")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "(" (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "f9"))  ($#r8_pboole :::"="::: )  (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "g9")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g"))) "holds"  (Bool (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set  "(" (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f9"))  ($#k12_lang1 :::"*"::: )  ")" )  ($#k1_partfun1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "g9")))))))) ; 
 
theorem :: ALGSPEC1:38 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "g9")) "being"    ($#m1_algspec1 :::"rng-retract"::: )   "of" (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g"))) "holds"  (Bool (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set  "(" (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "g9"))))))) ; 
 
theorem :: ALGSPEC1:39 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Var "S9")))) "holds"  (Bool (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is"    ($#m1_instalg1 :::"Subsignature"::: )   "of" (Set (Var "S9"))))) ; 
 
theorem :: ALGSPEC1:40 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S"))) "iff" (Bool (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f"))) "," (Set (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))  ")" ))) ; 
 
theorem :: ALGSPEC1:41 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f"))) "," (Set (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) ")" )  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g")))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))) ; 
 
theorem :: ALGSPEC1:42 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))) & (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S")) "," (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))) ; 
 
theorem :: ALGSPEC1:43 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "f")) ")" ) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))) ; 
 
theorem :: ALGSPEC1:44 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set  "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#k1_algspec1 :::"-indexing"::: )  (Set (Var "g")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )))) ; 
 begin  definitionlet "S" be   ($#l1_msualg_1 :::"Signature":::); mode  :::"Extension":::  "of" "S" ->   ($#l1_msualg_1 :::"Signature":::) means :: ALGSPEC1:def 5 (Bool "S" "is"    ($#m1_instalg1 :::"Subsignature"::: )   "of" it); end; 





:: deftheorem    defines :::"Extension"::: ALGSPEC1:def 5 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "b2")) "being"   ($#l1_msualg_1 :::"Signature":::) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S"))) "iff" (Bool (Set (Var "S")) "is"    ($#m1_instalg1 :::"Subsignature"::: )   "of" (Set (Var "b2")))  ")" )); 
 
theorem :: ALGSPEC1:45 (Bool  "for" (Set (Var "S")) "being"   ($#l1_msualg_1 :::"Signature":::) "holds"  (Bool (Set (Var "S")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S")))) ; 
 
theorem :: ALGSPEC1:46 (Bool  "for" (Set (Var "S1")) "being"   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "S2")) "being"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S1"))  (Bool  "for" (Set (Var "S3")) "being"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S2")) "holds"  (Bool (Set (Var "S3")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S1")))))) ; 
 
theorem :: ALGSPEC1:47 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::)  "st" (Bool (Bool (Set (Var "S1"))  ($#r1_circcomb :::"tolerates"::: )  (Set (Var "S2")))) "holds"  (Bool (Set (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2"))) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S1")))) ; 
 
theorem :: ALGSPEC1:48 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::) "holds"  (Bool (Set (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2"))) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S2")))) ; 
 
theorem :: ALGSPEC1:49 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "g1")) "," (Set (Var "f2")) "," (Set (Var "g2")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f1"))  ($#r1_partfun1 :::"tolerates"::: )  (Set (Var "f2"))) & (Bool (Set (Var "f1")) "," (Set (Var "g1"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S1")) "," (Set (Var "S"))) & (Bool (Set (Var "f2")) "," (Set (Var "g2"))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Var "S2")) "," (Set (Var "S")))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "f2"))) "," (Set (Set (Var "g1"))  ($#k1_funct_4 :::"+*"::: )  (Set (Var "g2")))  ($#r3_pua2mss1 :::"form_morphism_between"::: )  (Set (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2"))) "," (Set (Var "S"))))) ; 
 
theorem :: ALGSPEC1:50 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "," (Set (Var "E")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::) "holds"   (Bool  "("  (Bool (Set (Var "E")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S1"))) & (Bool (Set (Var "E")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S2"))) "iff" (Bool  "("  (Bool (Set (Var "S1"))  ($#r1_circcomb :::"tolerates"::: )  (Set (Var "S2"))) & (Bool (Set (Var "E")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2"))))  ")" )  ")" )) ; 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::); 
cluster   ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#m2_algspec1 :::"Extension"::: )   "of" "S"; 
end; registrationlet "S" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::); 
cluster   ->  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   for    ($#m2_algspec1 :::"Extension"::: )   "of" "S"; 
end; 
theorem :: ALGSPEC1:51 (Bool  "for" (Set (Var "S")) "," (Set (Var "T")) "being"   ($#l1_msualg_1 :::"Signature":::)  "st" (Bool (Bool (Set (Var "S")) "is"   ($#v2_struct_0 :::"empty"::: )  )) "holds"  (Bool (Set (Var "T")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S")))) ; 
 registrationlet "S" be   ($#l1_msualg_1 :::"Signature":::); 
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#v1_instalg1 :::"feasible"::: )    for    ($#m2_algspec1 :::"Extension"::: )   "of" "S"; 
end; 
theorem :: ALGSPEC1:52 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "E")))) "holds"  (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "S")))))) ; 
 
theorem :: ALGSPEC1:53 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Var "E")))) "holds"  (Bool (Set (Set (Var "E"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" ) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Set (Var "S"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" ))))) ; 
 
theorem :: ALGSPEC1:54 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  "st" (Bool (Bool (Set (Var "S1"))  ($#r1_circcomb :::"tolerates"::: )  (Set (Var "S2")))) "holds"  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g"))  ($#r1_algspec1 :::"form_a_replacement_in"::: )  (Set (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2"))))) "holds"  (Bool (Set (Set  "(" (Set (Var "S1"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S2")) ")" )  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "S1"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" )  ($#k2_circcomb :::"+*"::: )  (Set  "(" (Set (Var "S2"))  ($#k2_algspec1 :::"with-replacement"::: )   "(" (Set (Var "f")) "," (Set (Var "g")) ")"  ")" ))))) ; 
 begin  definitionmode  :::"Algebra":::  ->    ($#m1_hidden :::"set"::: )   means :: ALGSPEC1:def 6 (Bool  "ex" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::) "st" (Bool it "is"   ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")))); end; 




:: deftheorem    defines :::"Algebra"::: ALGSPEC1:def 6 :  (Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b1")) "is"    ($#m3_algspec1 :::"Algebra"::: )  ) "iff" (Bool  "ex" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::) "st" (Bool (Set (Var "b1")) "is"   ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))))  ")" )); 
 definitionlet "S" be   ($#l1_msualg_1 :::"Signature":::); mode  :::"Algebra":::  "of" "S" ->    ($#m3_algspec1 :::"Algebra"::: )   means :: ALGSPEC1:def 7 (Bool  "ex" (Set (Var "E")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#m2_algspec1 :::"Extension"::: )   "of" "S" "st" (Bool it "is"   ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "E")))); end; 





:: deftheorem    defines :::"Algebra"::: ALGSPEC1:def 7 :  (Bool  "for" (Set (Var "S")) "being"   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m3_algspec1 :::"Algebra"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S"))) "iff" (Bool  "ex" (Set (Var "E")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S")) "st" (Bool (Set (Var "b2")) "is"   ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "E"))))  ")" ))); 
 
theorem :: ALGSPEC1:55 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_msualg_6 :::"feasible"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set (Var "A")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S"))))) ; 
 
theorem :: ALGSPEC1:56 (Bool  "for" (Set (Var "S")) "being"   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S"))  (Bool  "for" (Set (Var "A")) "being"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "E")) "holds"  (Bool (Set (Var "A")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S")))))) ; 
 
theorem :: ALGSPEC1:57 (Bool  "for" (Set (Var "S")) "being"   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "A")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S")))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "E")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "E"))))  ")" )))) ; 
 
theorem :: ALGSPEC1:58 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "E")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "E"))  "st" (Bool (Bool (Set (Var "A")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S")))) "holds"  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "A")))  ($#k1_funct_1 :::"."::: )  (Set (Var "o"))) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) ")" ) "," (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ) ")" )))))) ; 
 
theorem :: ALGSPEC1:59 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S"))  (Bool  "for" (Set (Var "E")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    "st" (Bool (Bool (Set (Var "A")) "is"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "E")))) "holds"  (Bool (Set (Var "A")) "is"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Set (Var "E"))  ($#k2_circcomb :::"+*"::: )  (Set (Var "S"))))))) ; 
 
theorem :: ALGSPEC1:60 (Bool  "for" (Set (Var "S1")) "," (Set (Var "S2")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S1"))  "st" (Bool (Bool (Set (Var "A")) "is"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S2")))) "holds"  (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S2")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S1")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S2"))))  ")" ))) ; 
 registrationlet "S" be  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::); let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#v1_msafree1 :::"disjoint_valued"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A") ->   ($#v2_funct_1 :::"one-to-one"::: )   ; 
end; 
theorem :: ALGSPEC1:61 (Bool  "for" (Set (Var "S")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v1_msafree1 :::"disjoint_valued"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "C1")) "," (Set (Var "C2")) "being"   ($#m1_subset_1 :::"Component":::) "of" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  "holds"  (Bool  "("  (Bool (Set (Var "C1"))  ($#r1_hidden :::"="::: )  (Set (Var "C2"))) "or" (Bool (Set (Var "C1"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "C2")))  ")" )))) ; 
 
theorem :: ALGSPEC1:62 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#v1_msafree1 :::"disjoint_valued"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A")) "is"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S9")))) "holds"  (Bool (Set   ($#g1_msualg_1 :::"ManySortedSign"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S"))) "," (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))) "#)" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_msualg_1 :::"ManySortedSign"::: )  "(#"  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S9"))) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S9"))) "," (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S9"))) "," (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S9"))) "#)" )))) ; 
 
theorem :: ALGSPEC1:63 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )   ($#l1_msualg_1 :::"Signature":::)  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#v1_msafree1 :::"disjoint_valued"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  "st" (Bool (Bool (Set (Var "A")) "is"    ($#m4_algspec1 :::"Algebra"::: )   "of" (Set (Var "S9")))) "holds"  (Bool (Set (Var "S")) "is"    ($#m2_algspec1 :::"Extension"::: )   "of" (Set (Var "S9"))))) ;