:: BIRKHOFF  semantic presentation 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 "X" be bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "S"))); let "A" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); let "F" be    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Const "X")) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Const "A"))); func "F" :::"-hash":::  ->   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  "X" ")" ) "," "A" means :: BIRKHOFF:def 1 (Bool  "("  (Bool it  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set   ($#k11_msafree :::"FreeMSA"::: )  "X") "," "A") & (Bool (Set it  ($#k1_msafree :::"||"::: )  (Set  "("  ($#k13_msafree :::"FreeGen"::: )  "X" ")" ))  ($#r8_pboole :::"="::: )  (Set "F"  ($#k3_msualg_3 :::"**"::: )  (Set  "("  ($#k15_msafree :::"Reverse"::: )  "X" ")" )))  ")" ); end; 








:: deftheorem    defines :::"-hash"::: BIRKHOFF:def 1 :  (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 "X")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "X")) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  (Bool  "for" (Set (Var "b5")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X")) ")" ) "," (Set (Var "A")) "holds"   (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_birkhoff :::"-hash"::: )  )) "iff" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set   ($#k11_msafree :::"FreeMSA"::: )  (Set (Var "X"))) "," (Set (Var "A"))) & (Bool (Set (Set (Var "b5"))  ($#k1_msafree :::"||"::: )  (Set  "("  ($#k13_msafree :::"FreeGen"::: )  (Set (Var "X")) ")" ))  ($#r8_pboole :::"="::: )  (Set (Set (Var "F"))  ($#k3_msualg_3 :::"**"::: )  (Set  "("  ($#k15_msafree :::"Reverse"::: )  (Set (Var "X")) ")" )))  ")" )  ")" )))))); 
 
theorem :: BIRKHOFF:1 (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 "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "X")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "X")) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "holds"  (Bool (Set   ($#k3_funct_6 :::"rngs"::: )  (Set (Var "F")))  ($#r2_pboole :::"c="::: )  (Set   ($#k3_funct_6 :::"rngs"::: )  (Set  "(" (Set (Var "F"))  ($#k1_birkhoff :::"-hash"::: )  ")" ))))))) ; 
 scheme  :: BIRKHOFF:sch 1 ExFreeAlg1{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "A")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )(Bool  "ex" (Set (Var "F")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "A")) "st"  (Bool  "("  (Bool P1[(Set (Var "A"))]) & (Bool (Set (Var "F"))  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "A"))) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "G"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "B"))) & (Bool P1[(Set (Var "B"))])) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "A")) "," (Set (Var "B"))) & (Bool (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")))  ($#r8_pboole :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Set (Var "K"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")))  ($#r8_pboole :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "H"))  ($#r8_pboole :::"="::: )  (Set (Var "K")))  ")" )  ")" )))  ")" )  ")" )))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 and  
(Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "A"))])  ")" ))  ")" )) "holds"  (Bool P1[(Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "F")))])))
 proof 


end; scheme  :: BIRKHOFF:sch 2 ExFreeAlg2{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() -> bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "A")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )(Bool  "ex" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set F2 "("  ")" ) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A"))) "st"  (Bool  "("  (Bool P1[(Set (Var "A"))]) & (Bool  "("   "for" (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set F2 "("  ")" ) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "B")))  "st" (Bool (Bool P1[(Set (Var "B"))])) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "A")) "," (Set (Var "B"))) & (Bool (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")))  ($#r8_pboole :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "A")) "," (Set (Var "B"))) & (Bool (Set (Set (Var "K"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")))  ($#r8_pboole :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "H"))  ($#r8_pboole :::"="::: )  (Set (Var "K")))  ")" )  ")" )))  ")" )  ")" )))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 and  
(Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "A"))])  ")" ))  ")" )) "holds"  (Bool P1[(Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "F")))])))
 proof 


