:: FREEALG  semantic presentation begin  






definitionlet "IT" be    ($#m1_hidden :::"set"::: )  ; attr "IT" is  :::"disjoint_with_NAT":::  means :: FREEALG:def 1 (Bool "IT"  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k5_numbers :::"NAT"::: )  )); end; 




:: deftheorem    defines :::"disjoint_with_NAT"::: FREEALG:def 1 :  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v1_freealg :::"disjoint_with_NAT"::: )  ) "iff" (Bool (Set (Var "IT"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k5_numbers :::"NAT"::: )  ))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; notationlet "IT" be   ($#m1_hidden :::"Relation":::); antonym  :::"with_zero"::: "IT" for  :::"non-empty"::: ; synonym  :::"without_zero"::: "IT" for  :::"non-empty"::: ; end; definitionlet "IT" be   ($#m1_hidden :::"Relation":::); redefine attr "IT" is  :::"non-empty":::  means :: FREEALG:def 2 (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  "IT"))); end; 




:: deftheorem    defines :::"with_zero"::: FREEALG:def 2 :  (Bool  "for" (Set (Var "IT")) "being"   ($#m1_hidden :::"Relation":::) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "IT")) "is"   ($#v2_relat_1 :::"with_zero"::: )  )) "iff" (Bool (Bool  "not" (Set   ($#k6_numbers :::"0"::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "IT")))))  ")" )); 
 registration
cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"with_zero"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 

cluster  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_relat_1 :::"Relation-like"::: )     ($#v2_relat_1 :::"without_zero"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v4_relat_1 :::"-defined"::: )   (Set   ($#k5_numbers :::"NAT"::: )  )  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )   bbbadV1_FINSET_1()   ($#v1_finseq_1 :::"FinSequence-like"::: )     ($#v2_finseq_1 :::"FinSubsequence-like"::: )    for    ($#m1_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); 
end; begin  definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "n" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); assume 
(Bool (Set (Const "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Const "U1")))))
 ; func  :::"oper":::  "(" "n" "," "U1" ")"  ->   ($#m5_margrel1 :::"operation":::) "of" "U1" equals :: FREEALG:def 3 (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")  ($#k1_funct_1 :::"."::: )  "n"); end; 







:: deftheorem    defines :::"oper"::: FREEALG:def 3 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))))) "holds"  (Bool (Set   ($#k1_freealg :::"oper"::: )   "(" (Set (Var "n")) "," (Set (Var "U1")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); mode  :::"GeneratorSet":::  "of" "U0" ->   ($#m1_subset_1 :::"Subset":::) "of" "U0" means :: FREEALG:def 4 (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" "U0"  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  ) & (Bool it  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U0"))); end; 





:: deftheorem    defines :::"GeneratorSet"::: FREEALG:def 4 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set (Var "U0"))) "iff" (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool (Set (Var "A")) "is"   ($#v1_unialg_2 :::"opers_closed"::: )  ) & (Bool (Set (Var "b2"))  ($#r1_tarski :::"c="::: )  (Set (Var "A")))) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U0")))))  ")" ))); 
 definitionlet "U0" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "IT" be    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set (Const "U0")); attr "IT" is  :::"free":::  means :: FREEALG:def 5 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool "U0" "," (Set (Var "U1"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "IT" "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))) (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" "U0" "," (Set (Var "U1")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  "U0" "," (Set (Var "U1"))) & (Bool (Set (Set (Var "h"))  ($#k2_partfun1 :::"|"::: )  "IT")  ($#r1_hidden :::"="::: )  (Set (Var "f")))  ")" )))); end; 





:: deftheorem    defines :::"free"::: FREEALG:def 5 :  (Bool  "for" (Set (Var "U0")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "IT")) "being"    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set (Var "U0")) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v2_freealg :::"free"::: )  ) "iff" (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U0")) "," (Set (Var "U1"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "IT")) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))) (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U0")) "," (Set (Var "U1")) "st"  (Bool  "("  (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U0")) "," (Set (Var "U1"))) & (Bool (Set (Set (Var "h"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "IT")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))  ")" ))))  ")" ))); 
 definitionlet "IT" be   ($#l1_unialg_1 :::"Universal_Algebra":::); attr "IT" is  :::"free":::  means :: FREEALG:def 6 (Bool  "ex" (Set (Var "G")) "being"    ($#m1_freealg :::"GeneratorSet"::: )   "of" "IT" "st" (Bool (Set (Var "G")) "is"   ($#v2_freealg :::"free"::: )  )); end; 




:: deftheorem    defines :::"free"::: FREEALG:def 6 :  (Bool  "for" (Set (Var "IT")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_freealg :::"free"::: )  ) "iff" (Bool  "ex" (Set (Var "G")) "being"    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set (Var "IT")) "st" (Bool (Set (Var "G")) "is"   ($#v2_freealg :::"free"::: )  ))  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )   bbbadV2_UNIALG_1()   ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#v3_freealg :::"free"::: )    for    ($#l1_unialg_1 :::"UAStr"::: )  ; 
end; registrationlet "U0" be   ($#v3_freealg :::"free"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster   ($#v2_freealg :::"free"::: )    for    ($#m1_freealg :::"GeneratorSet"::: )   "of" "U0"; 
end; 
theorem :: FREEALG:1 (Bool  "for" (Set (Var "U0")) "being"   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "A")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U0"))  "st" (Bool (Bool  "("  (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set (Var "U0")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) "or" (Bool (Set (Var "A"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )) "holds"  (Bool  "("  (Bool (Set (Var "A")) "is"    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set (Var "U0"))) "iff" (Bool (Set   ($#k7_unialg_2 :::"GenUnivAlg"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set (Var "U0")))  ")" ))) ; 
 begin  definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"REL":::  "(" "f" "," "X" ")"  ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  "f" ")" )  ($#k2_xboole_0 :::"\/"::: )  "X" ")" ) "," (Set  "(" (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  "f" ")" )  ($#k2_xboole_0 :::"\/"::: )  "X" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) means :: FREEALG:def 7 (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  "f" ")" )  ($#k2_xboole_0 :::"\/"::: )  "X")  (Bool  "for" (Set (Var "b")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  "f" ")" )  ($#k2_xboole_0 :::"\/"::: )  "X" ")" )  ($#k3_finseq_2 :::"*"::: )  ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  "f")) & (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b"))))  ")" )  ")" ))); end; 






:: deftheorem    defines :::"REL"::: FREEALG:def 7 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Relation":::) "of" (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")) ")" ) "," (Set  "(" (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_freealg :::"REL"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" )) "iff" (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")))  (Bool  "for" (Set (Var "b")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")) ")" )  ($#k3_finseq_2 :::"*"::: )  ) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool  "("  (Bool (Set (Var "a"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b"))))  ")" )  ")" )))  ")" )))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; func  :::"DTConUA":::  "(" "f" "," "X" ")"  ->   ($#v1_lang1 :::"strict"::: )     ($#l1_lang1 :::"DTConstrStr"::: )   equals :: FREEALG:def 8 (Set   ($#g1_lang1 :::"DTConstrStr"::: )  "(#"  (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  "f" ")" )  ($#k2_xboole_0 :::"\/"::: )  "X" ")" ) "," (Set  "("  ($#k2_freealg :::"REL"::: )   "(" "f" "," "X" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"DTConUA"::: FREEALG:def 8 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_lang1 :::"DTConstrStr"::: )  "(#"  (Set  "(" (Set  "("  ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "X")) ")" ) "," (Set  "("  ($#k2_freealg :::"REL"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")"  ")" ) "#)" )))); 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "X" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )   ; 
end; 
theorem :: FREEALG:2 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")"  ")" ))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))  ")" ))) ; 
 
