:: FOMODEL1 semantic presentation begin registrationlet "z" be ($#v1_xboole_0 :::"zero"::: ) ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK16_COMPLEX1("z")) -> ($#v1_xboole_0 :::"zero"::: ) ($#v1_int_1 :::"integer"::: ) for ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; end; registration cluster ($#v1_xcmplx_0 :::"complex"::: ) ($#v1_xxreal_0 :::"ext-real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#v1_xreal_0 :::"real"::: ) ($#v1_int_1 :::"integer"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_xxreal_0 :::"positive"::: ) ($#v1_int_1 :::"integer"::: ) -> ($#v7_ordinal1 :::"natural"::: ) ($#v1_int_1 :::"integer"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l4_struct_0 :::"ZeroOneStr"::: ) ; cluster (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k4_xboole_0 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "S") ($#k6_domain_1 :::"}"::: ) )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; definitionattr "c1" is :::"strict"::: ; struct :::"Language-like"::: -> ($#l4_struct_0 :::"ZeroOneStr"::: ) ; aggr :::"Language-like":::(# :::"carrier":::, :::"ZeroF":::, :::"OneF":::, :::"adicity"::: #) -> ($#l1_fomodel1 :::"Language-like"::: ) ; sel :::"adicity"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "c1") ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "c1") ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language-like"::: ) ; func :::"AllSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 1 (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S"); func :::"LettersOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 2 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )); func :::"OpSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 3 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )); func :::"RelSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 4 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )); func :::"TermSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 5 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k8_relset_1 :::"""::: ) (Set ($#k5_numbers :::"NAT"::: ) )); func :::"LowerCompoundersOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 6 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )); func :::"TheEqSymbOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 7 (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "S"); func :::"TheNorSymbOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 8 (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "S"); func :::"OwnSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 9 (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k6_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "S") "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "S") ($#k2_tarski :::"}"::: ) )); end; :: deftheorem defines :::"AllSymbolsOf"::: FOMODEL1:def 1 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))))); :: deftheorem defines :::"LettersOf"::: FOMODEL1:def 2 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k2_fomodel1 :::"LettersOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )))); :: deftheorem defines :::"OpSymbolsOf"::: FOMODEL1:def 3 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k5_numbers :::"NAT"::: ) ) ($#k7_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )))); :: deftheorem defines :::"RelSymbolsOf"::: FOMODEL1:def 4 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ")" )))); :: deftheorem defines :::"TermSymbolsOf"::: FOMODEL1:def 5 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k8_relset_1 :::"""::: ) (Set ($#k5_numbers :::"NAT"::: ) )))); :: deftheorem defines :::"LowerCompoundersOf"::: FOMODEL1:def 6 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k8_relset_1 :::"""::: ) (Set "(" (Set ($#k4_numbers :::"INT"::: ) ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ")" )))); :: deftheorem defines :::"TheEqSymbOf"::: FOMODEL1:def 7 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "S"))))); :: deftheorem defines :::"TheNorSymbOf"::: FOMODEL1:def 8 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "S"))))); :: deftheorem defines :::"OwnSymbolsOf"::: FOMODEL1:def 9 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k2_tarski :::"{"::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "S"))) ($#k2_tarski :::"}"::: ) )))); definitionlet "S" be ($#l1_fomodel1 :::"Language-like"::: ) ; mode Element of "S" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); func :::"AtomicFormulaSymbolsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 10 (Set (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k8_fomodel1 :::"TheNorSymbOf"::: ) "S" ")" ) ($#k1_tarski :::"}"::: ) )); func :::"AtomicTermsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 11 (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k2_fomodel1 :::"LettersOf"::: ) "S" ")" )); attr "S" is :::"operational"::: means :: FOMODEL1:def 12 (Bool (Bool "not" (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) "S") "is" ($#v1_xboole_0 :::"empty"::: ) )); attr "S" is :::"relational"::: means :: FOMODEL1:def 13 (Bool (Bool "not" (Set (Set "(" ($#k4_fomodel1 :::"RelSymbolsOf"::: ) "S" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k7_fomodel1 :::"TheEqSymbOf"::: ) "S" ")" ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_xboole_0 :::"empty"::: ) )); end; :: deftheorem defines :::"AtomicFormulaSymbolsOf"::: FOMODEL1:def 10 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k10_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k8_fomodel1 :::"TheNorSymbOf"::: ) (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) )))); :: deftheorem defines :::"AtomicTermsOf"::: FOMODEL1:def 11 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool (Set ($#k11_fomodel1 :::"AtomicTermsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set "(" ($#k2_fomodel1 :::"LettersOf"::: ) (Set (Var "S")) ")" )))); :: deftheorem defines :::"operational"::: FOMODEL1:def 12 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v2_fomodel1 :::"operational"::: ) ) "iff" (Bool (Bool "not" (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S"))) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )); :: deftheorem defines :::"relational"::: FOMODEL1:def 13 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v3_fomodel1 :::"relational"::: ) ) "iff" (Bool (Bool "not" (Set (Set "(" ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k7_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S")) ")" ) ($#k1_tarski :::"}"::: ) )) "is" ($#v1_xboole_0 :::"empty"::: ) )) ")" )); definitionlet "S" be ($#l1_fomodel1 :::"Language-like"::: ) ; let "s" be ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); attr "s" is :::"literal"::: means :: FOMODEL1:def 14 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k2_fomodel1 :::"LettersOf"::: ) "S")); attr "s" is :::"low-compounding"::: means :: FOMODEL1:def 15 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) "S")); attr "s" is :::"operational"::: means :: FOMODEL1:def 16 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) "S")); attr "s" is :::"relational"::: means :: FOMODEL1:def 17 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k4_fomodel1 :::"RelSymbolsOf"::: ) "S")); attr "s" is :::"termal"::: means :: FOMODEL1:def 18 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) "S")); attr "s" is :::"own"::: means :: FOMODEL1:def 19 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) "S")); attr "s" is :::"ofAtomicFormula"::: means :: FOMODEL1:def 20 (Bool "s" ($#r2_hidden :::"in"::: ) (Set ($#k10_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) "S")); end; :: deftheorem defines :::"literal"::: FOMODEL1:def 14 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v4_fomodel1 :::"literal"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k2_fomodel1 :::"LettersOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"low-compounding"::: FOMODEL1:def 15 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v5_fomodel1 :::"low-compounding"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"operational"::: FOMODEL1:def 16 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v6_fomodel1 :::"operational"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"relational"::: FOMODEL1:def 17 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v7_fomodel1 :::"relational"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"termal"::: FOMODEL1:def 18 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v8_fomodel1 :::"termal"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"own"::: FOMODEL1:def 19 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v9_fomodel1 :::"own"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))) ")" ))); :: deftheorem defines :::"ofAtomicFormula"::: FOMODEL1:def 20 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ) "iff" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k10_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S")))) ")" ))); definitionlet "S" be ($#l4_struct_0 :::"ZeroOneStr"::: ) ; let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Const "S"))) ($#k1_tarski :::"}"::: ) )); func :::"TrivialArity"::: "s" -> ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) equals :: FOMODEL1:def 21 (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 2)) if (Bool "s" ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "S")) otherwise (Set ($#k6_numbers :::"0"::: ) ); end; :: deftheorem defines :::"TrivialArity"::: FOMODEL1:def 21 : (Bool "for" (Set (Var "S")) "being" ($#l4_struct_0 :::"ZeroOneStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "S"))) ($#k1_tarski :::"}"::: ) )) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "S"))))) "implies" (Bool (Set ($#k12_fomodel1 :::"TrivialArity"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 2))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "S")))))) "implies" (Bool (Set ($#k12_fomodel1 :::"TrivialArity"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ")" ))); definitionlet "S" be ($#l4_struct_0 :::"ZeroOneStr"::: ) ; let "s" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Const "S"))) ($#k1_tarski :::"}"::: ) )); :: original: :::"TrivialArity"::: redefine func :::"TrivialArity"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l4_struct_0 :::"ZeroOneStr"::: ) ; func "S" :::"TrivialArity"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "S") ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ) means :: FOMODEL1:def 22 (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "S") ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "S") ($#k6_domain_1 :::"}"::: ) )) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k13_fomodel1 :::"TrivialArity"::: ) (Set (Var "s"))))); end; :: deftheorem defines :::"TrivialArity"::: FOMODEL1:def 22 : (Bool "for" (Set (Var "S")) "being" ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l4_struct_0 :::"ZeroOneStr"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "S"))) ($#k6_domain_1 :::"}"::: ) ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k14_fomodel1 :::"TrivialArity"::: ) )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "S"))) ($#k6_domain_1 :::"}"::: ) )) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k13_fomodel1 :::"TrivialArity"::: ) (Set (Var "s"))))) ")" ))); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"infinite"::: ) for ($#l4_struct_0 :::"ZeroOneStr"::: ) ; end; registrationlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v8_struct_0 :::"infinite"::: ) ($#l4_struct_0 :::"ZeroOneStr"::: ) ; cluster (Set (Set "(" "S" ($#k14_fomodel1 :::"TrivialArity"::: ) ")" ) ($#k8_relat_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) )) -> ($#v1_finset_1 :::"infinite"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language-like"::: ) ; attr "S" is :::"eligible"::: means :: FOMODEL1:def 23 (Bool "(" (Bool (Set ($#k2_fomodel1 :::"LettersOf"::: ) "S") "is" ($#v1_finset_1 :::"infinite"::: ) ) & (Bool (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_fomodel1 :::"TheEqSymbOf"::: ) "S" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 2))) ")" ); end; :: deftheorem defines :::"eligible"::: FOMODEL1:def 23 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool "(" (Bool (Set (Var "S")) "is" ($#v11_fomodel1 :::"eligible"::: ) ) "iff" (Bool "(" (Bool (Set ($#k2_fomodel1 :::"LettersOf"::: ) (Set (Var "S"))) "is" ($#v1_finset_1 :::"infinite"::: ) ) & (Bool (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Num 2))) ")" ) ")" )); registration cluster ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v11_fomodel1 :::"eligible"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; definitionmode Language is ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v11_fomodel1 :::"eligible"::: ) ($#l1_fomodel1 :::"Language-like"::: ) ; end; definitionlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; :: original: :::"AllSymbolsOf"::: redefine func :::"AllSymbolsOf"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#v11_fomodel1 :::"eligible"::: ) ($#l1_fomodel1 :::"Language-like"::: ) ; cluster (Set ($#k2_fomodel1 :::"LettersOf"::: ) "S") -> ($#v1_finset_1 :::"infinite"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"LettersOf"::: redefine func :::"LettersOf"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) "S") -> ($#v7_fomodel1 :::"relational"::: ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; definitionlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; :: original: :::"AtomicFormulaSymbolsOf"::: redefine func :::"AtomicFormulaSymbolsOf"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ); end; definitionlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; :: original: :::"TheEqSymbOf"::: redefine func :::"TheEqSymbOf"::: "S" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) "S"); end; theorem :: FOMODEL1:1 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool "(" (Bool (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) (Set (Var "S")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set "(" ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S")))) & (Bool (Set (Set "(" ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k18_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S")) ")" ) ($#k6_domain_1 :::"}"::: ) )) & (Bool (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k16_fomodel1 :::"LettersOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S")))) & (Bool (Set ($#k6_fomodel1 :::"LowerCompoundersOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S")))) ")" )) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v9_fomodel1 :::"own"::: ) -> ($#v10_fomodel1 :::"ofAtomicFormula"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v7_fomodel1 :::"relational"::: ) -> ($#v5_fomodel1 :::"low-compounding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v6_fomodel1 :::"operational"::: ) -> ($#v8_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v4_fomodel1 :::"literal"::: ) -> ($#v8_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v8_fomodel1 :::"termal"::: ) -> ($#v9_fomodel1 :::"own"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v6_fomodel1 :::"operational"::: ) -> ($#v5_fomodel1 :::"low-compounding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v5_fomodel1 :::"low-compounding"::: ) -> ($#v10_fomodel1 :::"ofAtomicFormula"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v8_fomodel1 :::"termal"::: ) -> ($#~v7_fomodel1 "non" ($#v7_fomodel1 :::"relational"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v4_fomodel1 :::"literal"::: ) -> ($#~v7_fomodel1 "non" ($#v7_fomodel1 :::"relational"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v4_fomodel1 :::"literal"::: ) -> ($#~v6_fomodel1 "non" ($#v6_fomodel1 :::"operational"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#v7_fomodel1 :::"relational"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); cluster ($#v4_fomodel1 :::"literal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#v5_fomodel1 :::"low-compounding"::: ) ($#v8_fomodel1 :::"termal"::: ) -> ($#v5_fomodel1 :::"low-compounding"::: ) ($#v6_fomodel1 :::"operational"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#v10_fomodel1 :::"ofAtomicFormula"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); func :::"ar"::: "s" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) equals :: FOMODEL1:def 24 (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S") ($#k1_funct_1 :::"."::: ) "s"); end; :: deftheorem defines :::"ar"::: FOMODEL1:def 24 : (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")) "holds" (Bool (Set ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k19_fomodel1 :::"ar"::: ) "s") -> ($#v1_xboole_0 :::"zero"::: ) for ($#m1_hidden :::"number"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func "S" :::"-cons"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: FOMODEL1:def 25 (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k11_monoid_0 :::"-concatenation"::: ) ); end; :: deftheorem defines :::"-cons"::: FOMODEL1:def 25 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set (Var "S")) ($#k20_fomodel1 :::"-cons"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k11_monoid_0 :::"-concatenation"::: ) ))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func "S" :::"-multiCat"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) "," (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) equals :: FOMODEL1:def 26 (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k8_fomodel0 :::"-multiCat"::: ) ); end; :: deftheorem defines :::"-multiCat"::: FOMODEL1:def 26 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k8_fomodel0 :::"-multiCat"::: ) ))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func "S" :::"-firstChar"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) equals :: FOMODEL1:def 27 (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k6_fomodel0 :::"-firstChar"::: ) ); end; :: deftheorem defines :::"-firstChar"::: FOMODEL1:def 27 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k6_fomodel0 :::"-firstChar"::: ) ))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is "S" :::"-prefix"::: means :: FOMODEL1:def 28 (Bool "X" "is" (Set ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S") ($#v3_fomodel0 :::"-prefix"::: ) ); end; :: deftheorem defines :::"-prefix"::: FOMODEL1:def 28 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" (Set (Var "S")) ($#v12_fomodel1 :::"-prefix"::: ) ) "iff" (Bool (Set (Var "X")) "is" (Set ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S"))) ($#v3_fomodel0 :::"-prefix"::: ) ) ")" ))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster "S" ($#v12_fomodel1 :::"-prefix"::: ) -> (Set ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S") ($#v3_fomodel0 :::"-prefix"::: ) for ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S") ($#v3_fomodel0 :::"-prefix"::: ) -> "S" ($#v12_fomodel1 :::"-prefix"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); mode string of "S" is ($#m2_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; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) 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; registration cluster ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#v11_fomodel1 :::"eligible"::: ) -> ($#v8_struct_0 :::"infinite"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S") -> ($#v1_finset_1 :::"infinite"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "Strings" be ($#m1_hidden :::"set"::: ) ; func :::"Compound"::: "(" "s" "," "Strings" ")" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 29 "{" (Set "(" (Set ($#k4_matrix_2 :::"<*"::: ) "s" ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "StringTuple")) ")" ) ")" ) where StringTuple "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "StringTuple"))) ($#r1_tarski :::"c="::: ) "Strings") & (Bool (Set (Var "StringTuple")) "is" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) "s" ")" )) ($#v3_card_1 :::"-element"::: ) ) ")" ) "}" ; end; :: deftheorem defines :::"Compound"::: FOMODEL1:def 29 : (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 "Strings")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k23_fomodel1 :::"Compound"::: ) "(" (Set (Var "s")) "," (Set (Var "Strings")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "s")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "StringTuple")) ")" ) ")" ) where StringTuple "is" ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k3_finseq_2 :::"*"::: ) ) : (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "StringTuple"))) ($#r1_tarski :::"c="::: ) (Set (Var "Strings"))) & (Bool (Set (Var "StringTuple")) "is" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "s")) ")" )) ($#v3_card_1 :::"-element"::: ) ) ")" ) "}" )))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); let "Strings" be ($#m1_hidden :::"set"::: ) ; :: original: :::"Compound"::: redefine func :::"Compound"::: "(" "s" "," "Strings" ")" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func "S" :::"-termsOfMaxDepth"::: -> ($#m1_hidden :::"Function":::) means :: FOMODEL1:def 30 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_fomodel1 :::"AtomicTermsOf"::: ) "S")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k24_fomodel1 :::"Compound"::: ) "(" (Set (Var "s")) "," (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" ) where s "is" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" "S" : (Bool (Set (Var "s")) "is" ($#v6_fomodel1 :::"operational"::: ) ) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" it ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"-termsOfMaxDepth"::: FOMODEL1:def 30 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k5_numbers :::"NAT"::: ) )) & (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_fomodel1 :::"AtomicTermsOf"::: ) (Set (Var "S")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k24_fomodel1 :::"Compound"::: ) "(" (Set (Var "s")) "," (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ")" ")" ) where s "is" ($#v10_fomodel1 :::"ofAtomicFormula"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) : (Bool (Set (Var "s")) "is" ($#v6_fomodel1 :::"operational"::: ) ) "}" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"AtomicTermsOf"::: redefine func :::"AtomicTermsOf"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func :::"AllTermsOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 31 (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "S" ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ")" )); end; :: deftheorem defines :::"AllTermsOf"::: FOMODEL1:def 31 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "S")) ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ")" )))); theorem :: FOMODEL1:2 (Bool "for" (Set (Var "mm")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "mm"))) ($#r1_tarski :::"c="::: ) (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "w" be ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); attr "w" is :::"termal"::: means :: FOMODEL1:def 32 (Bool "w" ($#r2_hidden :::"in"::: ) (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) "S")); end; :: deftheorem defines :::"termal"::: FOMODEL1:def 32 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "w")) "being" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "w")) "is" ($#v13_fomodel1 :::"termal"::: ) ) "iff" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")))) ")" ))); definitionlet "m" be ($#m1_hidden :::"Nat":::); let "S" be ($#l1_fomodel1 :::"Language":::); let "w" be ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); attr "w" is "m" :::"-termal"::: means :: FOMODEL1:def 33 (Bool "w" ($#r2_hidden :::"in"::: ) (Set (Set "(" "S" ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "m")); end; :: deftheorem defines :::"-termal"::: FOMODEL1:def 33 : (Bool "for" (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "w")) "being" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "w")) "is" (Set (Var "m")) ($#v14_fomodel1 :::"-termal"::: ) ) "iff" (Bool (Set (Var "w")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k25_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" )))); registrationlet "m" be ($#m1_hidden :::"Nat":::); let "S" be ($#l1_fomodel1 :::"Language":::); cluster "m" ($#v14_fomodel1 :::"-termal"::: ) -> ($#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 :::"}"::: ) )); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"-termsOfMaxDepth"::: redefine func "S" :::"-termsOfMaxDepth"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"AllTermsOf"::: redefine func :::"AllTermsOf"::: "S" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); cluster (Set (Set "(" "S" ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "m") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" "S" ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "m"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k29_fomodel1 :::"AllTermsOf"::: ) "S"); end; registrationlet "m" be ($#m1_hidden :::"Nat":::); let "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"::: ) ($#v4_card_3 :::"countable"::: ) ($#v2_pre_poly :::"finite-support"::: ) "m" ($#v14_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 :::"}"::: ) )); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k6_numbers :::"0"::: ) ) ($#v14_fomodel1 :::"-termal"::: ) -> (Num 1) ($#v3_card_1 :::"-element"::: ) 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; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "w" be (Set ($#k6_numbers :::"0"::: ) ) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "w") -> ($#v4_fomodel1 :::"literal"::: ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "w" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "w") -> ($#v8_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func :::"ar"::: "t" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) equals :: FOMODEL1:def 34 (Set ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "t" ")" )); end; :: deftheorem defines :::"ar"::: FOMODEL1:def 34 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k30_fomodel1 :::"ar"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ))))); theorem :: FOMODEL1:3 (Bool "for" (Set (Var "mm")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "w")) "being" (Set (Set (Var "b1")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "ex" (Set (Var "T")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" (Set "(" (Set (Var "S")) ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "mm")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "st" (Bool "(" (Bool (Set (Var "T")) "is" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ) & (Bool (Set (Var "w")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "w")) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "T")) ")" ))) ")" ))))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); cluster (Set (Set "(" "S" ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "m") -> "S" ($#v12_fomodel1 :::"-prefix"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "V" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ); cluster (Set (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "V") -> ($#v1_relat_1 :::"Relation-like"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "V" be ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) (Set (Const "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ); cluster (Set (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "V") -> ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_hidden :::"Relation":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi" be ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); attr "phi" is :::"0wff"::: means :: FOMODEL1:def 35 (Bool "ex" (Set (Var "s")) "being" ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" "S"(Bool "ex" (Set (Var "V")) "being" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "b1")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ) "st" (Bool "phi" ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "s")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "V")) ")" ))))); end; :: deftheorem defines :::"0wff"::: FOMODEL1:def 35 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "phi")) "being" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "phi")) "is" ($#v15_fomodel1 :::"0wff"::: ) ) "iff" (Bool "ex" (Set (Var "s")) "being" ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S"))(Bool "ex" (Set (Var "V")) "being" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set (Var "b3")) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "st" (Bool (Set (Var "phi")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set (Var "s")) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "V")) ")" ))))) ")" ))); 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"::: ) ($#v4_card_3 :::"countable"::: ) ($#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; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "phi") -> ($#v7_fomodel1 :::"relational"::: ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func :::"AtomicFormulasOf"::: "S" -> ($#m1_hidden :::"set"::: ) equals :: FOMODEL1:def 36 "{" (Set (Var "phi")) where phi "is" ($#m2_subset_1 :::"string":::) "of" "S" : (Bool (Set (Var "phi")) "is" ($#v15_fomodel1 :::"0wff"::: ) ) "}" ; end; :: deftheorem defines :::"AtomicFormulasOf"::: FOMODEL1:def 36 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set ($#k31_fomodel1 :::"AtomicFormulasOf"::: ) (Set (Var "S"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "phi")) where phi "is" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) : (Bool (Set (Var "phi")) "is" ($#v15_fomodel1 :::"0wff"::: ) ) "}" )); definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"AtomicFormulasOf"::: redefine func :::"AtomicFormulasOf"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k31_fomodel1 :::"AtomicFormulasOf"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#v15_fomodel1 :::"0wff"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k32_fomodel1 :::"AtomicFormulasOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k27_fomodel1 :::"AllTermsOf"::: ) "S") -> "S" ($#v12_fomodel1 :::"-prefix"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func :::"SubTerms"::: "t" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ) means :: FOMODEL1:def 37 (Bool "(" (Bool it "is" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "t" ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ) & (Bool "t" ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "t" ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) it ")" ))) ")" ); end; :: deftheorem defines :::"SubTerms"::: FOMODEL1:def 37 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k33_fomodel1 :::"SubTerms"::: ) (Set (Var "t")))) "iff" (Bool "(" (Bool (Set (Var "b3")) "is" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ) & (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t")) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b3")) ")" ))) ")" ) ")" )))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k33_fomodel1 :::"SubTerms"::: ) "t") -> (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k30_fomodel1 :::"ar"::: ) "t" ")" )) ($#v3_card_1 :::"-element"::: ) for ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "t0" be (Set ($#k6_numbers :::"0"::: ) ) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k33_fomodel1 :::"SubTerms"::: ) "t0") -> ($#v1_xboole_0 :::"empty"::: ) for ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ); end; registrationlet "mm" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "S" be ($#l1_fomodel1 :::"Language":::); let "t" be (Set (Set (Const "mm")) ($#k2_xcmplx_0 :::"+"::: ) (Num 1)) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k33_fomodel1 :::"SubTerms"::: ) "t") -> (Set (Set "(" "S" ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "mm") ($#v5_relat_1 :::"-valued"::: ) for ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func :::"SubTerms"::: "phi" -> (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi" ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ) means :: FOMODEL1:def 38 (Bool "phi" ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi" ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) it ")" ))); end; :: deftheorem defines :::"SubTerms"::: FOMODEL1:def 38 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "phi")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" (Set (Var "b1")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b2")) ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ($#m2_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k29_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k34_fomodel1 :::"SubTerms"::: ) (Set (Var "phi")))) "iff" (Bool (Set (Var "phi")) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_matrix_2 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi")) ")" ) ($#k4_matrix_2 :::"*>"::: ) ) ($#k7_finseq_1 :::"^"::: ) (Set "(" (Set "(" (Set (Var "S")) ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b3")) ")" ))) ")" )))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k34_fomodel1 :::"SubTerms"::: ) "phi") -> (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi" ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"FinSequence":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"AllTermsOf"::: redefine func :::"AllTermsOf"::: "S" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#v13_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S"); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); func "S" :::"-subTerms"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) "," (Set "(" (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k2_fomodel0 :::"*"::: ) ")" ) means :: FOMODEL1:def 39 (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) "S") "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k33_fomodel1 :::"SubTerms"::: ) (Set (Var "t"))))); end; :: deftheorem defines :::"-subTerms"::: FOMODEL1:def 39 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) "," (Set "(" (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S")) ")" ) ($#k2_fomodel0 :::"*"::: ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k36_fomodel1 :::"-subTerms"::: ) )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set ($#k33_fomodel1 :::"SubTerms"::: ) (Set (Var "t"))))) ")" ))); theorem :: FOMODEL1:4 (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" (Set (Var "S")) ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "S")) ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ))))) ; theorem :: FOMODEL1:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))))) "holds" (Bool "ex" (Set (Var "nn")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "S")) ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "nn"))))))) ; theorem :: FOMODEL1:6 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FOMODEL1:7 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))) "is" (Set (Var "S")) ($#v12_fomodel1 :::"-prefix"::: ) )) ; theorem :: FOMODEL1:8 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k35_fomodel1 :::"AllTermsOf"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S"))))) ; theorem :: FOMODEL1:9 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" ($#k18_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: FOMODEL1:10 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_fomodel1 :::"OpSymbolsOf"::: ) (Set (Var "S"))))) ; theorem :: FOMODEL1:11 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set "(" ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set "(" ($#k4_fomodel1 :::"RelSymbolsOf"::: ) (Set (Var "S")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) (Set (Var "S"))))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#~v7_fomodel1 "non" ($#v7_fomodel1 :::"relational"::: ) ) ($#v10_fomodel1 :::"ofAtomicFormula"::: ) -> ($#v8_fomodel1 :::"termal"::: ) ($#v10_fomodel1 :::"ofAtomicFormula"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"OwnSymbolsOf"::: redefine func :::"OwnSymbolsOf"::: "S" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#~v4_fomodel1 "non" ($#v4_fomodel1 :::"literal"::: ) ) ($#v8_fomodel1 :::"termal"::: ) -> ($#v6_fomodel1 :::"operational"::: ) ($#v8_fomodel1 :::"termal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; theorem :: FOMODEL1:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_2 :::"Element"::: ) "of" (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) )) ")" ))) ; theorem :: FOMODEL1:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool "(" (Bool (Set (Var "x")) "is" ($#m2_subset_1 :::"string":::) "of" (Set (Var "S"))) "iff" (Bool (Set (Var "x")) "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")))) ")" ))) ; theorem :: FOMODEL1:14 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) "holds" (Bool (Set (Set (Var "S")) ($#k28_fomodel1 :::"-termsOfMaxDepth"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ")" ))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster -> ($#v4_fomodel1 :::"literal"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k16_fomodel1 :::"LettersOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) "S") -> ($#~v5_fomodel1 "non" ($#v5_fomodel1 :::"low-compounding"::: ) ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) "S") -> ($#~v9_fomodel1 "non" ($#v9_fomodel1 :::"own"::: ) ) for ($#m1_subset_1 :::"Element":::) "of" "S"; end; theorem :: FOMODEL1:15 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) (Set (Var "S")))) & (Bool (Set (Var "s")) ($#r1_hidden :::"<>"::: ) (Set ($#k18_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S")))))) ; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); func :::"Depth"::: "t" -> ($#m1_hidden :::"Nat":::) means :: FOMODEL1:def 40 (Bool "(" (Bool "t" "is" it ($#v14_fomodel1 :::"-termal"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool "t" "is" (Set (Var "n")) ($#v14_fomodel1 :::"-termal"::: ) )) "holds" (Bool it ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ); end; :: deftheorem defines :::"Depth"::: FOMODEL1:def 40 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k38_fomodel1 :::"Depth"::: ) (Set (Var "t")))) "iff" (Bool "(" (Bool (Set (Var "t")) "is" (Set (Var "b3")) ($#v14_fomodel1 :::"-termal"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "t")) "is" (Set (Var "n")) ($#v14_fomodel1 :::"-termal"::: ) )) "holds" (Bool (Set (Var "b3")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" ) ")" ) ")" )))); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m0" be ($#v1_xboole_0 :::"zero"::: ) ($#m1_hidden :::"number"::: ) ; let "t" be (Set (Const "m0")) ($#v14_fomodel1 :::"-termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k38_fomodel1 :::"Depth"::: ) "t") -> ($#v1_xboole_0 :::"zero"::: ) for ($#m1_hidden :::"number"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v5_fomodel1 :::"low-compounding"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k19_fomodel1 :::"ar"::: ) "s") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) for ($#m1_hidden :::"number"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v8_fomodel1 :::"termal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k19_fomodel1 :::"ar"::: ) "s") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "s" be ($#v7_fomodel1 :::"relational"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k19_fomodel1 :::"ar"::: ) "s") -> ($#v1_xxreal_0 :::"ext-real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ; end; theorem :: FOMODEL1:16 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "t")) "being" ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "st" (Bool (Bool (Bool "not" (Set (Var "t")) "is" (Set ($#k6_numbers :::"0"::: ) ) ($#v14_fomodel1 :::"-termal"::: ) ))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) "is" ($#v6_fomodel1 :::"operational"::: ) ) & (Bool (Set ($#k33_fomodel1 :::"SubTerms"::: ) (Set (Var "t"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ))) ; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set "S" ($#k21_fomodel1 :::"-multiCat"::: ) ) -> ($#v1_pre_poly :::"FinSequence-yielding"::: ) for ($#m1_hidden :::"Function":::); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "W" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Const "S")) ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set (Set "(" "S" ($#k21_fomodel1 :::"-multiCat"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "W") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "l" be ($#v4_fomodel1 :::"literal"::: ) ($#m1_subset_1 :::"Element":::) "of" (Set (Const "S")); cluster (Set ($#k5_finseq_1 :::"<*"::: ) "l" ($#k5_finseq_1 :::"*>"::: ) ) -> (Set ($#k6_numbers :::"0"::: ) ) ($#v14_fomodel1 :::"-termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m", "n" be ($#m1_hidden :::"Nat":::); cluster (Set "m" ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k3_xcmplx_0 :::"*"::: ) "n" ")" )) ($#v14_fomodel1 :::"-termal"::: ) -> (Set "m" ($#k2_xcmplx_0 :::"+"::: ) "n") ($#v14_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 :::"}"::: ) )); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#~v5_fomodel1 "non" ($#v5_fomodel1 :::"low-compounding"::: ) ) ($#v9_fomodel1 :::"own"::: ) -> ($#v4_fomodel1 :::"literal"::: ) ($#v9_fomodel1 :::"own"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S"); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k33_fomodel1 :::"SubTerms"::: ) "t") -> (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "t" ")" ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k34_fomodel1 :::"SubTerms"::: ) "phi0") -> (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "phi0" ")" ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_hidden :::"Relation":::); end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); :: original: :::"-termsOfMaxDepth"::: redefine func "S" :::"-termsOfMaxDepth"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ); end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "mm" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster (Set (Set "(" "S" ($#k39_fomodel1 :::"-termsOfMaxDepth"::: ) ")" ) ($#k1_funct_1 :::"."::: ) "mm") -> ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "m" be ($#m1_hidden :::"Nat":::); let "t" be ($#v13_fomodel1 :::"termal"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set "t" ($#k13_fomodel0 :::"null"::: ) "m") -> (Set (Set "(" ($#k38_fomodel1 :::"Depth"::: ) "t" ")" ) ($#k2_xcmplx_0 :::"+"::: ) "m") ($#v14_fomodel1 :::"-termal"::: ) for ($#m2_subset_1 :::"string":::) "of" "S"; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#v13_fomodel1 :::"termal"::: ) -> (Set ($#k5_fomodel1 :::"TermSymbolsOf"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) 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; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set (Set "(" ($#k35_fomodel1 :::"AllTermsOf"::: ) "S" ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" (Set "(" ($#k5_fomodel1 :::"TermSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); let "phi0" be ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Const "S")); cluster (Set ($#k34_fomodel1 :::"SubTerms"::: ) "phi0") -> (Set (Set "(" ($#k5_fomodel1 :::"TermSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ) ($#v5_relat_1 :::"-valued"::: ) (Set ($#k1_int_2 :::"abs"::: ) (Set "(" ($#k19_fomodel1 :::"ar"::: ) (Set "(" (Set "(" "S" ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) "phi0" ")" ) ")" )) ($#v3_card_1 :::"-element"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#v15_fomodel1 :::"0wff"::: ) -> (Set ($#k17_fomodel1 :::"AtomicFormulaSymbolsOf"::: ) "S") ($#v5_relat_1 :::"-valued"::: ) 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; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k9_fomodel1 :::"OwnSymbolsOf"::: ) "S") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: FOMODEL1:17 (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "phi0")) "being" ($#v15_fomodel1 :::"0wff"::: ) ($#m2_subset_1 :::"string":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set "(" (Set (Var "S")) ($#k22_fomodel1 :::"-firstChar"::: ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "phi0"))) ($#r1_hidden :::"<>"::: ) (Set ($#k18_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S"))))) "holds" (Bool (Set (Var "phi0")) "is" (Set ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) (Set (Var "S"))) ($#v5_relat_1 :::"-valued"::: ) ))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fomodel1 :::"strict"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; definitionlet "S1", "S2" be ($#l1_fomodel1 :::"Language-like"::: ) ; attr "S2" is "S1" :::"-extending"::: means :: FOMODEL1:def 41 (Bool "(" (Bool (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S1") ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "S2")) & (Bool (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) "S1") ($#r1_hidden :::"="::: ) (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) "S2")) & (Bool (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) "S1") ($#r1_hidden :::"="::: ) (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) "S2")) ")" ); end; :: deftheorem defines :::"-extending"::: FOMODEL1:def 41 : (Bool "for" (Set (Var "S1")) "," (Set (Var "S2")) "being" ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool "(" (Bool (Set (Var "S2")) "is" (Set (Var "S1")) ($#v16_fomodel1 :::"-extending"::: ) ) "iff" (Bool "(" (Bool (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S1"))) ($#r1_relset_1 :::"c="::: ) (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "S2")))) & (Bool (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_fomodel1 :::"TheEqSymbOf"::: ) (Set (Var "S2")))) & (Bool (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) (Set (Var "S1"))) ($#r1_hidden :::"="::: ) (Set ($#k8_fomodel1 :::"TheNorSymbOf"::: ) (Set (Var "S2")))) ")" ) ")" )); registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster (Set "S" ($#k22_fomodel0 :::"null"::: ) ) -> "S" ($#v16_fomodel1 :::"-extending"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "S" be ($#l1_fomodel1 :::"Language":::); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"infinite"::: ) ($#v11_fomodel1 :::"eligible"::: ) "S" ($#v16_fomodel1 :::"-extending"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "S1" be ($#l1_fomodel1 :::"Language":::); let "S2" be (Set (Const "S1")) ($#v16_fomodel1 :::"-extending"::: ) ($#l1_fomodel1 :::"Language":::); cluster (Set (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S1" ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k37_fomodel1 :::"OwnSymbolsOf"::: ) "S2" ")" )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; definitionlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; func "L" :::"extendWith"::: "f" -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fomodel1 :::"strict"::: ) ($#l1_fomodel1 :::"Language-like"::: ) means :: FOMODEL1:def 42 (Bool "(" (Bool (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "L") ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" "L"))) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" "L")) & (Bool (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" "L")) ")" ); end; :: deftheorem defines :::"extendWith"::: FOMODEL1:def 42 : (Bool "for" (Set (Var "f")) "being" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "L")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) (Bool "for" (Set (Var "b3")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fomodel1 :::"strict"::: ) ($#l1_fomodel1 :::"Language-like"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "L")) ($#k40_fomodel1 :::"extendWith"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "L"))) ($#k6_domain_1 :::"}"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "the" ($#u1_fomodel1 :::"adicity"::: ) "of" (Set (Var "L"))))) & (Bool (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u2_struct_0 :::"ZeroF"::: ) "of" (Set (Var "L")))) & (Bool (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u3_struct_0 :::"OneF"::: ) "of" (Set (Var "L")))) ")" ) ")" )))); registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; let "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "S" ($#k40_fomodel1 :::"extendWith"::: ) "f") -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_fomodel1 :::"strict"::: ) "S" ($#v16_fomodel1 :::"-extending"::: ) ; end; registrationlet "S" be ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; cluster "S" ($#v16_fomodel1 :::"-extending"::: ) -> ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "S" be ($#v11_fomodel1 :::"eligible"::: ) ($#l1_fomodel1 :::"Language-like"::: ) ; cluster "S" ($#v16_fomodel1 :::"-extending"::: ) -> ($#v11_fomodel1 :::"eligible"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "E" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Relation":::); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k6_relat_1 :::"|`"::: ) "E") -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "m" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "m") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "S" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; func "S" :::"addLettersNotIn"::: "X" -> "S" ($#v16_fomodel1 :::"-extending"::: ) ($#l1_fomodel1 :::"Language":::) equals :: FOMODEL1:def 43 (Set "S" ($#k40_fomodel1 :::"extendWith"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k21_fomodel0 :::"SymbolsOf"::: ) "X" ")" ) ")" ) ($#k23_fomodel0 :::"-freeCountableSet"::: ) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )); end; :: deftheorem defines :::"addLettersNotIn"::: FOMODEL1:def 43 : (Bool "for" (Set (Var "S")) "being" ($#l1_fomodel1 :::"Language":::) (Bool "for" (Set (Var "X")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "S")) ($#k41_fomodel1 :::"addLettersNotIn"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k40_fomodel1 :::"extendWith"::: ) (Set "(" (Set "(" (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set (Var "S")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k21_fomodel0 :::"SymbolsOf"::: ) (Set (Var "X")) ")" ) ")" ) ($#k23_fomodel0 :::"-freeCountableSet"::: ) ")" ) ($#k8_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ))))); registrationlet "S1" be ($#l1_fomodel1 :::"Language":::); let "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set (Set "(" ($#k16_fomodel1 :::"LettersOf"::: ) (Set "(" "S1" ($#k41_fomodel1 :::"addLettersNotIn"::: ) "X" ")" ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set "(" ($#k21_fomodel0 :::"SymbolsOf"::: ) "X" ")" )) -> ($#v1_finset_1 :::"infinite"::: ) ; end; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v6_struct_0 "non" ($#v6_struct_0 :::"degenerated"::: ) ) ($#~v7_struct_0 "non" ($#v7_struct_0 :::"trivial"::: ) ) ($#v8_struct_0 :::"infinite"::: ) ($#v1_orders_4 :::"countable"::: ) ($#v11_fomodel1 :::"eligible"::: ) for ($#l1_fomodel1 :::"Language-like"::: ) ; end; registrationlet "S" be ($#v1_orders_4 :::"countable"::: ) ($#l1_fomodel1 :::"Language":::); cluster (Set ($#k1_fomodel1 :::"AllSymbolsOf"::: ) "S") -> ($#v4_card_3 :::"countable"::: ) ; end; registrationlet "S" be ($#v1_orders_4 :::"countable"::: ) ($#l1_fomodel1 :::"Language":::); cluster (Set (Set "(" (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "S" ")" ) ($#k3_finseq_2 :::"*"::: ) ")" ) ($#k4_xboole_0 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v4_card_3 :::"countable"::: ) ; end; registrationlet "L" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_fomodel1 :::"Language-like"::: ) ; let "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) (Set "(" "L" ($#k40_fomodel1 :::"extendWith"::: ) "f" ")" ) ")" ) ($#k5_xboole_0 :::"\+\"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k15_fomodel1 :::"AllSymbolsOf"::: ) "L" ")" ) ")" )) -> ($#v1_xboole_0 :::"empty"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "S" be ($#v1_orders_4 :::"countable"::: ) ($#l1_fomodel1 :::"Language":::); let "X" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set "S" ($#k41_fomodel1 :::"addLettersNotIn"::: ) "X") -> ($#v1_orders_4 :::"countable"::: ) for ($#l1_struct_0 :::"1-sorted"::: ) ; end;