end; scheme  :: BIRKHOFF:sch 3 Exhash{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F4() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F2 "("  ")" )), F5() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F3 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set F3 "("  ")" )) & (Bool (Set (Set F5 "("  ")" )  ($#k1_birkhoff :::"-hash"::: )  )  ($#r8_pboole :::"="::: )  (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set  "(" (Set F4 "("  ")" )  ($#k1_birkhoff :::"-hash"::: )  ")" )))  ")" ))
 provided
(Bool P1[(Set F3 "("  ")" )])
 and  
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P1[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Var "G"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "h"))  ($#k3_msualg_3 :::"**"::: )  (Set F4 "("  ")" )))  ")" ))))
 proof 


end; scheme  :: BIRKHOFF:sch 4 EqTerms{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F2 "("  ")" )), F4() ->   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "("  ")" ), F5() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k3_equation :::"TermAlg"::: )  (Set F1 "("  ")" ) ")" ))  ($#k1_funct_1 :::"."::: )  (Set F4 "("  ")" )), F6() ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k3_equation :::"TermAlg"::: )  (Set F1 "("  ")" ) ")" ))  ($#k1_funct_1 :::"."::: )  (Set F4 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "for" (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "B"))])) "holds"  (Bool (Set (Var "B"))  ($#r1_equation :::"|="::: )  (Set (Set F5 "("  ")" )  ($#k5_equation :::"'='"::: )  (Set F6 "("  ")" ))))
 provided
(Bool (Set (Set  "(" (Set  "(" (Set F3 "("  ")" )  ($#k1_birkhoff :::"-hash"::: )  ")" )  ($#k1_msualg_3 :::"."::: )  (Set F4 "("  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set F5 "("  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set F3 "("  ")" )  ($#k1_birkhoff :::"-hash"::: )  ")" )  ($#k1_msualg_3 :::"."::: )  (Set F4 "("  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set F6 "("  ")" )))
 and  
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P1[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Var "G"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "h"))  ($#k3_msualg_3 :::"**"::: )  (Set F3 "("  ")" )))  ")" ))))
 proof 


end; scheme  :: BIRKHOFF:sch 5 FreeIsGen{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() -> bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" )), F3() ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F4() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set F2 "("  ")" ) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F3 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set (Set F4 "("  ")" )  ($#k9_pboole :::".:.:"::: )  (Set F2 "("  ")" )) "is" bbbadV2_RELAT_1()   ($#m1_msafree :::"GeneratorSet"::: )   "of" (Set F3 "("  ")" ))
 provided
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set F2 "("  ")" ) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P1[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F3 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F3 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set F4 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F3 "("  ")" ) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F3 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "K"))  ($#k3_msualg_3 :::"**"::: )  (Set F4 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "H"))  ($#r8_pboole :::"="::: )  (Set (Var "K")))  ")" )  ")" ))))
 and  
(Bool P1[(Set F3 "("  ")" )])
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 proof 


end; scheme  :: BIRKHOFF:sch 6 Hashisonto{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F2 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool (Set (Set F3 "("  ")" )  ($#k1_birkhoff :::"-hash"::: )  )  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set   ($#k11_msafree :::"FreeMSA"::: )  (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) ) ")" )) "," (Set F2 "("  ")" ))
 provided
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P1[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set F3 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "K"))  ($#k3_msualg_3 :::"**"::: )  (Set F3 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "H"))  ($#r8_pboole :::"="::: )  (Set (Var "K")))  ")" )  ")" ))))
 and  
(Bool P1[(Set F2 "("  ")" )])
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 proof 


end; scheme  :: BIRKHOFF:sch 7 FinGenAlgInVar{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#v3_msafree2 :::"finitely-generated"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F4() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F3 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P1[(Set F2 "("  ")" )])
 provided
(Bool P2[(Set F2 "("  ")" )])
 and  
(Bool P1[(Set F3 "("  ")" )])
 and  
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P2[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "h")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F3 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F3 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Var "G"))  ($#r8_pboole :::"="::: )  (Set (Set (Var "h"))  ($#k3_msualg_3 :::"**"::: )  (Set F4 "("  ")" )))  ")" ))))
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k13_msualg_4 :::"QuotMSAlg"::: )   "(" (Set (Var "A")) "," (Set (Var "R")) ")" )])))
 proof 


end; scheme  :: BIRKHOFF:sch 8 QuotEpi{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P1[(Set F3 "("  ")" )])
 provided
(Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set F3 "("  ")" ) "st" (Bool (Set (Var "H"))  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set F2 "("  ")" ) "," (Set F3 "("  ")" )))
 and  
(Bool P1[(Set F2 "("  ")" )])
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k13_msualg_4 :::"QuotMSAlg"::: )   "(" (Set (Var "A")) "," (Set (Var "R")) ")" )])))
 proof 


end; scheme  :: BIRKHOFF:sch 9 AllFinGen{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P1[(Set F2 "("  ")" )])
 provided
(Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#v3_msafree2 :::"finitely-generated"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set F2 "("  ")" ) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k13_msualg_4 :::"QuotMSAlg"::: )   "(" (Set (Var "A")) "," (Set (Var "R")) ")" )])))
 and  
(Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "A"))])  ")" ))  ")" )) "holds"  (Bool P1[(Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "F")))])))
 proof 


end; scheme  :: BIRKHOFF:sch 10 FreeInModIsInVar1{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P2[(Set F2 "("  ")" )])
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool P2[(Set (Var "A"))]) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "("  ($#k4_equation :::"Equations"::: )  (Set F1 "("  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  "st" (Bool (Bool  "("   "for" (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "B"))])) "holds"  (Bool (Set (Var "B"))  ($#r1_equation :::"|="::: )  (Set (Var "e")))  ")" )) "holds"  (Bool (Set (Var "A"))  ($#r1_equation :::"|="::: )  (Set (Var "e")))))  ")" ))
 and  
(Bool P1[(Set F2 "("  ")" )])
 proof 


end; scheme  :: BIRKHOFF:sch 11 FreeInModIsInVar{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , F2() ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ), F3() ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set F2 "("  ")" )), P1[   ($#m1_hidden :::"set"::: )  ], P2[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool P1[(Set F2 "("  ")" )])
 provided
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool P2[(Set (Var "A"))]) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "e")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "("  ($#k4_equation :::"Equations"::: )  (Set F1 "("  ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  "st" (Bool (Bool  "("   "for" (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool P1[(Set (Var "B"))])) "holds"  (Bool (Set (Var "B"))  ($#r1_equation :::"|="::: )  (Set (Var "e")))  ")" )) "holds"  (Bool (Set (Var "A"))  ($#r1_equation :::"|="::: )  (Set (Var "e")))))  ")" ))
 and  
(Bool  "for" (Set (Var "C")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set F1 "("  ")" ))  ($#k7_funcop_1 :::"-->"::: )  (Set  ($#k5_numbers :::"NAT"::: ) )) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "C")))  "st" (Bool (Bool P2[(Set (Var "C"))])) "holds"  (Bool  "ex" (Set (Var "H")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C")) "st"  (Bool  "("  (Bool (Set (Var "H"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "H"))  ($#k3_msualg_3 :::"**"::: )  (Set F3 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G"))) & (Bool  "("   "for" (Set (Var "K")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set F2 "("  ")" ) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "K"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set F2 "("  ")" ) "," (Set (Var "C"))) & (Bool (Set (Set (Var "K"))  ($#k3_msualg_3 :::"**"::: )  (Set F3 "("  ")" ))  ($#r8_pboole :::"="::: )  (Set (Var "G")))) "holds"  (Bool (Set (Var "H"))  ($#r8_pboole :::"="::: )  (Set (Var "K")))  ")" )  ")" ))))
 and  
(Bool P2[(Set F2 "("  ")" )])
 and  
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 and  
(Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "A"))])  ")" ))  ")" )) "holds"  (Bool P1[(Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "F")))])))
 proof 


end; scheme  :: BIRKHOFF:sch 12 Birkhoff{ F1() ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  , P1[   ($#m1_hidden :::"set"::: )  ] } : 
(Bool  "ex" (Set (Var "E")) "being"   ($#m3_pboole :::"EqualSet":::) "of" (Set F1 "("  ")" ) "st"  (Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "holds"   (Bool  "("  (Bool P1[(Set (Var "A"))]) "iff" (Bool (Set (Var "A"))  ($#r2_equation :::"|="::: )  (Set (Var "E")))  ")" )))
 provided
(Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  "st" (Bool (Bool (Set (Var "A")) "," (Set (Var "B"))  ($#r6_msualg_3 :::"are_isomorphic"::: )  ) & (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))]))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "B")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#m1_msualg_2 :::"MSSubAlgebra"::: )   "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set (Var "B"))])))
 and  
(Bool  "for" (Set (Var "A")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" )  (Bool  "for" (Set (Var "R")) "being"   ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))  "st" (Bool (Bool P1[(Set (Var "A"))])) "holds"  (Bool P1[(Set   ($#k13_msualg_4 :::"QuotMSAlg"::: )   "(" (Set (Var "A")) "," (Set (Var "R")) ")" )])))
 and  
(Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "F")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set F1 "("  ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "A")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set F1 "("  ")" ) "st"  (Bool  "("  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool P1[(Set (Var "A"))])  ")" ))  ")" )) "holds"  (Bool P1[(Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "F")))])))
 proof 


end;