theorem :: FREEALG:3 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "X")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "X"))))) ; 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "X" ")" ) ->   ($#v1_lang1 :::"strict"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )   ; 
end; registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "X" ")" ) ->   ($#v1_lang1 :::"strict"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )   ; 
end; registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")" ) ->   ($#v1_lang1 :::"strict"::: )     ($#v1_dtconstr :::"with_terminals"::: )     ($#v2_dtconstr :::"with_nonterminals"::: )     ($#v3_dtconstr :::"with_useful_nonterminals"::: )   ; 
end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "X" be    ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Const "f"))))
 ; func  :::"Sym":::  "(" "n" "," "f" "," "X" ")"  ->   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "X" ")"  ")" ) equals :: FREEALG:def 9 "n"; end; 








:: deftheorem    defines :::"Sym"::: FREEALG:def 9 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k4_freealg :::"Sym"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "X")) ")" )  ($#r1_hidden :::"="::: )  (Set (Var "n")))))); 
 begin  definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Const "f"))))
 ; func  :::"FreeOpNSG":::  "(" "n" "," "f" "," "D" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) means :: FREEALG:def 10 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_freealg :::"Sym"::: )   "(" "n" "," "f" "," "D" ")"  ")" )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p"))))  ")" )  ")" ); end; 








