:: LANG1  semantic presentation begin  definitionattr "c1" is  :::"strict"::: ; struct  :::"DTConstrStr":::  ->    ($#l1_struct_0 :::"1-sorted"::: )  ; aggr :::"DTConstrStr":::(# :::"carrier":::, :::"Rules"::: #) ->    ($#l1_lang1 :::"DTConstrStr"::: )  ; sel  :::"Rules"::: "c1" ->   ($#m1_subset_1 :::"Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1") "," (Set  "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1")  ($#k3_finseq_2 :::"*"::: )  ")" ); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_lang1 :::"strict"::: )    for    ($#l1_lang1 :::"DTConstrStr"::: )  ; 
end; definitionattr "c1" is  :::"strict"::: ; struct  :::"GrammarStr":::  ->    ($#l1_lang1 :::"DTConstrStr"::: )  ; aggr :::"GrammarStr":::(# :::"carrier":::, :::"InitialSym":::, :::"Rules"::: #) ->    ($#l2_lang1 :::"GrammarStr"::: )  ; sel  :::"InitialSym"::: "c1" ->    ($#m1_subset_1 :::"Element"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "c1"); end; registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   for    ($#l2_lang1 :::"GrammarStr"::: )  ; 
end; definitionlet "G" be    ($#l1_lang1 :::"DTConstrStr"::: )  ; mode Symbol of "G" is   ($#m1_subset_1 :::"Element":::) "of" "G"; mode String of "G" is    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ); end; 









definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; let "s" be   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Const "G")); let "n" be   ($#m1_hidden :::"FinSequence":::); pred "s" :::"==>"::: "n" means :: LANG1:def 1 (Bool (Set  ($#k4_tarski :::"["::: ) "s" "," "n" ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" "G")); end; 






:: deftheorem    defines :::"==>"::: LANG1:def 1 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"FinSequence":::) "holds"   (Bool  "("  (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n"))) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "s")) "," (Set (Var "n")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "G"))))  ")" )))); 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; func  :::"Terminals"::: "G" ->    ($#m1_hidden :::"set"::: )   equals :: LANG1:def 2  "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" "G" : (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"FinSequence":::)  "holds" (Bool (Bool  "not" (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n")))))  "}"  ; func  :::"NonTerminals"::: "G" ->    ($#m1_hidden :::"set"::: )   equals :: LANG1:def 3  "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" "G" : (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n"))))  "}"  ; end; 










:: deftheorem    defines :::"Terminals"::: LANG1:def 2 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) : (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"FinSequence":::)  "holds" (Bool (Bool  "not" (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n")))))  "}"  )); 
 
:: deftheorem    defines :::"NonTerminals"::: LANG1:def 3 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"  (Bool (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "s")) where s "is"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) : (Bool  "ex" (Set (Var "n")) "being"   ($#m1_hidden :::"FinSequence":::) "st" (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n"))))  "}"  )); 
 
theorem :: LANG1:1 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )   "holds"  (Bool (Set (Set  "("  ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")) ")" )  ($#k2_xboole_0 :::"\/"::: )  (Set  "("  ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "G")) ")" ))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))))) ; 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; let "n", "m" be   ($#m2_finseq_2 :::"String":::) "of" (Set (Const "G")); pred "n" :::"==>"::: "m" means :: LANG1:def 4 (Bool  "ex" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being"   ($#m2_finseq_2 :::"String":::) "of" "G"(Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "G" "st"  (Bool  "("  (Bool "n"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "s")) ($#k3_pre_poly :::"*>"::: ) ) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))) & (Bool "m"  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n3")) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))) & (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n3")))  ")" ))); end; 






:: deftheorem    defines :::"==>"::: LANG1:def 4 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_lang1 :::"==>"::: )  (Set (Var "m"))) "iff" (Bool  "ex" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))(Bool  "ex" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Var "n"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "s")) ($#k3_pre_poly :::"*>"::: ) ) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))) & (Bool (Set (Var "m"))  ($#r2_relset_1 :::"="::: )  (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n3")) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))) & (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n3")))  ")" )))  ")" ))); 
 





theorem :: LANG1:2 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "n")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "s")) ($#k3_pre_poly :::"*>"::: ) ) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))  ($#r2_lang1 :::"==>"::: )  (Set (Set  "(" (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n")) ")" )  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2"))))))) ; 
 
theorem :: LANG1:3 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "n")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n")))) "holds"  (Bool (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "s")) ($#k3_pre_poly :::"*>"::: ) )  ($#r2_lang1 :::"==>"::: )  (Set (Var "n")))))) ; 
 
