:: FOMODEL3 semantic presentation begin definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "V" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Const "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ); func "s" :::"-compound"::: "V" -> ($#m2_subset_1 :::"string":::) "of" "S" equals :: FOMODEL3:def 1 (Set (Set ($#k31_fomodel2 :::"<*"::: ) "s" ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "V" ")" )); end; :: deftheorem defines :::"-compound"::: FOMODEL3:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "V")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "s")) ($#k1_fomodel3 :::"-compound"::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_fomodel2 :::"<*"::: ) (Set (Var "s")) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "V")) ")" )))))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "mm" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "s" be ($#v8_fomodel1 :::"termal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "V" be (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Const "s")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set (Const "S")) ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Const "mm")) ")" ) ($#k2_fomodel0 :::"*"::: ) ); cluster (Set "s" ($#k1_fomodel3 :::"-compound"::: ) "V") -> (Set "mm" ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#v14_fomodel1 :::"-termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v8_fomodel1 :::"termal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "V" be (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Const "s")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ); cluster (Set "s" ($#k1_fomodel3 :::"-compound"::: ) "V") -> ($#v13_fomodel1 :::"termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "V" be (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Const "s")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ); cluster (Set "s" ($#k1_fomodel3 :::"-compound"::: ) "V") -> ($#v15_fomodel1 :::"0wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func "s" :::"-compound"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) means :: FOMODEL3:def 2 (Bool "for" (Set (Var "V")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_fomodel3 :::"-compound"::: ) (Set (Var "V"))))); end; :: deftheorem defines :::"-compound"::: FOMODEL3:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_fomodel3 :::"-compound"::: ) )) "iff" (Bool "for" (Set (Var "V")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "V"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_fomodel3 :::"-compound"::: ) (Set (Var "V"))))) ")" )))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v8_fomodel1 :::"termal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set (Set "(" "s" ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ")" )) -> (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set (Set "(" "s" ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ")" )) -> (Set ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "X" be ($#m1_hidden :::"set"::: ) ; func "X" :::"-freeInterpreter"::: "s" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL3:def 3 (Set (Set "(" "s" ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ")" )) if (Bool (Bool "not" "s" "is" ($#v7_fomodel1 :::"relational"::: ) )) otherwise (Set (Set "(" (Set "(" "s" ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_fomodel0 :::"chi"::: ) "(" "X" "," (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) "S" ")" ) ")" ")" )); end; :: deftheorem defines :::"-freeInterpreter"::: FOMODEL3:def 3 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "s")) "being" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) ))) "implies" (Bool (Set (Set (Var "X")) ($#k3_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) )) "implies" (Bool (Set (Set (Var "X")) ($#k3_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_fomodel3 :::"-compound"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k9_fomodel0 :::"chi"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ")" ))) ")" ")" )))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"-freeInterpreter"::: redefine func "X" :::"-freeInterpreter"::: "s" -> ($#m2_fomodel2 :::"Interpreter"::: ) "of" "s" "," (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S"); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; func "(" "S" "," "X" ")" :::"-freeInterpreter"::: -> ($#m1_hidden :::"Function":::) means :: FOMODEL3:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S")) & (Bool "(" "for" (Set (Var "s")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set "X" ($#k4_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "s")))) ")" ) ")" ); end; :: deftheorem defines :::"-freeInterpreter"::: FOMODEL3:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "S")) "," (Set (Var "X")) ")" ($#k5_fomodel3 :::"-freeInterpreter"::: ) )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "s")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k4_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "s")))) ")" ) ")" ) ")" )))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "S" "," "X" ")" ($#k5_fomodel3 :::"-freeInterpreter"::: ) ) -> ($#v1_funcop_1 :::"Function-yielding"::: ) for ($#m1_hidden :::"Function":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"-freeInterpreter"::: redefine func "(" "S" "," "X" ")" :::"-freeInterpreter"::: -> ($#m3_fomodel2 :::"Interpreter"::: ) "of" "S" "," (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "S" "," "X" ")" ($#k5_fomodel3 :::"-freeInterpreter"::: ) ) -> "S" "," (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S") ($#v1_fomodel2 :::"-interpreter-like"::: ) for ($#m1_hidden :::"Function":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"-freeInterpreter"::: redefine func "(" "S" "," "X" ")" :::"-freeInterpreter"::: -> ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k16_fomodel2 :::"-InterpretersOf"::: ) "S"); end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "n" be ($#m1_hidden :::"Nat":::); func "n" :::"-placesOf"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "Y" ")" ) equals :: FOMODEL3:def 5 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) where p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X"), q "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "Y") : (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) "n"))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R")) "}" ; end; :: deftheorem defines :::"-placesOf"::: FOMODEL3:def 5 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k8_fomodel3 :::"-placesOf"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) where p "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "X"))), q "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set (Var "n")) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set (Var "Y"))) : (Bool "for" (Set (Var "j")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) "," (Set "(" (Set (Var "q")) ($#k1_funct_1 :::"."::: ) (Set (Var "j")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R")))) "}" )))); registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k8_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "Y" ")" ); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k8_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "Y" ")" ); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "n" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k8_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) "," (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "Y" ")" ); end; 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")); let "n" be ($#m1_hidden :::"Nat":::); func "n" :::"-placesOf"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) equals :: FOMODEL3:def 6 (Set "n" ($#k8_fomodel3 :::"-placesOf"::: ) "R"); end; :: deftheorem defines :::"-placesOf"::: FOMODEL3:def 6 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k9_fomodel3 :::"-placesOf"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k8_fomodel3 :::"-placesOf"::: ) (Set (Var "R"))))))); 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")); let "n" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"Nat":::); :: original: :::"-placesOf"::: redefine func "n" :::"-placesOf"::: "R" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ) equals :: FOMODEL3:def 7 (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ); end; :: deftheorem defines :::"-placesOf"::: FOMODEL3:def 7 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "n")) "being" ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "n")) ($#k10_fomodel3 :::"-placesOf"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k9_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k9_fomodel3 :::"-placesOf"::: ) "R") -> ($#v3_relat_2 :::"symmetric"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k9_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v1_partfun1 :::"total"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k9_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); cluster (Set "n" ($#k9_fomodel3 :::"-placesOf"::: ) "R") -> ($#v1_partfun1 :::"total"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); let "R" be ($#m1_hidden :::"Relation":::); func "R" :::"quotient"::: "(" "E" "," "F" ")" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL3:def 8 "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where e "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "E"), f "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "F") : (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "e"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "R") ")" )) "}" ; end; :: deftheorem defines :::"quotient"::: FOMODEL3:def 8 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool (Set (Set (Var "R")) ($#k11_fomodel3 :::"quotient"::: ) "(" (Set (Var "E")) "," (Set (Var "F")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set ($#k1_domain_1 :::"["::: ) (Set (Var "e")) "," (Set (Var "f")) ($#k1_domain_1 :::"]"::: ) ) where e "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E"))), f "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "F"))) : (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "e"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "R"))) ")" )) "}" ))))); definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); let "R" be ($#m1_hidden :::"Relation":::); :: original: :::"quotient"::: redefine func "R" :::"quotient"::: "(" "E" "," "F" ")" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "F" ")" ); end; definitionlet "E", "F" be ($#m1_hidden :::"Relation":::); let "f" be ($#m1_hidden :::"Function":::); attr "f" is "E" "," "F" :::"-respecting"::: means :: FOMODEL3:def 9 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "E")) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) "F")); end; :: deftheorem defines :::"-respecting"::: FOMODEL3:def 9 : (Bool "for" (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Relation":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "E")) "," (Set (Var "F")) ($#v1_fomodel3 :::"-respecting"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "E")))) "holds" (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "F")))) ")" ))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "U")); let "f" be ($#m2_fomodel2 :::"Interpreter"::: ) "of" (Set (Const "s")) "," (Set (Const "U")); attr "f" is "E" :::"-respecting"::: means :: FOMODEL3:def 10 (Bool "f" "is" (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) "E") "," "E" ($#v1_fomodel3 :::"-respecting"::: ) ) if (Bool (Bool "not" "s" "is" ($#v7_fomodel1 :::"relational"::: ) )) otherwise (Bool "f" "is" (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) "E") "," (Set ($#k3_fomodel2 :::"id"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ($#v1_fomodel3 :::"-respecting"::: ) ); end; :: deftheorem defines :::"-respecting"::: FOMODEL3:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "f")) "being" ($#m2_fomodel2 :::"Interpreter"::: ) "of" (Set (Var "s")) "," (Set (Var "U")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "E")) ($#v2_fomodel3 :::"-respecting"::: ) ) "iff" (Bool (Set (Var "f")) "is" (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) (Set (Var "E"))) "," (Set (Var "E")) ($#v1_fomodel3 :::"-respecting"::: ) ) ")" ) ")" & "(" (Bool (Bool (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) )) "implies" (Bool "(" (Bool (Set (Var "f")) "is" (Set (Var "E")) ($#v2_fomodel3 :::"-respecting"::: ) ) "iff" (Bool (Set (Var "f")) "is" (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) (Set (Var "E"))) "," (Set ($#k3_fomodel2 :::"id"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ($#v1_fomodel3 :::"-respecting"::: ) ) ")" ) ")" ")" )))))); registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) "E" "," "F" ($#v1_fomodel3 :::"-respecting"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k4_finseq_2 :::"-tuples_on"::: ) "U") ($#v4_relat_1 :::"-defined"::: ) (Set "U" ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) "E" ($#v2_fomodel3 :::"-respecting"::: ) for ($#m1_fomodel2 :::"Interpreter"::: ) "of" "s" "," "U"; end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) "E" "," "F" ($#v1_fomodel3 :::"-respecting"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "n" be ($#m1_hidden :::"Nat":::); :: original: :::"-placesOf"::: redefine func "n" :::"-placesOf"::: "E" -> ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) "X" ")" ); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Const "X"))); func :::"DeTrivial"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" "X" means :: FOMODEL3:def 11 (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) it ($#k6_domain_1 :::"}"::: ) )); end; :: deftheorem defines :::"DeTrivial"::: FOMODEL3:def 11 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_eqrel_1 :::"SmallestPartition"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k14_fomodel3 :::"DeTrivial"::: ) (Set (Var "x")))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "b3")) ($#k6_domain_1 :::"}"::: ) )) ")" )))); definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"peeler"::: "X" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k10_eqrel_1 :::"{_{"::: ) "X" ($#k10_eqrel_1 :::"}_}"::: ) ) "," "X" means :: FOMODEL3:def 12 (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_eqrel_1 :::"{_{"::: ) "X" ($#k10_eqrel_1 :::"}_}"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k14_fomodel3 :::"DeTrivial"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"peeler"::: FOMODEL3:def 12 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_fomodel3 :::"peeler"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k10_eqrel_1 :::"{_{"::: ) (Set (Var "X")) ($#k10_eqrel_1 :::"}_}"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k14_fomodel3 :::"DeTrivial"::: ) (Set (Var "x"))))) ")" ))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "EqR" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) "EqR"); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); let "f" be (Set (Const "E")) "," (Set (Const "F")) ($#v1_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k11_fomodel3 :::"quotient"::: ) "(" "E" "," "F" ")" ) -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); let "R" be ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "R" ($#k11_fomodel3 :::"quotient"::: ) "(" "E" "," "F" ")" ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "F" ")" ); end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); let "F" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "Y")); let "f" be (Set (Const "E")) "," (Set (Const "F")) ($#v1_fomodel3 :::"-respecting"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"quotient"::: redefine func "f" :::"quotient"::: "(" "E" "," "F" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "F" ")" ); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); func "E" :::"-class"::: -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) means :: FOMODEL3:def 13 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_eqrel_1 :::"EqClass"::: ) "(" "E" "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"-class"::: FOMODEL3:def 13 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "E")) ($#k17_fomodel3 :::"-class"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_eqrel_1 :::"EqClass"::: ) "(" (Set (Var "E")) "," (Set (Var "x")) ")" ))) ")" )))); registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "X")); cluster (Set "E" ($#k17_fomodel3 :::"-class"::: ) ) -> ($#v2_funct_2 :::"onto"::: ) for ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_2 :::"onto"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_2 :::"onto"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_relat_1 :::"~"::: ) ) -> "Y" ($#v4_relat_1 :::"-defined"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_2 :::"onto"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_relat_1 :::"~"::: ) ) -> "Y" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"Y" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); end; registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be ($#v2_funct_2 :::"onto"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "R" ($#k2_relat_1 :::"~"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" "Y" "," "X"; end; registrationlet "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "R" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#v2_funct_2 :::"onto"::: ) ($#m1_hidden :::"Relation":::); cluster (Set "R" ($#k2_relat_1 :::"~"::: ) ) -> "Y" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"Y" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); func "n" :::"-tuple2Class"::: "E" -> ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" "n" ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) ")" ) equals :: FOMODEL3:def 14 (Set (Set "(" "n" ($#k8_fomodel3 :::"-placesOf"::: ) (Set "(" (Set "(" "E" ($#k17_fomodel3 :::"-class"::: ) ")" ) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set "(" "n" ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) ($#k17_fomodel3 :::"-class"::: ) ")" )); end; :: deftheorem defines :::"-tuple2Class"::: FOMODEL3:def 14 : (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) "holds" (Bool (Set (Set (Var "n")) ($#k18_fomodel3 :::"-tuple2Class"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "n")) ($#k8_fomodel3 :::"-placesOf"::: ) (Set "(" (Set "(" (Set (Var "E")) ($#k17_fomodel3 :::"-class"::: ) ")" ) ($#k3_relset_1 :::"~"::: ) ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k13_fomodel3 :::"-placesOf"::: ) (Set (Var "E")) ")" ) ($#k17_fomodel3 :::"-class"::: ) ")" )))))); registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster (Set "n" ($#k18_fomodel3 :::"-tuple2Class"::: ) "E") -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" "n" ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) ")" ); end; registrationlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster (Set "n" ($#k18_fomodel3 :::"-tuple2Class"::: ) "E") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Relation":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" "n" ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) ")" ); end; definitionlet "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); :: original: :::"-tuple2Class"::: redefine func "n" :::"-tuple2Class"::: "E" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" "n" ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) ")" ) "," (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set "(" "n" ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "f" be ($#m2_fomodel2 :::"Interpreter"::: ) "of" (Set (Const "s")) "," (Set (Const "U")); func "f" :::"quotient"::: "E" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL3:def 15 (Set (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k19_fomodel3 :::"-tuple2Class"::: ) "E" ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" "f" ($#k12_fomodel3 :::"quotient"::: ) "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) "," "E" ")" ")" )) if (Bool (Bool "not" "s" "is" ($#v7_fomodel1 :::"relational"::: ) )) otherwise (Set (Set "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k19_fomodel3 :::"-tuple2Class"::: ) "E" ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" "f" ($#k12_fomodel3 :::"quotient"::: ) "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" ) ")" ) ($#k13_fomodel3 :::"-placesOf"::: ) "E" ")" ) "," (Set "(" ($#k3_fomodel2 :::"id"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ")" ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k15_fomodel3 :::"peeler"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" )); end; :: deftheorem defines :::"quotient"::: FOMODEL3:def 15 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "f")) "being" ($#m2_fomodel2 :::"Interpreter"::: ) "of" (Set (Var "s")) "," (Set (Var "U")) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) ))) "implies" (Bool (Set (Set (Var "f")) ($#k20_fomodel3 :::"quotient"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k19_fomodel3 :::"-tuple2Class"::: ) (Set (Var "E")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_fomodel3 :::"quotient"::: ) "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k13_fomodel3 :::"-placesOf"::: ) (Set (Var "E")) ")" ) "," (Set (Var "E")) ")" ")" ))) ")" & "(" (Bool (Bool (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) )) "implies" (Bool (Set (Set (Var "f")) ($#k20_fomodel3 :::"quotient"::: ) (Set (Var "E"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k19_fomodel3 :::"-tuple2Class"::: ) (Set (Var "E")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k12_fomodel3 :::"quotient"::: ) "(" (Set "(" (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" ) ")" ) ($#k13_fomodel3 :::"-placesOf"::: ) (Set (Var "E")) ")" ) "," (Set "(" ($#k3_fomodel2 :::"id"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ) ")" ")" ) ")" ) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k15_fomodel3 :::"peeler"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) ) ")" ))) ")" ")" )))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "f" be (Set (Const "E")) ($#v2_fomodel3 :::"-respecting"::: ) ($#m2_fomodel2 :::"Interpreter"::: ) "of" (Set (Const "s")) "," (Set (Const "U")); :: original: :::"quotient"::: redefine func "f" :::"quotient"::: "E" -> ($#m2_fomodel2 :::"Interpreter"::: ) "of" "s" "," (Set ($#k8_eqrel_1 :::"Class"::: ) "E"); end; theorem :: FOMODEL3:1 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "E"))) "st" (Bool (Bool (Set (Var "C1")) ($#r2_subset_1 :::"meets"::: ) (Set (Var "C2")))) "holds" (Bool (Set (Var "C1")) ($#r1_hidden :::"="::: ) (Set (Var "C2")))))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#v9_fomodel1 :::"own"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S"); cluster -> ($#v10_fomodel1 :::"ofAtomicFormula"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#~v7_fomodel1 "non" ($#v7_fomodel1 :::"relational"::: ) ) ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "U")); cluster "E" ($#v2_fomodel3 :::"-respecting"::: ) -> (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "o" ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) "E") "," "E" ($#v1_fomodel3 :::"-respecting"::: ) for ($#m1_fomodel2 :::"Interpreter"::: ) "of" "o" "," "U"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "r" be ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "E" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "U")); cluster "E" ($#v2_fomodel3 :::"-respecting"::: ) -> (Set (Set "(" ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "r" ")" ) ")" ) ($#k9_fomodel3 :::"-placesOf"::: ) "E") "," (Set ($#k3_fomodel2 :::"id"::: ) (Set ($#k6_margrel1 :::"BOOLEAN"::: ) )) ($#v1_fomodel3 :::"-respecting"::: ) for ($#m1_fomodel2 :::"Interpreter"::: ) "of" "r" "," "U"; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "U1", "U2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_funct_1 :::"Function-like"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); cluster (Set "n" ($#k8_fomodel3 :::"-placesOf"::: ) "f") -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "U1", "U2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "n" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"Nat":::); let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); cluster (Set (Set "(" "n" ($#k8_fomodel3 :::"-placesOf"::: ) "R" ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k3_fomodel2 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k3_xboole_0 :::"/\"::: ) "Y") -> ($#v4_funct_1 :::"functional"::: ) ; end; theorem :: FOMODEL3:2 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "V")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) (Bool "ex" (Set (Var "mm")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "V")) "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set (Var "S")) ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "mm")) ")" ) ($#k2_fomodel0 :::"*"::: ) ))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::); attr "I" is "E" :::"-respecting"::: means :: FOMODEL3:def 16 (Bool "for" (Set (Var "s")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set "I" ($#k4_fomodel2 :::"."::: ) (Set (Var "s"))) "is" "E" ($#v2_fomodel3 :::"-respecting"::: ) )); end; :: deftheorem defines :::"-respecting"::: FOMODEL3:def 16 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b1")) "," (Set (Var "b2")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "I")) "is" (Set (Var "E")) ($#v3_fomodel3 :::"-respecting"::: ) ) "iff" (Bool "for" (Set (Var "s")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "I")) ($#k4_fomodel2 :::"."::: ) (Set (Var "s"))) "is" (Set (Var "E")) ($#v2_fomodel3 :::"-respecting"::: ) )) ")" ))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::); func "I" :::"quotient"::: "E" -> ($#m1_hidden :::"Function":::) means :: FOMODEL3:def 17 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S")) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S") "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "I" ($#k4_fomodel2 :::"."::: ) (Set (Var "o")) ")" ) ($#k20_fomodel3 :::"quotient"::: ) "E")) ")" ) ")" ); end; :: deftheorem defines :::"quotient"::: FOMODEL3:def 17 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b1")) "," (Set (Var "b2")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k22_fomodel3 :::"quotient"::: ) (Set (Var "E")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k4_fomodel2 :::"."::: ) (Set (Var "o")) ")" ) ($#k20_fomodel3 :::"quotient"::: ) (Set (Var "E")))) ")" ) ")" ) ")" )))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::); redefine func "I" :::"quotient"::: "E" means :: FOMODEL3:def 18 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S")) & (Bool "(" "for" (Set (Var "o")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "I" ($#k4_fomodel2 :::"."::: ) (Set (Var "o")) ")" ) ($#k20_fomodel3 :::"quotient"::: ) "E")) ")" ) ")" ); end; :: deftheorem defines :::"quotient"::: FOMODEL3:def 18 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b1")) "," (Set (Var "b2")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "I")) ($#k22_fomodel3 :::"quotient"::: ) (Set (Var "E")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "o")) "being" ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I")) ($#k4_fomodel2 :::"."::: ) (Set (Var "o")) ")" ) ($#k20_fomodel3 :::"quotient"::: ) (Set (Var "E")))) ")" ) ")" ) ")" )))))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::); let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster (Set "I" ($#k22_fomodel3 :::"quotient"::: ) "E") -> (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S") ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S") ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() "S" "," "U" ($#v1_fomodel2 :::"-interpreter-like"::: ) "E" ($#v3_fomodel3 :::"-respecting"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "U" ($#k16_fomodel2 :::"-InterpretersOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funcop_1 :::"Function-yielding"::: ) bbbadV2_FUNCOP_1() "S" "," "U" ($#v1_fomodel2 :::"-interpreter-like"::: ) "E" ($#v3_fomodel3 :::"-respecting"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "o" be ($#v9_fomodel1 :::"own"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) (Set (Const "E")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::); cluster (Set "I" ($#k1_funct_1 :::"."::: ) "o") -> "E" ($#v2_fomodel3 :::"-respecting"::: ) for ($#m2_fomodel2 :::"Interpreter"::: ) "of" "o" "," "U"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) (Set (Const "E")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::); cluster (Set "I" ($#k22_fomodel3 :::"quotient"::: ) "E") -> "S" "," (Set ($#k8_eqrel_1 :::"Class"::: ) "E") ($#v1_fomodel2 :::"-interpreter-like"::: ) for ($#m1_hidden :::"Function":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "U" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "U")); let "I" be (Set (Const "S")) "," (Set (Const "U")) ($#v1_fomodel2 :::"-interpreter-like"::: ) (Set (Const "E")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::); :: original: :::"quotient"::: redefine func "I" :::"quotient"::: "E" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "E" ")" ) ($#k16_fomodel2 :::"-InterpretersOf"::: ) "S"); end; theorem :: FOMODEL3:3 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b2")) "," (Set (Var "b1")) ($#v1_fomodel2 :::"-interpreter-like"::: ) (Set (Var "b3")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "I")) ($#k23_fomodel3 :::"quotient"::: ) (Set (Var "E")) ")" ) ($#k10_fomodel2 :::"-TermEval"::: ) ) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "E")) ($#k17_fomodel3 :::"-class"::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ))))))) ; theorem :: FOMODEL3:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" "(" (Set (Var "S")) "," (Set (Var "X")) ")" ($#k7_fomodel3 :::"-freeInterpreter"::: ) ")" ) ($#k10_fomodel2 :::"-TermEval"::: ) ) ($#r2_funct_2 :::"="::: ) (Set ($#k3_fomodel2 :::"id"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ))))) ; theorem :: FOMODEL3:5 (Bool "for" (Set (Var "U1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U1")) (Bool "for" (Set (Var "phi")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" (Set (Var "b2")) "," (Set (Var "b1")) ($#v1_fomodel2 :::"-interpreter-like"::: ) (Set (Var "b3")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi"))) ($#r1_hidden :::"<>"::: ) (Set ($#k34_fomodel2 :::"TheEqSymbOf"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Set "(" (Set (Var "i")) ($#k23_fomodel3 :::"quotient"::: ) (Set (Var "R")) ")" ) ($#k14_fomodel2 :::"-AtomicEval"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k14_fomodel2 :::"-AtomicEval"::: ) (Set (Var "phi"))))))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "x" be ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "w" be ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"-SymbolSubstIn"::: redefine func "(" "x" "," "s" ")" :::"-SymbolSubstIn"::: "w" -> ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "m" be ($#m1_hidden :::"Nat":::); let "t" be (Set (Const "m")) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l1" "," "l2" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "t") -> "m" ($#v14_fomodel1 :::"-termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set "(" "l1" "," "l2" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "t") -> ($#v13_fomodel1 :::"termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "phi" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l1" "," "l2" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "phi") -> ($#v15_fomodel1 :::"0wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m0" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"number"::: ) ; let "phi" be (Set (Const "m0")) ($#v3_fomodel2 :::"-wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k32_fomodel2 :::"Depth"::: ) "phi") -> ($#v1_xboole_0 :::"zero"::: ) for ($#m1_hidden :::"number"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); let "w" be ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"null"::: redefine func "w" :::"null"::: "m" -> ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "m" be ($#m1_hidden :::"Nat":::); cluster (Set "phi" ($#k13_fomodel0 :::"null"::: ) "m") -> (Set (Set "(" ($#k32_fomodel2 :::"Depth"::: ) "phi" ")" ) ($#k2_xcmplx_0 :::"+"::: ) "m") ($#v3_fomodel2 :::"-wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); let "phi" be (Set (Const "m")) ($#v3_fomodel2 :::"-wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "m" ($#k6_xcmplx_0 :::"-"::: ) (Set "(" ($#k32_fomodel2 :::"Depth"::: ) "phi" ")" )) -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) for ($#v1_xxreal_0 :::"ext-real"::: ) ($#m1_hidden :::"number"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "m" be ($#m1_hidden :::"Nat":::); let "phi" be (Set (Const "m")) ($#v3_fomodel2 :::"-wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l1" "," "l2" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "phi") -> "m" ($#v3_fomodel2 :::"-wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l1" "," "l2" ")" ($#k17_fomodel0 :::"-SymbolSubstIn"::: ) "phi") -> ($#v4_fomodel2 :::"wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set (Set "(" ($#k32_fomodel2 :::"Depth"::: ) (Set "(" "(" "l1" "," "l2" ")" ($#k24_fomodel3 :::"-SymbolSubstIn"::: ) "phi" ")" ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" ($#k32_fomodel2 :::"Depth"::: ) "phi" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL3:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "a")) "being" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "T")) "being" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "b3")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Bool "not" (Set (Var "a")) "is" ($#v7_fomodel1 :::"relational"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "a")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k1_fomodel3 :::"-compound"::: ) (Set (Var "T")))) ")" & "(" (Bool (Bool (Set (Var "a")) "is" ($#v7_fomodel1 :::"relational"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "X")) ($#k4_fomodel3 :::"-freeInterpreter"::: ) (Set (Var "a")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "T"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_fomodel0 :::"chi"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "a")) ($#k1_fomodel3 :::"-compound"::: ) (Set (Var "T")) ")" ))) ")" ")" ))))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#v13_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ($#v2_finseq_1 :::"FinSubsequence-like"::: ) ($#v2_pre_poly :::"finite-support"::: ) ($#v15_fomodel1 :::"0wff"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )); end; theorem :: FOMODEL3:7 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b4")) "," (Set (Var "b2")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "tt0")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set "(" "(" (Set "(" "(" (Set (Var "l")) "," (Set (Var "tt0")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set "(" "(" (Set (Var "S")) "," (Set (Var "X")) ")" ($#k7_fomodel3 :::"-freeInterpreter"::: ) ")" ) ")" ) "," (Set (Var "tt0")) ")" ($#k8_fomodel2 :::"-TermEval"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set "(" "(" (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tt0")) ")" ) ")" ($#k5_fomodel2 :::"ReassignIn"::: ) (Set (Var "I")) ")" ) "," (Set "(" (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tt0")) ")" ) ")" ($#k8_fomodel2 :::"-TermEval"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "n")) ")" )))))))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "tt" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S"))); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func "(" "l" "," "tt" ")" :::"AtomicSubst"::: "phi0" -> ($#m1_hidden :::"FinSequence":::) equals :: FOMODEL3:def 19 (Set (Set ($#k31_fomodel2 :::"<*"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi0" ")" ) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" "(" "l" "," "tt" ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set "(" "(" "S" "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ($#k7_fomodel3 :::"-freeInterpreter"::: ) ")" ) ")" ) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k34_fomodel1 :::"SubTerms"::: ) "phi0" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"AtomicSubst"::: FOMODEL3:def 19 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "tt")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) (Bool "for" (Set (Var "phi0")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool (Set "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k26_fomodel3 :::"AtomicSubst"::: ) (Set (Var "phi0"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_fomodel2 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi0")) ")" ) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set "(" "(" (Set (Var "S")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ($#k7_fomodel3 :::"-freeInterpreter"::: ) ")" ) ")" ) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k34_fomodel1 :::"SubTerms"::: ) (Set (Var "phi0")) ")" ) ")" ) ")" ))))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "tt" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S"))); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"AtomicSubst"::: redefine func "(" "l" "," "tt" ")" :::"AtomicSubst"::: "phi0" -> ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "tt" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S"))); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l" "," "tt" ")" ($#k26_fomodel3 :::"AtomicSubst"::: ) "phi0") -> ($#v15_fomodel1 :::"0wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; theorem :: FOMODEL3:8 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "phi0")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" (Set (Var "b2")) "," (Set (Var "b1")) ($#v1_fomodel2 :::"-interpreter-like"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "tt")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set (Var "I")) ($#k14_fomodel2 :::"-AtomicEval"::: ) (Set "(" "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k27_fomodel3 :::"AtomicSubst"::: ) (Set (Var "phi0")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tt")) ")" ) ")" ($#k5_fomodel2 :::"ReassignIn"::: ) (Set (Var "I")) ")" ) ($#k14_fomodel2 :::"-AtomicEval"::: ) (Set (Var "phi0")))))))))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "m" be ($#m1_hidden :::"Nat":::); cluster (Set (Set "(" "l1" ($#k20_fomodel0 :::"SubstWith"::: ) "l2" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" "S" ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) "m" ")" )) -> (Set (Set "(" "S" ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k8_nat_1 :::"."::: ) "m") ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l1", "l2" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set (Set "(" "l1" ($#k20_fomodel0 :::"SubstWith"::: ) "l2" ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" )) -> (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; theorem :: FOMODEL3:9 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l2")) "," (Set (Var "l1")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "psi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "l2")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "psi")))))) "holds" (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set "(" "(" (Set (Var "l1")) "," (Set (Var "u1")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set (Var "I")) ")" ) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "psi"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "l2")) "," (Set (Var "u1")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set (Var "I")) ")" ) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set "(" "(" (Set (Var "l1")) "," (Set (Var "l2")) ")" ($#k24_fomodel3 :::"-SymbolSubstIn"::: ) (Set (Var "psi")) ")" ))))))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func "(" "l" "," "t" "," "n" "," "f" ")" :::"Subst2"::: "phi" -> ($#m1_hidden :::"FinSequence":::) equals :: FOMODEL3:def 20 (Set (Set "(" (Set ($#k31_fomodel2 :::"<*"::: ) (Set "(" ($#k1_fomodel2 :::"TheNorSymbOf"::: ) "S" ")" ) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) "phi" ")" ) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k41_fomodel2 :::"tail"::: ) "phi" ")" ) ")" )) if (Bool "(" (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) "phi") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Bool "not" "phi" "is" ($#v5_fomodel2 :::"exal"::: ) )) ")" ) (Set (Set ($#k31_fomodel2 :::"<*"::: ) "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) "S" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "t" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) "phi" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) "l" ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set "(" "(" (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi" ")" ) "," "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) "S" ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "t" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) "phi" ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) "l" ($#k6_domain_1 :::"}"::: ) ) ")" )) ")" ($#k24_fomodel3 :::"-SymbolSubstIn"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) "phi" ")" ) ")" ) ")" )) if (Bool "(" (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) "phi") ($#r1_hidden :::"="::: ) (Set "n" ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool "phi" "is" ($#v5_fomodel2 :::"exal"::: ) ) & (Bool (Set (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi") ($#r1_hidden :::"<>"::: ) "l") ")" ) otherwise (Set "f" ($#k1_funct_1 :::"."::: ) "phi"); end; :: deftheorem defines :::"Subst2"::: FOMODEL3:def 20 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#v1_pre_poly :::"FinSequence-yielding"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "phi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Bool "not" (Set (Var "phi")) "is" ($#v5_fomodel2 :::"exal"::: ) ))) "implies" (Bool (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "n")) "," (Set (Var "f")) ")" ($#k28_fomodel3 :::"Subst2"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k31_fomodel2 :::"<*"::: ) (Set "(" ($#k1_fomodel2 :::"TheNorSymbOf"::: ) (Set (Var "S")) ")" ) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) (Set (Var "phi")) ")" ) ")" ) ")" ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k41_fomodel2 :::"tail"::: ) (Set (Var "phi")) ")" ) ")" ))) ")" & "(" (Bool (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) & (Bool (Set (Var "phi")) "is" ($#v5_fomodel2 :::"exal"::: ) ) & (Bool (Set (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi"))) ($#r1_hidden :::"<>"::: ) (Set (Var "l")))) "implies" (Bool (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "n")) "," (Set (Var "f")) ")" ($#k28_fomodel3 :::"Subst2"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k31_fomodel2 :::"<*"::: ) "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) (Set (Var "S")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) (Set (Var "phi")) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "l")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ($#k31_fomodel2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" "(" (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi")) ")" ) "," "the" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) (Set (Var "S")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "t")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) (Set (Var "phi")) ")" ) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "l")) ($#k6_domain_1 :::"}"::: ) ) ")" )) ")" ($#k24_fomodel3 :::"-SymbolSubstIn"::: ) (Set "(" ($#k40_fomodel2 :::"head"::: ) (Set (Var "phi")) ")" ) ")" ) ")" ))) ")" & "(" (Bool (Bool "(" "not" (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" (Bool (Set (Var "phi")) "is" ($#v5_fomodel2 :::"exal"::: ) ) ")" ) & (Bool "(" "not" (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1))) "or" "not" (Bool (Set (Var "phi")) "is" ($#v5_fomodel2 :::"exal"::: ) ) "or" "not" (Bool (Set (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi"))) ($#r1_hidden :::"<>"::: ) (Set (Var "l"))) ")" )) "implies" (Bool (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "n")) "," (Set (Var "f")) ")" ($#k28_fomodel3 :::"Subst2"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "phi")))) ")" ")" ))))))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) ")" ); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"Subst2"::: redefine func "(" "l" "," "t" "," "n" "," "f" ")" :::"Subst2"::: "phi" -> ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) ")" ); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l" "," "t" "," "n" "," "f" ")" ($#k28_fomodel3 :::"Subst2"::: ) "phi") -> ($#v4_fomodel2 :::"wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "nn" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) ")" ); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"Subst2"::: redefine func "(" "l" "," "t" "," "nn" "," "f" ")" :::"Subst2"::: "phi" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S"); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) ")" ); func "(" "l" "," "t" "," "n" "," "f" ")" :::"Subst3"::: -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) ")" ) means :: FOMODEL3:def 21 (Bool "for" (Set (Var "phi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" "S" "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set "(" "l" "," "t" "," "n" "," "f" ")" ($#k29_fomodel3 :::"Subst2"::: ) (Set (Var "phi"))))); end; :: deftheorem defines :::"Subst3"::: FOMODEL3:def 21 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "b6")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "n")) "," (Set (Var "f")) ")" ($#k31_fomodel3 :::"Subst3"::: ) )) "iff" (Bool "for" (Set (Var "phi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "n")) "," (Set (Var "f")) ")" ($#k29_fomodel3 :::"Subst2"::: ) (Set (Var "phi"))))) ")" )))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "f" be ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Const "S")) ")" ) ")" ); func "(" "l" "," "t" ")" :::"Subst4"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) ")" ")" ) means :: FOMODEL3:def 22 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "f") & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "(" "l" "," "t" "," (Set (Var "m")) "," (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ($#k31_fomodel3 :::"Subst3"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"Subst4"::: FOMODEL3:def 22 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "l")) "," (Set (Var "t")) ")" ($#k32_fomodel3 :::"Subst4"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool "(" "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "l")) "," (Set (Var "t")) "," (Set (Var "m")) "," (Set "(" (Set (Var "b5")) ($#k8_nat_1 :::"."::: ) (Set (Var "m")) ")" ) ")" ($#k31_fomodel3 :::"Subst3"::: ) )) ")" ) ")" ) ")" )))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func "l" :::"AtomicSubst"::: "t" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) "S" ")" ) "," (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) "S" ")" ) means :: FOMODEL3:def 23 (Bool "for" (Set (Var "phi0")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" "S" (Bool "for" (Set (Var "tt")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S") "st" (Bool (Bool (Set (Var "tt")) ($#r1_hidden :::"="::: ) "t")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "phi0"))) ($#r1_hidden :::"="::: ) (Set "(" "l" "," (Set (Var "tt")) ")" ($#k27_fomodel3 :::"AtomicSubst"::: ) (Set (Var "phi0")))))); end; :: deftheorem defines :::"AtomicSubst"::: FOMODEL3:def 23 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) (Set (Var "S")) ")" ) "," (Set "(" ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) (Set (Var "S")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "l")) ($#k33_fomodel3 :::"AtomicSubst"::: ) (Set (Var "t")))) "iff" (Bool "for" (Set (Var "phi0")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "tt")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "st" (Bool (Bool (Set (Var "tt")) ($#r1_hidden :::"="::: ) (Set (Var "t")))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "phi0"))) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k27_fomodel3 :::"AtomicSubst"::: ) (Set (Var "phi0")))))) ")" ))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func "l" :::"Subst1"::: "t" -> ($#m1_hidden :::"Function":::) equals :: FOMODEL3:def 24 (Set (Set "(" ($#k3_fomodel2 :::"id"::: ) (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "l" ($#k33_fomodel3 :::"AtomicSubst"::: ) "t" ")" )); end; :: deftheorem defines :::"Subst1"::: FOMODEL3:def 24 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "l")) ($#k34_fomodel3 :::"Subst1"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_fomodel2 :::"id"::: ) (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) (Set (Var "S")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "l")) ($#k33_fomodel3 :::"AtomicSubst"::: ) (Set (Var "t")) ")" )))))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"Subst1"::: redefine func "l" :::"Subst1"::: "t" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) "," (Set "(" (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); :: original: :::"Subst1"::: redefine func "l" :::"Subst1"::: "t" -> ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) "," (Set "(" ($#k33_fomodel2 :::"AllFormulasOf"::: ) "S" ")" ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func "(" "l" "," "t" ")" :::"SubstIn"::: "phi" -> ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" "S" equals :: FOMODEL3:def 25 (Set (Set "(" (Set "(" "(" "l" "," "t" ")" ($#k32_fomodel3 :::"Subst4"::: ) (Set "(" "l" ($#k36_fomodel3 :::"Subst1"::: ) "t" ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k32_fomodel2 :::"Depth"::: ) "phi" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) "phi"); end; :: deftheorem defines :::"SubstIn"::: FOMODEL3:def 25 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "phi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool (Set "(" (Set (Var "l")) "," (Set (Var "t")) ")" ($#k37_fomodel3 :::"SubstIn"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" "(" (Set (Var "l")) "," (Set (Var "t")) ")" ($#k32_fomodel3 :::"Subst4"::: ) (Set "(" (Set (Var "l")) ($#k36_fomodel3 :::"Subst1"::: ) (Set (Var "t")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "phi")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "phi")))))))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "phi" be ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l" "," "t" ")" ($#k37_fomodel3 :::"SubstIn"::: ) "phi") -> ($#v4_fomodel2 :::"wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "tt" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S"))); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); identify ; identify ; end; theorem :: FOMODEL3:10 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "psi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "tt")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "holds" (Bool "(" (Bool (Set ($#k32_fomodel2 :::"Depth"::: ) (Set "(" "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k37_fomodel3 :::"SubstIn"::: ) (Set (Var "psi")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_fomodel2 :::"Depth"::: ) (Set (Var "psi")))) & (Bool "(" "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set (Var "I")) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set "(" "(" (Set (Var "l")) "," (Set (Var "tt")) ")" ($#k37_fomodel3 :::"SubstIn"::: ) (Set (Var "psi")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "I")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "tt")) ")" ) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set (Var "I")) ")" ) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "psi")))) ")" ) ")" )))))) ; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); let "phi" be (Set (Const "m")) ($#v3_fomodel2 :::"-wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "(" "l" "," "t" ")" ($#k37_fomodel3 :::"SubstIn"::: ) "phi") -> "m" ($#v3_fomodel2 :::"-wff"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; theorem :: FOMODEL3:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "I1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S1"))) (Bool "for" (Set (Var "I2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S2"))) "st" (Bool (Bool (Set (Set (Var "I1")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))) & (Bool (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S1"))) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S2"))) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "I1")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "I2")) ($#k10_fomodel2 :::"-TermEval"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_finseq_2 :::"*"::: ) ")" )))))))) ; theorem :: FOMODEL3:12 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_fomodel1 :::"Language":::) "st" (Bool (Bool (Set ($#k1_fomodel2 :::"TheNorSymbOf"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_fomodel2 :::"TheNorSymbOf"::: ) (Set (Var "S2")))) & (Bool (Set ($#k34_fomodel2 :::"TheEqSymbOf"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k34_fomodel2 :::"TheEqSymbOf"::: ) (Set (Var "S2")))) & (Bool (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S1"))) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S2"))) ($#k2_partfun1 :::"|"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S1")) ")" )))) "holds" (Bool "for" (Set (Var "I1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S1"))) (Bool "for" (Set (Var "I2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S2"))) (Bool "for" (Set (Var "phi1")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S1")) "st" (Bool (Bool (Set (Set (Var "I1")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S1")) ")" )))) "holds" (Bool "ex" (Set (Var "phi2")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S2")) "st" (Bool "(" (Bool (Set (Var "phi2")) ($#r1_hidden :::"="::: ) (Set (Var "phi1"))) & (Bool (Set (Set (Var "I2")) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "phi2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I1")) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "phi1")))) ")" ))))))) ; theorem :: FOMODEL3:13 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "phi")) "being" ($#v4_fomodel2 :::"wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I1")) "," (Set (Var "I2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S"))) "st" (Bool (Bool (Set (Set (Var "I1")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "phi")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "phi")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "I1")) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "phi"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "I2")) ($#k26_fomodel2 :::"-TruthEval"::: ) (Set (Var "phi")))))))) ; theorem :: FOMODEL3:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "I")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S"))) "st" (Bool (Bool (Set (Var "l")) "is" (Set (Var "X")) ($#v7_fomodel2 :::"-absent"::: ) ) & (Bool (Set (Var "X")) "is" (Set (Var "I")) ($#v10_fomodel2 :::"-satisfied"::: ) )) "holds" (Bool (Set (Var "X")) "is" (Set "(" (Set (Var "l")) "," (Set (Var "u")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set (Var "I"))) ($#v10_fomodel2 :::"-satisfied"::: ) ))))))) ; theorem :: FOMODEL3:15 (Bool "for" (Set (Var "U")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "u")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "U")) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "l")) "being" ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "E")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U")) (Bool "for" (Set (Var "i")) "being" (Set (Var "b5")) ($#v3_fomodel3 :::"-respecting"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set (Var "U")) ($#k16_fomodel2 :::"-InterpretersOf"::: ) (Set (Var "S"))) "holds" (Bool (Set "(" (Set (Var "l")) "," (Set "(" (Set "(" (Set (Var "E")) ($#k17_fomodel3 :::"-class"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "u")) ")" ) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set "(" (Set (Var "i")) ($#k23_fomodel3 :::"quotient"::: ) (Set (Var "E")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "l")) "," (Set (Var "u")) ")" ($#k37_fomodel2 :::"ReassignIn"::: ) (Set (Var "i")) ")" ) ($#k22_fomodel3 :::"quotient"::: ) (Set (Var "E")))))))))) ;