:: deftheorem    defines :::"FreeOpNSG"::: FREEALG:def 10 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_freealg :::"FreeOpNSG"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_freealg :::"Sym"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p"))))  ")" )  ")" )  ")" ))))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeOpSeqNSG":::  "(" "f" "," "D" ")"  ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) means :: FREEALG:def 11 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_freealg :::"FreeOpNSG"::: )   "(" (Set (Var "n")) "," "f" "," "D" ")" ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"FreeOpSeqNSG"::: FREEALG:def 11 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_freealg :::"FreeOpSeqNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_freealg :::"FreeOpNSG"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")" ))  ")" )  ")" )  ")" )))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeUnivAlgNSG":::  "(" "f" "," "D" ")"  ->   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) equals :: FREEALG:def 12 (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) "," (Set  "("  ($#k6_freealg :::"FreeOpSeqNSG"::: )   "(" "f" "," "D" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"FreeUnivAlgNSG"::: FREEALG:def 12 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "," (Set  "("  ($#k6_freealg :::"FreeOpSeqNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) "#)" )))); 
 
theorem :: FREEALG:4 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set  "("  ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))) ; 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeGenSetNSG":::  "(" "f" "," "D" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" "f" "," "D" ")"  ")" ) equals :: FREEALG:def 13  "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" ) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) : (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" )))  "}"  ; end; 






:: deftheorem    defines :::"FreeGenSetNSG"::: FREEALG:def 13 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k8_freealg :::"FreeGenSetNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" ) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) : (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )))  "}"  ))); 
 
theorem :: FREEALG:5 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    "holds" (Bool (Bool  "not" (Set   ($#k8_freealg :::"FreeGenSetNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  )))) ; 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"FreeGenSetNSG"::: redefine func  :::"FreeGenSetNSG":::  "(" "f" "," "D" ")"  ->    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set   ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" "f" "," "D" ")" ); end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; let "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" ); let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_freealg :::"FreeGenSetNSG"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" ) "," (Set (Const "C")); assume 
(Bool (Set (Const "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" )))
 ; func  :::"pi":::  "(" "F" "," "s" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "C" equals :: FREEALG:def 14 (Set "F"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  "s" ")" )); end; 










:: deftheorem    defines :::"pi"::: FREEALG:def 14 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k9_freealg :::"FreeGenSetNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k6_dtconstr :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )))) "holds"  (Bool (Set   ($#k10_freealg :::"pi"::: )   "(" (Set (Var "F")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" )))))))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" ); given "p" being   ($#m1_hidden :::"FinSequence":::) such that 
(Bool (Set (Const "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Const "p")))
 ; func  :::"@"::: "s" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ) equals :: FREEALG:def 15 "s"; end; 








:: deftheorem    defines :::"@"::: FREEALG:def 15 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )  "st" (Bool (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "p"))))) "holds"  (Bool (Set   ($#k11_freealg :::"@"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set (Var "s")))))); 
 
theorem :: FREEALG:6 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k9_freealg :::"FreeGenSetNSG"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) "is"   ($#v2_freealg :::"free"::: )  ))) ; 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" "f" "," "D" ")" ) ->   ($#v1_unialg_1 :::"strict"::: )     ($#v3_freealg :::"free"::: )   ; 
end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"FreeGenSetNSG"::: redefine func  :::"FreeGenSetNSG":::  "(" "f" "," "D" ")"  ->   ($#v2_freealg :::"free"::: )     ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set   ($#k7_freealg :::"FreeUnivAlgNSG"::: )   "(" "f" "," "D" ")" ); end; begin  definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; let "n" be   ($#m1_hidden :::"Nat":::); assume 
(Bool (Set (Const "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Const "f"))))
 ; func  :::"FreeOpZAO":::  "(" "n" "," "f" "," "D" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) means :: FREEALG:def 16 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k7_partfun1 :::"/."::: )  "n" ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_freealg :::"Sym"::: )   "(" "n" "," "f" "," "D" ")"  ")" )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p"))))  ")" )  ")" ); end; 








:: deftheorem    defines :::"FreeOpZAO"::: FREEALG:def 16 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool  "for" (Set (Var "b4")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_freealg :::"FreeOpZAO"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k7_partfun1 :::"/."::: )  (Set (Var "n")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "p")) "being"    ($#m1_trees_4 :::"FinSequence"::: )   "of" (Set   ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ))  "st" (Bool (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4"))))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k4_freealg :::"Sym"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )  ($#k8_trees_4 :::"-tree"::: )  (Set (Var "p"))))  ")" )  ")" )  ")" ))))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeOpSeqZAO":::  "(" "f" "," "D" ")"  ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) means :: FREEALG:def 17 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  "f")) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k13_freealg :::"FreeOpZAO"::: )   "(" (Set (Var "n")) "," "f" "," "D" ")" ))  ")" )  ")" ); end; 






:: deftheorem    defines :::"FreeOpSeqZAO"::: FREEALG:def 17 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k14_freealg :::"FreeOpSeqZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "f")))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k13_freealg :::"FreeOpZAO"::: )   "(" (Set (Var "n")) "," (Set (Var "f")) "," (Set (Var "D")) ")" ))  ")" )  ")" )  ")" )))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeUnivAlgZAO":::  "(" "f" "," "D" ")"  ->   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) equals :: FREEALG:def 18 (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) ")" ) "," (Set  "("  ($#k14_freealg :::"FreeOpSeqZAO"::: )   "(" "f" "," "D" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"FreeUnivAlgZAO"::: FREEALG:def 18 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k4_dtconstr :::"TS"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) ")" ) "," (Set  "("  ($#k14_freealg :::"FreeOpSeqZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) "#)" )))); 
 
theorem :: FREEALG:7 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_unialg_1 :::"signature"::: )  (Set  "("  ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "f"))))) ; 
 