theorem :: LANG1:4 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "G"))  (Bool  "for" (Set (Var "n")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set  ($#k3_pre_poly :::"<*"::: ) (Set (Var "s")) ($#k3_pre_poly :::"*>"::: ) )  ($#r2_lang1 :::"==>"::: )  (Set (Var "n")))) "holds"  (Bool (Set (Var "s"))  ($#r1_lang1 :::"==>"::: )  (Set (Var "n")))))) ; 
 
theorem :: LANG1:5 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "n1"))  ($#r2_lang1 :::"==>"::: )  (Set (Var "n2")))) "holds"  (Bool  "("  (Bool (Set (Set (Var "n"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n1")))  ($#r2_lang1 :::"==>"::: )  (Set (Set (Var "n"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n2")))) & (Bool (Set (Set (Var "n1"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n")))  ($#r2_lang1 :::"==>"::: )  (Set (Set (Var "n2"))  ($#k1_pre_poly :::"^"::: )  (Set (Var "n"))))  ")" ))) ; 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )  ; let "n", "m" be   ($#m2_finseq_2 :::"String":::) "of" (Set (Const "G")); pred "m" :::"is_derivable_from"::: "n" means :: LANG1:def 5 (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  "n") & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  "m") & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m2_finseq_2 :::"String":::) "of" "G" "st"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_lang1 :::"==>"::: )  (Set (Var "b")))  ")" ))  ")" )  ")" )); end; 






:: deftheorem    defines :::"is_derivable_from"::: LANG1:def 5 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "m"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n"))) "iff" (Bool  "ex" (Set (Var "p")) "being"   ($#m1_hidden :::"FinSequence":::) "st"  (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Num 1))  ($#r1_hidden :::"="::: )  (Set (Var "n"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k3_finseq_1 :::"len"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "m"))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::">="::: )  (Num 1)) & (Bool (Set (Var "i"))  ($#r1_xxreal_0 :::"<"::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "p"))))) "holds"  (Bool  "ex" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G")) "st"  (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "i"))  ($#k2_nat_1 :::"+"::: )  (Num 1) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "b"))) & (Bool (Set (Var "a"))  ($#r2_lang1 :::"==>"::: )  (Set (Var "b")))  ")" ))  ")" )  ")" ))  ")" ))); 
 
theorem :: LANG1:6 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G")) "holds"  (Bool (Set (Var "n"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n"))))) ; 
 
theorem :: LANG1:7 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n")) "," (Set (Var "m")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "n"))  ($#r2_lang1 :::"==>"::: )  (Set (Var "m")))) "holds"  (Bool (Set (Var "m"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n"))))) ; 
 
