:: TURING_1 semantic presentation begin definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"+*"::: redefine func "f" :::"+*"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); let "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Y")); :: original: :::".-->"::: redefine func "a" :::".-->"::: "b" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; notationlet "n" be ($#m1_hidden :::"Nat":::); synonym :::"SegM"::: "n" for :::"succ"::: "n"; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); :: original: :::"SegM"::: redefine func :::"SegM"::: "n" -> ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: TURING_1:def 1 "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) "n") "}" ; end; :: deftheorem defines :::"SegM"::: TURING_1:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_turing_1 :::"SegM"::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) "{" (Set (Var "k")) where k "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) "}" )); registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k1_ordinal1 :::"SegM"::: ) "n") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: TURING_1:1 (Bool "for" (Set (Var "k")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "k")) ($#r2_hidden :::"in"::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Set (Var "n")))) "iff" (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "n"))) ")" )) ; theorem :: TURING_1:2 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "u")) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: TURING_1:3 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "u")) "," (Set (Var "v")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "v")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "v")) ($#k4_tarski :::"]"::: ) ))))) ; notationlet "i" be ($#m1_hidden :::"Nat":::); let "f" be ($#m1_hidden :::"FinSequence":::); synonym :::"Prefix"::: "(" "f" "," "i" ")" for "f" :::"|"::: "i"; end; definitionlet "i" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); :: original: :::"Prefix"::: redefine func :::"Prefix"::: "(" "f" "," "i" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ); end; theorem :: TURING_1:4 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_finseq_4 :::"*>"::: ) ) "," (Num 2) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "x2")))) ")" )) ; theorem :: TURING_1:5 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x1"))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 2) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "x1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "x2")))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) ($#k3_finseq_4 :::"*>"::: ) ) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "x2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "x3")))) ")" )) ; begin definitionattr "c1" is :::"strict"::: ; struct :::"TuringStr"::: -> ; aggr :::"TuringStr":::(# :::"Symbols":::, :::"FStates":::, :::"Tran":::, :::"InitS":::, :::"AcceptS"::: #) -> ($#l1_turing_1 :::"TuringStr"::: ) ; sel :::"Symbols"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; sel :::"FStates"::: "c1" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) ; sel :::"Tran"::: "c1" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "c1") "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "c1") ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "c1") "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "c1") "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ); sel :::"InitS"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "c1"); sel :::"AcceptS"::: "c1" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "c1"); end; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; mode State of "T" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "T"); mode Tape of "T" is ($#m2_funct_2 :::"Element"::: ) "of" (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T") ")" ); mode Symbol of "T" is ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T"); end; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "t" be ($#m2_funct_2 :::"Tape":::) "of" (Set (Const "T")); let "h" be ($#m1_hidden :::"Integer":::); let "s" be ($#m1_subset_1 :::"Symbol":::) "of" (Set (Const "T")); func :::"Tape-Chg"::: "(" "t" "," "h" "," "s" ")" -> ($#m2_funct_2 :::"Tape":::) "of" "T" equals :: TURING_1:def 2 (Set "t" ($#k1_funct_4 :::"+*"::: ) (Set "(" "h" ($#k16_funcop_1 :::".-->"::: ) "s" ")" )); end; :: deftheorem defines :::"Tape-Chg"::: TURING_1:def 2 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set (Var "t")) "," (Set (Var "h")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "h")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "s")) ")" ))))))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; mode All-State of "T" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "T") "," (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T") ")" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ); mode Tran-Source of "T" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "T") "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T") ($#k2_zfmisc_1 :::":]"::: ) ); mode Tran-Goal of "T" is ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "T") "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T") "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ); end; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "g" be ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Const "T")); func :::"offset"::: "g" -> ($#m1_hidden :::"Integer":::) equals :: TURING_1:def 3 (Set "g" ($#k3_mcart_1 :::"`3_3"::: ) ); end; :: deftheorem defines :::"offset"::: TURING_1:def 3 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k6_turing_1 :::"offset"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) )))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); func :::"Head"::: "s" -> ($#m1_hidden :::"Integer":::) equals :: TURING_1:def 4 (Set "s" ($#k2_mcart_1 :::"`2_3"::: ) ); end; :: deftheorem defines :::"Head"::: TURING_1:def 4 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k7_turing_1 :::"Head"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_mcart_1 :::"`2_3"::: ) )))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); func :::"TRAN"::: "s" -> ($#m1_subset_1 :::"Tran-Goal":::) "of" "T" equals :: TURING_1:def 5 (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" "T") ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "s" ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set "(" "s" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_turing_1 :::"Head"::: ) "s" ")" ) ")" ) ($#k4_tarski :::"]"::: ) )); end; :: deftheorem defines :::"TRAN"::: TURING_1:def 5 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "T"))) ($#k1_funct_1 :::"."::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "s")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "s")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k7_turing_1 :::"Head"::: ) (Set (Var "s")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); func :::"Following"::: "s" -> ($#m1_subset_1 :::"All-State":::) "of" "T" equals :: TURING_1:def 6 (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) "s" ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set "(" ($#k7_turing_1 :::"Head"::: ) "s" ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_turing_1 :::"offset"::: ) (Set "(" ($#k8_turing_1 :::"TRAN"::: ) "s" ")" ) ")" ) ")" ) "," (Set "(" ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set "(" "s" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) "," (Set "(" ($#k7_turing_1 :::"Head"::: ) "s" ")" ) "," (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) "s" ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ")" ) ($#k3_xtuple_0 :::"]"::: ) ) if (Bool (Set "s" ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "T")) otherwise "s"; end; :: deftheorem defines :::"Following"::: TURING_1:def 6 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "s")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T"))))) "implies" (Bool (Set ($#k9_turing_1 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set "(" ($#k7_turing_1 :::"Head"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_turing_1 :::"offset"::: ) (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set "(" (Set (Var "s")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) "," (Set "(" ($#k7_turing_1 :::"Head"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ")" ) ($#k3_xtuple_0 :::"]"::: ) )) ")" & "(" (Bool (Bool (Bool "not" (Set (Set (Var "s")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T")))))) "implies" (Bool (Set ($#k9_turing_1 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) ")" ")" ))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); func :::"Computation"::: "s" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "T") "," (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T") ")" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) means :: TURING_1:def 7 (Bool "(" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "s") & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set it ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_turing_1 :::"Following"::: ) (Set "(" it ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"Computation"::: TURING_1:def 7 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "T"))) "," (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "T"))) ")" ")" ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")))) "iff" (Bool "(" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_turing_1 :::"Following"::: ) (Set "(" (Set (Var "b3")) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ))) ")" ) ")" ) ")" )))); theorem :: TURING_1:6 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "s")) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T"))))) "holds" (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k9_turing_1 :::"Following"::: ) (Set (Var "s")))))) ; theorem :: TURING_1:7 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "s"))))) ; theorem :: TURING_1:8 (Bool "for" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_turing_1 :::"Following"::: ) (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" )))))) ; theorem :: TURING_1:9 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k9_turing_1 :::"Following"::: ) (Set (Var "s")))))) ; theorem :: TURING_1:10 (Bool "for" (Set (Var "i")) "," (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k"))))))) ; theorem :: TURING_1:11 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set ($#k9_turing_1 :::"Following"::: ) (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))))))) ; theorem :: TURING_1:12 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "j"))) & (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T"))))) "holds" (Bool (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i"))))))) ; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); attr "s" is :::"Accept-Halt"::: means :: TURING_1:def 8 (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) "s" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "T"))); end; :: deftheorem defines :::"Accept-Halt"::: TURING_1:def 8 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T"))))) ")" ))); definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "s" be ($#m1_subset_1 :::"All-State":::) "of" (Set (Const "T")); assume (Bool (Set (Const "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) ; func :::"Result"::: "s" -> ($#m1_subset_1 :::"All-State":::) "of" "T" means :: TURING_1:def 9 (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) "s" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) "s" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "T")) ")" )); end; :: deftheorem defines :::"Result"::: TURING_1:def 9 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) )) "holds" (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")))) "iff" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) & (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T")))) ")" )) ")" )))); theorem :: TURING_1:13 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) )) "holds" (Bool "ex" (Set (Var "k")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"="::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T")))) & (Bool (Set ($#k11_turing_1 :::"Result"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "k")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k")))) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_turing_1 :::"Computation"::: ) (Set (Var "s")) ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T")))) ")" ) ")" )))) ; definitionlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "y" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "y")) ($#r2_hidden :::"in"::: ) (Set (Const "B"))) ; func :::"id"::: "(" "A" "," "B" "," "y" ")" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) means :: TURING_1:def 10 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," "y" ($#k4_tarski :::"]"::: ) ))); end; :: deftheorem defines :::"id"::: TURING_1:def 10 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k12_turing_1 :::"id"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "y")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) ")" )))); definitionfunc :::"Sum_Tran"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 5) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k9_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 5) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k9_mcart_1 :::":]"::: ) ) equals :: TURING_1:def 11 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 5) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 5) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" )); end; :: deftheorem defines :::"Sum_Tran"::: TURING_1:def 11 : (Bool (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 5) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 5) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" ))); theorem :: TURING_1:14 (Bool "(" (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k13_turing_1 :::"Sum_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 5) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) ")" ) ; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "t" be ($#m2_funct_2 :::"Tape":::) "of" (Set (Const "T")); let "i", "j" be ($#m1_hidden :::"Integer":::); pred "t" :::"is_1_between"::: "i" "," "j" means :: TURING_1:def 12 (Bool "(" (Bool (Set "t" ($#k1_funct_1 :::"."::: ) "i") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "t" ($#k1_funct_1 :::"."::: ) "j") ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool "i" ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) "j")) "holds" (Bool (Set "t" ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ); end; :: deftheorem defines :::"is_1_between"::: TURING_1:def 12 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "i")) "," (Set (Var "j"))) "iff" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "j"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "k")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "k"))) & (Bool (Set (Var "k")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "j")))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ) ")" )))); definitionlet "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "t" be ($#m2_funct_2 :::"Tape":::) "of" (Set (Const "T")); pred "t" :::"storeData"::: "f" means :: TURING_1:def 13 (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f"))) "holds" (Bool "t" ($#r1_turing_1 :::"is_1_between"::: ) (Set (Set "(" ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" "f" "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )) "," (Set (Set "(" ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" "f" "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"storeData"::: TURING_1:def 13 : (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Var "f"))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Set "(" ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set (Var "f")) "," (Set (Var "i")) ")" ")" ) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "i")) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )) "," (Set (Set "(" ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set (Var "f")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Num 2) ($#k4_nat_1 :::"*"::: ) (Set (Var "i")) ")" )))) ")" )))); theorem :: TURING_1:15 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "s")) "," (Set (Var "n")) ($#k2_finseq_4 :::"*>"::: ) ))) "holds" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "s")) "," (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))))) ; theorem :: TURING_1:16 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "s")) "," (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))) "holds" (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "s")) "," (Set (Var "n")) ($#k2_finseq_4 :::"*>"::: ) ))))) ; theorem :: TURING_1:17 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "s")) "," (Set (Var "n")) ($#k2_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: TURING_1:18 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "s")) "," (Set (Var "n1")) "," (Set (Var "n2")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "s")) "," (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) "," (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) ")" )))) ; theorem :: TURING_1:19 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "s")) "," (Set (Var "n1")) "," (Set (Var "n2")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Var "s")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Bool (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "i"))) & (Bool (Set (Var "i")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n1")) ")" ) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4)))) "holds" (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" )))) ; theorem :: TURING_1:20 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool "(" (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 2) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ))) ")" ))) ; theorem :: TURING_1:21 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 3))) "holds" (Bool "(" (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 1) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 2) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 3) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ))) & (Bool (Set ($#k1_gr_cy_1 :::"Sum"::: ) (Set "(" ($#k4_turing_1 :::"Prefix"::: ) "(" (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" ) "," (Num 4) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3) ")" ))) ")" ))) ; theorem :: TURING_1:22 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "s")) "," (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))))))) ; theorem :: TURING_1:23 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "s")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 3)) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "s")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Var "s")) "," (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2))) & (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 2)) "," (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (Bool (Set (Var "t")) ($#r1_turing_1 :::"is_1_between"::: ) (Set (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4)) "," (Set (Set "(" (Set "(" (Set "(" (Set (Var "s")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 6))) ")" ))))) ; begin definitionfunc :::"SumTuring"::: -> ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) means :: TURING_1:def 14 (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 5))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k13_turing_1 :::"Sum_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Num 5)) ")" ); end; :: deftheorem defines :::"SumTuring"::: TURING_1:def 14 : (Bool "for" (Set (Var "b1")) "being" ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k14_turing_1 :::"SumTuring"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 5))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "b1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k13_turing_1 :::"Sum_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Num 5)) ")" ) ")" )); theorem :: TURING_1:24 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set (Var "t")) "," (Set (Var "h")) "," (Set (Var "s")) ")" ) ($#r2_funct_2 :::"="::: ) (Set (Var "t"))))))) ; theorem :: TURING_1:25 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "p")) "," (Set (Var "h")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set (Var "p")) "," (Set (Var "h")) "," (Set (Var "t")) ($#k3_xtuple_0 :::"]"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T"))))) "holds" (Bool (Set ($#k9_turing_1 :::"Following"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k3_xtuple_0 :::"["::: ) (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "(" (Set "(" ($#k7_turing_1 :::"Head"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" ($#k6_turing_1 :::"offset"::: ) (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ")" ) ")" ) "," (Set "(" ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set "(" (Set (Var "s")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) "," (Set "(" ($#k7_turing_1 :::"Head"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set "(" ($#k8_turing_1 :::"TRAN"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) ")" ")" ) ($#k3_xtuple_0 :::"]"::: ) ))))) ; theorem :: TURING_1:26 (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set (Var "t")) "," (Set (Var "h")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & "(" (Bool (Bool (Set (Var "i")) ($#r1_hidden :::"<>"::: ) (Set (Var "h")))) "implies" (Bool (Set (Set "(" ($#k5_turing_1 :::"Tape-Chg"::: ) "(" (Set (Var "t")) "," (Set (Var "h")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "t")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ")" )))))) ; theorem :: TURING_1:27 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set ($#k14_turing_1 :::"SumTuring"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set ($#k14_turing_1 :::"SumTuring"::: ) ) (Bool "for" (Set (Var "head")) "," (Set (Var "n1")) "," (Set (Var "n2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "head")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Set (Var "n1")) "," (Set (Var "n2")) ($#k3_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "head")))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Num 1) ($#k2_nat_1 :::"+"::: ) (Set (Var "head")) ")" ) "," (Set "(" (Set (Var "n1")) ($#k2_nat_1 :::"+"::: ) (Set (Var "n2")) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ")" )))) ; definitionlet "T" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "F" be ($#m1_hidden :::"Function":::); pred "T" :::"computes"::: "F" means :: TURING_1:def 15 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" "T" (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" "T" (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "F")) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "T") "," (Set (Var "a")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool "ex" (Set (Var "b")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set "F" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ))) ")" )) ")" ))))); end; :: deftheorem defines :::"computes"::: TURING_1:def 15 : (Bool "for" (Set (Var "T")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "T")) ($#r3_turing_1 :::"computes"::: ) (Set (Var "F"))) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "a")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "x")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T"))) "," (Set (Var "a")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "a")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool "ex" (Set (Var "b")) "," (Set (Var "y")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "b")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "y")) ($#k12_finseq_1 :::"*>"::: ) ))) ")" )) ")" ))))) ")" ))); theorem :: TURING_1:28 (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k15_comput_1 :::"[+]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Num 2) ($#k4_finseq_2 :::"-tuples_on"::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) ; theorem :: TURING_1:29 (Bool (Set ($#k14_turing_1 :::"SumTuring"::: ) ) ($#r3_turing_1 :::"computes"::: ) (Set ($#k15_comput_1 :::"[+]"::: ) )) ; begin definitionfunc :::"Succ_Tran"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k9_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k9_mcart_1 :::":]"::: ) ) equals :: TURING_1:def 16 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" )); end; :: deftheorem defines :::"Succ_Tran"::: TURING_1:def 16 : (Bool (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" ))); theorem :: TURING_1:30 (Bool "(" (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k15_turing_1 :::"Succ_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) ")" ) ; definitionfunc :::"SuccTuring"::: -> ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) means :: TURING_1:def 17 (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 4))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k15_turing_1 :::"Succ_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Num 4)) ")" ); end; :: deftheorem defines :::"SuccTuring"::: TURING_1:def 17 : (Bool "for" (Set (Var "b1")) "being" ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k16_turing_1 :::"SuccTuring"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 4))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "b1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k15_turing_1 :::"Succ_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) ")" )); theorem :: TURING_1:31 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set ($#k16_turing_1 :::"SuccTuring"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set ($#k16_turing_1 :::"SuccTuring"::: ) ) (Bool "for" (Set (Var "head")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "head")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Set (Var "n")) ($#k2_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "head"))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ")" )))) ; theorem :: TURING_1:32 (Bool (Set ($#k16_turing_1 :::"SuccTuring"::: ) ) ($#r3_turing_1 :::"computes"::: ) (Set (Num 1) ($#k4_comput_1 :::"succ"::: ) (Num 1))) ; begin definitionfunc :::"Zero_Tran"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k9_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k9_mcart_1 :::":]"::: ) ) equals :: TURING_1:def 18 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Num 1) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" )); end; :: deftheorem defines :::"Zero_Tran"::: TURING_1:def 18 : (Bool (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 4) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Num 1) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ) ")" ))); theorem :: TURING_1:33 (Bool "(" (Bool (Set (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Num 1) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k17_turing_1 :::"Zero_Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 3) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 4) "," (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) ")" ) ; definitionfunc :::"ZeroTuring"::: -> ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) means :: TURING_1:def 19 (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 4))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k17_turing_1 :::"Zero_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Num 4)) ")" ); end; :: deftheorem defines :::"ZeroTuring"::: TURING_1:def 19 : (Bool "for" (Set (Var "b1")) "being" ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k18_turing_1 :::"ZeroTuring"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 4))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "b1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k17_turing_1 :::"Zero_Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Num 4)) ")" ) ")" )); theorem :: TURING_1:34 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set ($#k18_turing_1 :::"ZeroTuring"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set ($#k18_turing_1 :::"ZeroTuring"::: ) ) (Bool "for" (Set (Var "head")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 1)) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "head")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "head")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "head"))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_finseq_4 :::"*>"::: ) )) ")" ))))) ; theorem :: TURING_1:35 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 1))) "holds" (Bool (Set ($#k18_turing_1 :::"ZeroTuring"::: ) ) ($#r3_turing_1 :::"computes"::: ) (Set (Set (Var "n")) ($#k3_comput_1 :::"const"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; begin definitionfunc :::"U3(n)Tran"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 3) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k9_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 3) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k9_mcart_1 :::":]"::: ) ) equals :: TURING_1:def 20 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 3) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" )); end; :: deftheorem defines :::"U3(n)Tran"::: TURING_1:def 20 : (Bool (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" ($#k12_turing_1 :::"id"::: ) "(" (Set ($#k8_mcart_1 :::"[:"::: ) (Set "(" ($#k3_turing_1 :::"SegM"::: ) (Num 3) ")" ) "," (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) ) ($#k8_mcart_1 :::":]"::: ) ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) ) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) ($#k2_turing_1 :::".-->"::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) ) ")" ))); theorem :: TURING_1:36 (Bool "(" (Bool (Set (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Num 1) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Num 3) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_domain_1 :::"]"::: ) )) ")" ) ; definitionfunc :::"U3(n)Turing"::: -> ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) means :: TURING_1:def 21 (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 3))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Num 3)) ")" ); end; :: deftheorem defines :::"U3(n)Turing"::: TURING_1:def 21 : (Bool "for" (Set (Var "b1")) "being" ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k20_turing_1 :::"U3(n)Turing"::: ) )) "iff" (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k7_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k7_domain_1 :::"}"::: ) )) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_turing_1 :::"SegM"::: ) (Num 3))) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "b1"))) ($#r1_funct_2 :::"="::: ) (Set ($#k19_turing_1 :::"U3(n)Tran"::: ) )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Num 3)) ")" ) ")" )); theorem :: TURING_1:37 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set ($#k20_turing_1 :::"U3(n)Turing"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set ($#k20_turing_1 :::"U3(n)Turing"::: ) ) (Bool "for" (Set (Var "head")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_xxreal_0 :::">="::: ) (Num 3)) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set (Var "head")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "head")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "head")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "head")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 1) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 2) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Num 4) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Num 3) ")" ) ($#k2_finseq_4 :::"*>"::: ) )) ")" ))))) ; theorem :: TURING_1:38 (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">="::: ) (Num 3))) "holds" (Bool (Set ($#k20_turing_1 :::"U3(n)Turing"::: ) ) ($#r3_turing_1 :::"computes"::: ) (Set (Set (Var "n")) ($#k5_comput_1 :::"proj"::: ) (Num 3)))) ; begin definitionlet "t1", "t2" be ($#l1_turing_1 :::"TuringStr"::: ) ; func :::"UnionSt"::: "(" "t1" "," "t2" ")" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) equals :: TURING_1:def 22 (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "t1") "," (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "t2") ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "t1") ($#k6_domain_1 :::"}"::: ) ) "," (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" "t2") ($#k2_zfmisc_1 :::":]"::: ) )); end; :: deftheorem defines :::"UnionSt"::: TURING_1:def 22 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "t1"))) "," (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t2"))) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "t1"))) ($#k6_domain_1 :::"}"::: ) ) "," (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "t2"))) ($#k2_zfmisc_1 :::":]"::: ) )))); theorem :: TURING_1:39 (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t1"))) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t2"))) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" )) & (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "t1"))) "," (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "t2"))) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" )) ")" )) ; theorem :: TURING_1:40 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x")) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t"))) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" )))) ; theorem :: TURING_1:41 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "t")) "holds" (Bool (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s"))) "," (Set (Var "x")) ($#k1_domain_1 :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" )))) ; theorem :: TURING_1:42 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) (Bool "ex" (Set (Var "x1")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "x2")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "t")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k1_domain_1 :::"]"::: ) )))))) ; definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "x" be ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Const "s")); func :::"FirstTuringTran"::: "(" "s" "," "t" "," "x" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) equals :: TURING_1:def 23 (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" "x" ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "t") ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" "x" ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" "x" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"FirstTuringTran"::: TURING_1:def 23 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Var "s")) "holds" (Bool (Set ($#k22_turing_1 :::"FirstTuringTran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t"))) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) )))); definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "x" be ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Const "t")); func :::"SecondTuringTran"::: "(" "s" "," "t" "," "x" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) equals :: TURING_1:def 24 (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "s") "," (Set "(" "x" ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" "x" ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" "x" ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"SecondTuringTran"::: TURING_1:def 24 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Var "t")) "holds" (Bool (Set ($#k23_turing_1 :::"SecondTuringTran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s"))) "," (Set "(" (Set (Var "x")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "x")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) )))); definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Const "s")) "," (Set (Const "t")) ")" ); :: original: :::"`1"::: redefine func "x" :::"`1"::: -> ($#m1_subset_1 :::"State":::) "of" "s"; :: original: :::"`2"::: redefine func "x" :::"`2"::: -> ($#m1_subset_1 :::"State":::) "of" "t"; end; definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Const "s")) "," (Set (Const "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Const "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Const "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"FirstTuringState"::: "x" -> ($#m1_subset_1 :::"State":::) "of" "s" equals :: TURING_1:def 25 (Set (Set "(" "x" ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k24_turing_1 :::"`1"::: ) ); func :::"SecondTuringState"::: "x" -> ($#m1_subset_1 :::"State":::) "of" "t" equals :: TURING_1:def 26 (Set (Set "(" "x" ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k25_turing_1 :::"`2"::: ) ); end; :: deftheorem defines :::"FirstTuringState"::: TURING_1:def 25 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k26_turing_1 :::"FirstTuringState"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k24_turing_1 :::"`1"::: ) )))); :: deftheorem defines :::"SecondTuringState"::: TURING_1:def 26 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set ($#k27_turing_1 :::"SecondTuringState"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k2_domain_1 :::"`1"::: ) ")" ) ($#k25_turing_1 :::"`2"::: ) )))); definitionlet "X", "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set "(" (Set (Const "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set (Const "Z")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); given "u" being ($#m1_hidden :::"set"::: ) , "y" being ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Y")) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Const "u")) "," (Set (Const "y")) ($#k4_tarski :::"]"::: ) )) ; func :::"FirstTuringSymbol"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" "Y" equals :: TURING_1:def 27 (Set "x" ($#k3_domain_1 :::"`2"::: ) ); end; :: deftheorem defines :::"FirstTuringSymbol"::: TURING_1:def 27 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set (Var "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Z")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "ex" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))))) "holds" (Bool (Set ($#k28_turing_1 :::"FirstTuringSymbol"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_domain_1 :::"`2"::: ) )))); definitionlet "X", "Y", "Z" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "X")) "," (Set "(" (Set (Const "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set (Const "Z")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); given "u" being ($#m1_hidden :::"set"::: ) , "z" being ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "Z")) such that (Bool (Set (Const "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Const "u")) "," (Set (Const "z")) ($#k4_tarski :::"]"::: ) )) ; func :::"SecondTuringSymbol"::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" "Z" equals :: TURING_1:def 28 (Set "x" ($#k3_domain_1 :::"`2"::: ) ); end; :: deftheorem defines :::"SecondTuringSymbol"::: TURING_1:def 28 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" (Set (Var "Y")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Z")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "st" (Bool (Bool "ex" (Set (Var "u")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Z")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "u")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))))) "holds" (Bool (Set ($#k29_turing_1 :::"SecondTuringSymbol"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k3_domain_1 :::"`2"::: ) )))); definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Const "s")) "," (Set (Const "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Const "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Const "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ); func :::"Uniontran"::: "(" "s" "," "t" "," "x" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) equals :: TURING_1:def 29 (Set ($#k22_turing_1 :::"FirstTuringTran"::: ) "(" "s" "," "t" "," (Set "(" (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" "s") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k26_turing_1 :::"FirstTuringState"::: ) "x" ")" ) "," (Set "(" ($#k28_turing_1 :::"FirstTuringSymbol"::: ) "x" ")" ) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) if (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"State":::) "of" "s"(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" "s" "st" (Bool "(" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "t") ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "s")) ")" ))) (Set ($#k23_turing_1 :::"SecondTuringTran"::: ) "(" "s" "," "t" "," (Set "(" (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" "t") ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k27_turing_1 :::"SecondTuringState"::: ) "x" ")" ) "," (Set "(" ($#k29_turing_1 :::"SecondTuringSymbol"::: ) "x" ")" ) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" ) if (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" "t"(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" "t" "st" (Bool "x" ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "s") "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )))) otherwise (Set ($#k4_domain_1 :::"["::: ) (Set "(" "x" ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" "x" ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) ); end; :: deftheorem defines :::"Uniontran"::: TURING_1:def 29 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" "(" (Bool (Bool "ex" (Set (Var "p")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "s"))(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "s")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t"))) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s")))) ")" )))) "implies" (Bool (Set ($#k30_turing_1 :::"Uniontran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k22_turing_1 :::"FirstTuringTran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set "(" (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "s"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k26_turing_1 :::"FirstTuringState"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k28_turing_1 :::"FirstTuringSymbol"::: ) (Set (Var "x")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )) ")" & "(" (Bool (Bool "ex" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "t"))(Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "t")) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s"))) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) ))))) "implies" (Bool (Set ($#k30_turing_1 :::"Uniontran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k23_turing_1 :::"SecondTuringTran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set "(" (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "t"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" ($#k27_turing_1 :::"SecondTuringState"::: ) (Set (Var "x")) ")" ) "," (Set "(" ($#k29_turing_1 :::"SecondTuringSymbol"::: ) (Set (Var "x")) ")" ) ($#k1_domain_1 :::"]"::: ) ) ")" ) ")" )) ")" & "(" (Bool (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "s")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "s")) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "t"))) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) "or" "not" (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s")))) ")" )) ")" ) & (Bool "(" "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "t")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "t")) "holds" (Bool (Bool "not" (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "s"))) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )))) ")" )) "implies" (Bool (Set ($#k30_turing_1 :::"Uniontran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "(" (Set (Var "x")) ($#k2_domain_1 :::"`1"::: ) ")" ) "," (Set "(" (Set (Var "x")) ($#k3_domain_1 :::"`2"::: ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k4_domain_1 :::"]"::: ) )) ")" ")" ))); definitionlet "s", "t" be ($#l1_turing_1 :::"TuringStr"::: ) ; func :::"UnionTran"::: "(" "s" "," "t" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) means :: TURING_1:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" "s" "," "t" ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "s") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "t") ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k30_turing_1 :::"Uniontran"::: ) "(" "s" "," "t" "," (Set (Var "x")) ")" ))); end; :: deftheorem defines :::"UnionTran"::: TURING_1:def 30 : (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k3_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) "," (Set ($#k8_domain_1 :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k8_domain_1 :::"}"::: ) ) ($#k3_zfmisc_1 :::":]"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k31_turing_1 :::"UnionTran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ")" ) "," (Set "(" (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "s"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "t"))) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) "holds" (Bool (Set (Set (Var "b3")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k30_turing_1 :::"Uniontran"::: ) "(" (Set (Var "s")) "," (Set (Var "t")) "," (Set (Var "x")) ")" ))) ")" ))); definitionlet "T1", "T2" be ($#l1_turing_1 :::"TuringStr"::: ) ; func "T1" :::"';'"::: "T2" -> ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) means :: TURING_1:def 31 (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T1") ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" "T2"))) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" "T1" "," "T2" ")" )) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" it) ($#r1_funct_2 :::"="::: ) (Set ($#k31_turing_1 :::"UnionTran"::: ) "(" "T1" "," "T2" ")" )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "T1") "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" "T2") ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" it) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "T1") "," (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" "T2") ($#k1_domain_1 :::"]"::: ) )) ")" ); end; :: deftheorem defines :::"';'"::: TURING_1:def 31 : (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "b3")) "being" ($#v1_turing_1 :::"strict"::: ) ($#l1_turing_1 :::"TuringStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "T1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "T2")))) "iff" (Bool "(" (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "T1"))) ($#k2_xboole_0 :::"\/"::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "T2"))))) & (Bool (Set "the" ($#u2_turing_1 :::"FStates"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k21_turing_1 :::"UnionSt"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) & (Bool (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "b3"))) ($#r1_funct_2 :::"="::: ) (Set ($#k31_turing_1 :::"UnionTran"::: ) "(" (Set (Var "T1")) "," (Set (Var "T2")) ")" )) & (Bool (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T2"))) ($#k1_domain_1 :::"]"::: ) )) & (Bool (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T1"))) "," (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T2"))) ($#k1_domain_1 :::"]"::: ) )) ")" ) ")" ))); theorem :: TURING_1:43 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "T1")) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T1")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "T1"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )))) "holds" (Bool (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set "(" (Set (Var "T1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "T2")) ")" )) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "p")) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T2"))) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) "," (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T2"))) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) )))))) ; theorem :: TURING_1:44 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Tran-Goal":::) "of" (Set (Var "T2")) (Bool "for" (Set (Var "q")) "being" ($#m1_subset_1 :::"State":::) "of" (Set (Var "T2")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "T2")) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set (Var "T2"))) ($#k3_funct_2 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set (Var "q")) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )))) "holds" (Bool (Set (Set "the" ($#u3_turing_1 :::"Tran"::: ) "of" (Set "(" (Set (Var "T1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "T2")) ")" )) ($#k1_funct_1 :::"."::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T1"))) "," (Set (Var "q")) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "y")) ($#k1_domain_1 :::"]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set "the" ($#u5_turing_1 :::"AcceptS"::: ) "of" (Set (Var "T1"))) "," (Set "(" (Set (Var "g")) ($#k1_mcart_1 :::"`1_3"::: ) ")" ) ($#k1_domain_1 :::"]"::: ) ) "," (Set "(" (Set (Var "g")) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) )))))) ; theorem :: TURING_1:45 (Bool "for" (Set (Var "T1")) "," (Set (Var "T2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "s1")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "h")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "T1")) (Bool "for" (Set (Var "s2")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set (Var "T2")) (Bool "for" (Set (Var "s3")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set "(" (Set (Var "T1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "T2")) ")" ) "st" (Bool (Bool (Set (Var "s1")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Var "s1")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T1"))) "," (Set (Var "h")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "s2")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Var "s2")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set (Var "T2"))) "," (Set "(" (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s1")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ")" ) "," (Set "(" (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s1")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ")" ) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "s3")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set "the" ($#u4_turing_1 :::"InitS"::: ) "of" (Set "(" (Set (Var "T1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "T2")) ")" )) "," (Set (Var "h")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "s3")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s3")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s2")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) )) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s3")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s2")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) )) ")" ))))))) ; theorem :: TURING_1:46 (Bool "for" (Set (Var "tm1")) "," (Set (Var "tm2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "tm1")) "st" (Bool (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "tm1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "tm2"))))) "holds" (Bool (Set (Var "t")) "is" ($#m2_funct_2 :::"Tape":::) "of" (Set "(" (Set (Var "tm1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "tm2")) ")" )))) ; theorem :: TURING_1:47 (Bool "for" (Set (Var "tm1")) "," (Set (Var "tm2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set "(" (Set (Var "tm1")) ($#k32_turing_1 :::"';'"::: ) (Set (Var "tm2")) ")" ) "st" (Bool (Bool (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "tm1"))) ($#r1_hidden :::"="::: ) (Set "the" ($#u1_turing_1 :::"Symbols"::: ) "of" (Set (Var "tm2"))))) "holds" (Bool "(" (Bool (Set (Var "t")) "is" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "tm1"))) & (Bool (Set (Var "t")) "is" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "tm2"))) ")" ))) ; theorem :: TURING_1:48 (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "tm1")) "," (Set (Var "tm2")) "being" ($#l1_turing_1 :::"TuringStr"::: ) (Bool "for" (Set (Var "t1")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "tm1")) (Bool "for" (Set (Var "t2")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set (Var "tm2")) "st" (Bool (Bool (Set (Var "t1")) ($#r1_funct_2 :::"="::: ) (Set (Var "t2"))) & (Bool (Set (Var "t1")) ($#r2_turing_1 :::"storeData"::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "t2")) ($#r2_turing_1 :::"storeData"::: ) (Set (Var "f"))))))) ; theorem :: TURING_1:49 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"All-State":::) "of" (Set "(" (Set ($#k18_turing_1 :::"ZeroTuring"::: ) ) ($#k32_turing_1 :::"';'"::: ) (Set ($#k16_turing_1 :::"SuccTuring"::: ) ) ")" ) (Bool "for" (Set (Var "t")) "being" ($#m2_funct_2 :::"Tape":::) "of" (Set ($#k18_turing_1 :::"ZeroTuring"::: ) ) (Bool "for" (Set (Var "head")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set ($#k4_domain_1 :::"["::: ) (Set ($#k1_domain_1 :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k1_domain_1 :::"]"::: ) ) "," (Set (Var "head")) "," (Set (Var "t")) ($#k4_domain_1 :::"]"::: ) )) & (Bool (Set (Var "t")) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Set (Var "n")) ($#k2_finseq_4 :::"*>"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v2_turing_1 :::"Accept-Halt"::: ) ) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k2_mcart_1 :::"`2_3"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "head"))) & (Bool (Set (Set "(" ($#k11_turing_1 :::"Result"::: ) (Set (Var "s")) ")" ) ($#k3_mcart_1 :::"`3_3"::: ) ) ($#r2_turing_1 :::"storeData"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "head")) "," (Num 1) ($#k2_finseq_4 :::"*>"::: ) )) ")" )))) ;