theorem :: FREEALG:8 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) "is"   ($#v2_unialg_2 :::"with_const_op"::: )  ))) ; 
 
theorem :: FREEALG:9 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    "holds" (Bool (Set   ($#k6_unialg_2 :::"Constants"::: )  (Set  "("  ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) ; 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; func  :::"FreeGenSetZAO":::  "(" "f" "," "D" ")"  ->   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" "f" "," "D" ")"  ")" ) equals :: FREEALG:def 19  "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" ) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" ) : (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" "f" "," "D" ")"  ")" )))  "}"  ; end; 






:: deftheorem    defines :::"FreeGenSetZAO"::: FREEALG:def 19 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k16_freealg :::"FreeGenSetZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" )  ($#r1_hidden :::"="::: )   "{"  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" ) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) : (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )))  "}"  ))); 
 definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"FreeGenSetZAO"::: redefine func  :::"FreeGenSetZAO":::  "(" "f" "," "D" ")"  ->    ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set   ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" "f" "," "D" ")" ); end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; let "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "s" be   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" ); let "F" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k17_freealg :::"FreeGenSetZAO"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" ) "," (Set (Const "C")); assume 
(Bool (Set (Const "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Const "f")) "," (Set (Const "D")) ")"  ")" )))
 ; func  :::"pi":::  "(" "F" "," "s" ")"  ->    ($#m1_subset_1 :::"Element"::: )   "of" "C" equals :: FREEALG:def 20 (Set "F"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  "s" ")" )); end; 










:: deftheorem    defines :::"pi"::: FREEALG:def 20 :  (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )  (Bool  "for" (Set (Var "F")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k17_freealg :::"FreeGenSetZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" ) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k3_freealg :::"DTConUA"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")"  ")" )))) "holds"  (Bool (Set   ($#k18_freealg :::"pi"::: )   "(" (Set (Var "F")) "," (Set (Var "s")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_trees_4 :::"root-tree"::: )  (Set (Var "s")) ")" )))))))); 
 
theorem :: FREEALG:10 (Bool  "for" (Set (Var "f")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "D")) "being"   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k17_freealg :::"FreeGenSetZAO"::: )   "(" (Set (Var "f")) "," (Set (Var "D")) ")" ) "is"   ($#v2_freealg :::"free"::: )  ))) ; 
 registrationlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" "f" "," "D" ")" ) ->   ($#v1_unialg_1 :::"strict"::: )     ($#v3_freealg :::"free"::: )   ; 
end; definitionlet "f" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_relat_1 :::"with_zero"::: )     ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  ); let "D" be   ($#v1_freealg :::"disjoint_with_NAT"::: )     ($#m1_hidden :::"set"::: )  ; :: original: :::"FreeGenSetZAO"::: redefine func  :::"FreeGenSetZAO":::  "(" "f" "," "D" ")"  ->   ($#v2_freealg :::"free"::: )     ($#m1_freealg :::"GeneratorSet"::: )   "of" (Set   ($#k15_freealg :::"FreeUnivAlgZAO"::: )   "(" "f" "," "D" ")" ); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_unialg_1 :::"strict"::: )   bbbadV2_UNIALG_1()   ($#v3_unialg_1 :::"quasi_total"::: )     ($#v4_unialg_1 :::"non-empty"::: )     ($#v2_unialg_2 :::"with_const_op"::: )     ($#v3_freealg :::"free"::: )    for    ($#l1_unialg_1 :::"UAStr"::: )  ; 
end;