theorem :: LANG1:8 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_lang1 :::"DTConstrStr"::: )    (Bool  "for" (Set (Var "n1")) "," (Set (Var "n2")) "," (Set (Var "n3")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G"))  "st" (Bool (Bool (Set (Var "n1"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n2"))) & (Bool (Set (Var "n2"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n3")))) "holds"  (Bool (Set (Var "n1"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set (Var "n3"))))) ; 
 definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )  ; func  :::"Lang"::: "G" ->    ($#m1_hidden :::"set"::: )   equals :: LANG1:def 6  "{"  (Set (Var "a")) where a "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "G")) & (Bool (Set (Var "a"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" "G") ($#k3_pre_poly :::"*>"::: ) ))  ")" )  "}"  ; end; 





:: deftheorem    defines :::"Lang"::: LANG1:def 6 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )   "holds"  (Bool (Set   ($#k3_lang1 :::"Lang"::: )  (Set (Var "G")))  ($#r1_hidden :::"="::: )   "{"  (Set (Var "a")) where a "is"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))  ($#k3_finseq_2 :::"*"::: )  ) : (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "a")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")))) & (Bool (Set (Var "a"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "G"))) ($#k3_pre_poly :::"*>"::: ) ))  ")" )  "}"  )); 
 
theorem :: LANG1:9 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )    (Bool  "for" (Set (Var "n")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "G")) "holds"   (Bool  "("  (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_lang1 :::"Lang"::: )  (Set (Var "G")))) "iff" (Bool  "("  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "n")))  ($#r1_tarski :::"c="::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "G")))) & (Bool (Set (Var "n"))  ($#r3_lang1 :::"is_derivable_from"::: )  (Set  ($#k3_pre_poly :::"<*"::: ) (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "G"))) ($#k3_pre_poly :::"*>"::: ) ))  ")" )  ")" ))) ; 
 definitionlet "D", "E" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "a" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "E")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"{"::: redefine func :::"{":::"a":::"}"::: ->   ($#m1_subset_1 :::"Relation":::) "of" "D" "," "E"; let "b" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "D")) "," (Set (Const "E")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"{"::: redefine func :::"{":::"a" "," "b":::"}"::: ->   ($#m1_subset_1 :::"Relation":::) "of" "D" "," "E"; end; definitionlet "a" be    ($#m1_hidden :::"set"::: )  ; func  :::"EmptyGrammar"::: "a" ->   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   means :: LANG1:def 7 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) "a" ($#k1_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) "a" "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" ); let "b" be    ($#m1_hidden :::"set"::: )  ; func  :::"SingleGrammar":::  "(" "a" "," "b" ")"  ->   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   means :: LANG1:def 8 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) "a" "," "b" ($#k2_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" it)  ($#r1_hidden :::"="::: )  "a") & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) "a" "," (Set  ($#k9_finseq_1 :::"<*"::: ) "b" ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" ); func  :::"IterGrammar":::  "(" "a" "," "b" ")"  ->   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   means :: LANG1:def 9 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) "a" "," "b" ($#k2_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" it)  ($#r1_hidden :::"="::: )  "a") & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) "a" "," (Set  ($#k10_finseq_1 :::"<*"::: ) "b" "," "a" ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) "a" "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))  ")" ); end; 

















:: deftheorem    defines :::"EmptyGrammar"::: LANG1:def 7 :  (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_lang1 :::"EmptyGrammar"::: )  (Set (Var "a")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"SingleGrammar"::: LANG1:def 8 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_lang1 :::"SingleGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))  ")" )  ")" ))); 
 
:: deftheorem    defines :::"IterGrammar"::: LANG1:def 9 :  (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k8_lang1 :::"IterGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")" )) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))) & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "b")) "," (Set (Var "a")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))  ")" )  ")" ))); 
 registrationlet "a" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k6_lang1 :::"EmptyGrammar"::: )  "a") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lang1 :::"strict"::: )   ; 
let "b" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k7_lang1 :::"SingleGrammar"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lang1 :::"strict"::: )   ; 

cluster (Set   ($#k8_lang1 :::"IterGrammar"::: )   "(" "a" "," "b" ")" ) ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lang1 :::"strict"::: )   ; 
end; definitionlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; func  :::"TotalGrammar"::: "D" ->   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   means :: LANG1:def 10 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  "D")) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" it)  ($#r1_hidden :::"="::: )  "D") & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set  "{"  (Set  ($#k4_tarski :::"["::: ) "D" "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d")) "," "D" ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) where d "is"    ($#m1_subset_1 :::"Element"::: )   "of" "D" : (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))  "}"    ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) "D" "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))  ")" ); end; 





:: deftheorem    defines :::"TotalGrammar"::: LANG1:def 10 :  (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "b2")) "being"   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_lang1 :::"TotalGrammar"::: )  (Set (Var "D")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_ordinal1 :::"succ"::: )  (Set (Var "D")))) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Var "D"))) & (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set  "{"  (Set  ($#k4_tarski :::"["::: ) (Set (Var "D")) "," (Set  ($#k10_finseq_1 :::"<*"::: ) (Set (Var "d")) "," (Set (Var "D")) ($#k10_finseq_1 :::"*>"::: ) ) ($#k4_tarski :::"]"::: ) ) where d "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "D")) : (Bool (Set (Var "d"))  ($#r1_hidden :::"="::: )  (Set (Var "d")))  "}"    ($#k2_xboole_0 :::"\/"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "D")) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))  ")" )  ")" ))); 
 registrationlet "D" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k9_lang1 :::"TotalGrammar"::: )  "D") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v2_lang1 :::"strict"::: )   ; 
end; 











theorem :: LANG1:10 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k6_lang1 :::"EmptyGrammar"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: LANG1:11 (Bool  "for" (Set (Var "a")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_lang1 :::"Lang"::: )  (Set  "("  ($#k6_lang1 :::"EmptyGrammar"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: LANG1:12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k7_lang1 :::"SingleGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: LANG1:13 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k3_lang1 :::"Lang"::: )  (Set  "("  ($#k7_lang1 :::"SingleGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k9_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k9_finseq_1 :::"*>"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: LANG1:14 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k8_lang1 :::"IterGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))) ; 
 
theorem :: LANG1:15 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "a"))  ($#r1_hidden :::"<>"::: )  (Set (Var "b")))) "holds"  (Bool (Set   ($#k3_lang1 :::"Lang"::: )  (Set  "("  ($#k8_lang1 :::"IterGrammar"::: )   "(" (Set (Var "a")) "," (Set (Var "b")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) )  ($#k3_finseq_2 :::"*"::: )  ))) ; 
 
theorem :: LANG1:16 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k1_lang1 :::"Terminals"::: )  (Set  "("  ($#k9_lang1 :::"TotalGrammar"::: )  (Set (Var "D")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "D")))) ; 
 
theorem :: LANG1:17 (Bool  "for" (Set (Var "D")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k3_lang1 :::"Lang"::: )  (Set  "("  ($#k9_lang1 :::"TotalGrammar"::: )  (Set (Var "D")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "D"))  ($#k3_finseq_2 :::"*"::: )  ))) ; 
 definitionlet "IT" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )  ; attr "IT" is  :::"efective":::  means :: LANG1:def 11 (Bool  "("  (Bool (Bool  "not" (Set   ($#k3_lang1 :::"Lang"::: )  "IT") "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" "IT")  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lang1 :::"NonTerminals"::: )  "IT")) & (Bool  "("   "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" "IT"  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  "IT"))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m2_finseq_2 :::"String":::) "of" "IT" "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_lang1 :::"Lang"::: )  "IT")) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p"))))  ")" ))  ")" )  ")" ); end; 




:: deftheorem    defines :::"efective"::: LANG1:def 11 :  (Bool  "for" (Set (Var "IT")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v3_lang1 :::"efective"::: )  ) "iff" (Bool  "("  (Bool (Bool  "not" (Set   ($#k3_lang1 :::"Lang"::: )  (Set (Var "IT"))) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "IT")))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_lang1 :::"NonTerminals"::: )  (Set (Var "IT")))) & (Bool  "("   "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "IT"))  "st" (Bool (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_lang1 :::"Terminals"::: )  (Set (Var "IT"))))) "holds"  (Bool  "ex" (Set (Var "p")) "being"   ($#m2_finseq_2 :::"String":::) "of" (Set (Var "IT")) "st"  (Bool  "("  (Bool (Set (Var "p"))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_lang1 :::"Lang"::: )  (Set (Var "IT")))) & (Bool (Set (Var "s"))  ($#r2_hidden :::"in"::: )  (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "p"))))  ")" ))  ")" )  ")" )  ")" )); 
 definitionlet "IT" be    ($#l2_lang1 :::"GrammarStr"::: )  ; attr "IT" is  :::"finite":::  means :: LANG1:def 12 (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" "IT") "is"   ($#v1_finset_1 :::"finite"::: )  ); end; 




:: deftheorem    defines :::"finite"::: LANG1:def 12 :  (Bool  "for" (Set (Var "IT")) "being"    ($#l2_lang1 :::"GrammarStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "IT")) "is"   ($#v4_lang1 :::"finite"::: )  ) "iff" (Bool (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "IT"))) "is"   ($#v1_finset_1 :::"finite"::: )  )  ")" )); 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lang1 :::"efective"::: )     ($#v4_lang1 :::"finite"::: )    for    ($#l2_lang1 :::"GrammarStr"::: )  ; 
end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v3_lang1 :::"efective"::: )     ($#l2_lang1 :::"GrammarStr"::: )  ; :: original: :::"NonTerminals"::: redefine func  :::"NonTerminals"::: "G" ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" "G"; end; definitionlet "X", "Y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "p" be    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set (Const "X")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"*"::: redefine func "f" :::"*"::: "p" ->    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "Y"  ($#k3_finseq_2 :::"*"::: )  ); end; definitionlet "X", "Y" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func "f" :::"*":::  ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" "X"  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "(" "Y"  ($#k3_finseq_2 :::"*"::: )  ")" ) means :: LANG1:def 13 (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "X"  ($#k3_finseq_2 :::"*"::: )  ) "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k11_lang1 :::"*"::: )  (Set (Var "p"))))); end; 







:: deftheorem    defines :::"*"::: LANG1:def 13 :  (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "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 "X")) "," (Set (Var "Y"))  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set (Var "X"))  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "(" (Set (Var "Y"))  ($#k3_finseq_2 :::"*"::: )  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k12_lang1 :::"*"::: )  )) "iff" (Bool  "for" (Set (Var "p")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "X"))  ($#k3_finseq_2 :::"*"::: )  ) "holds"  (Bool (Set (Set (Var "b4"))  ($#k3_funct_2 :::"."::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k11_lang1 :::"*"::: )  (Set (Var "p")))))  ")" )))); 
 







theorem :: LANG1:18 (Bool  "for" (Set (Var "R")) "being"   ($#m1_hidden :::"Relation":::) "holds"  (Bool (Set (Var "R"))  ($#r1_tarski :::"c="::: )  (Set (Set (Var "R"))  ($#k18_finseq_1 :::"[*]"::: )  ))) ; 
 definitionlet "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "R" be   ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); :: original: :::"[*]"::: redefine func "R" :::"[*]":::  ->   ($#m1_subset_1 :::"Relation":::) "of" "X"; end; definitionlet "G" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )  ; let "X" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Const "G"))) "," (Set (Const "X")); func "G" :::"."::: "f" ->   ($#v2_lang1 :::"strict"::: )     ($#l2_lang1 :::"GrammarStr"::: )   equals :: LANG1:def 14 (Set   ($#g2_lang1 :::"GrammarStr"::: )  "(#"  "X" "," (Set  "(" "f"  ($#k3_funct_2 :::"."::: )  (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" "G") ")" ) "," (Set  "(" (Set  "(" (Set  "(" "f"  ($#k3_relset_1 :::"~"::: )  ")" )  ($#k4_relset_1 :::"*"::: )  (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" "G") ")" )  ($#k4_relset_1 :::"*"::: )  (Set  "(" "f"  ($#k12_lang1 :::"*"::: )  ")" ) ")" ) "#)" ); end; 







:: deftheorem    defines :::"."::: LANG1:def 14 :  (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l2_lang1 :::"GrammarStr"::: )    (Bool  "for" (Set (Var "X")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G"))) "," (Set (Var "X")) "holds"  (Bool (Set (Set (Var "G"))  ($#k14_lang1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#g2_lang1 :::"GrammarStr"::: )  "(#"  (Set (Var "X")) "," (Set  "(" (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set  "the"  ($#u2_lang1 :::"InitialSym"::: )  "of" (Set (Var "G"))) ")" ) "," (Set  "(" (Set  "(" (Set  "(" (Set (Var "f"))  ($#k3_relset_1 :::"~"::: )  ")" )  ($#k4_relset_1 :::"*"::: )  (Set  "the"  ($#u1_lang1 :::"Rules"::: )  "of" (Set (Var "G"))) ")" )  ($#k4_relset_1 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k12_lang1 :::"*"::: )  ")" ) ")" ) "#)" )))));