:: FIB_FUSC semantic presentation begin definitionfunc :::"Fib_Program"::: -> ($#m1_hidden :::"XFinSequence":::) "of" equals :: FIB_FUSC:def 1 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k9_ami_3 :::">0_goto"::: ) (Num 2) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 1) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Num 3) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )); end; :: deftheorem defines :::"Fib_Program"::: FIB_FUSC:def 1 : (Bool (Set ($#k1_fib_fusc :::"Fib_Program"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k9_ami_3 :::">0_goto"::: ) (Num 2) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 1) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Num 3) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))); theorem :: FIB_FUSC:1 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k1_fib_fusc :::"Fib_Program"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Num 1) "," (Set (Var "N")) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k16_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & "(" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 6) ($#k4_nat_1 :::"*"::: ) (Set (Var "N")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 2))) ")" & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "N")))) ")" )))) ; definitionlet "i" be ($#m1_hidden :::"Integer":::); func :::"Fusc'"::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: FIB_FUSC:def 2 (Bool "(" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool "i" ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")))) ")" )) "or" (Bool "(" (Bool "i" "is" (Bool "not" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool it ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"Fusc'"::: FIB_FUSC:def 2 : (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_fib_fusc :::"Fusc'"::: ) (Set (Var "i")))) "iff" (Bool "(" (Bool "ex" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Var "n"))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")))) ")" )) "or" (Bool "(" (Bool (Set (Var "i")) "is" (Bool "not" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ))) & (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" ) ")" ) ")" ))); definitionfunc :::"Fusc_Program"::: -> ($#m1_hidden :::"XFinSequence":::) "of" equals :: FIB_FUSC:def 3 (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 8) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 6) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )); end; :: deftheorem defines :::"Fusc_Program"::: FIB_FUSC:def 3 : (Bool (Set ($#k3_fib_fusc :::"Fusc_Program"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 8) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 1) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 4) ")" ) ($#k8_ami_3 :::"=0_goto"::: ) (Num 6) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k7_ami_3 :::"SCM-goto"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ))); theorem :: FIB_FUSC:2 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k3_fib_fusc :::"Fusc_Program"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Num 2) "," (Set (Var "N")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k16_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N")))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" )))) ; theorem :: FIB_FUSC:3 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k1_fib_fusc :::"Fib_Program"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "N")) "," (Set (Var "k")) "," (Set (Var "Fk")) "," (Set (Var "Fk1")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Num 3) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Num 1) "," (Set (Var "N")) "," (Set (Var "Fk")) "," (Set (Var "Fk1")) ($#k16_afinsq_1 :::"%>"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "Fk")) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "k")))) & (Bool (Set (Var "Fk1")) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" )))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 6) ($#k4_nat_1 :::"*"::: ) (Set (Var "N")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 4))) & (Bool "ex" (Set (Var "m")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "m")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "k")) ($#k2_nat_1 :::"+"::: ) (Set (Var "N")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set (Var "m")))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_pre_ff :::"Fib"::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) ")" )) ")" )))) ; theorem :: FIB_FUSC:4 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k3_fib_fusc :::"Fusc_Program"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "n")) "," (Set (Var "N")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Num 2) "," (Set (Var "n")) "," (Set (Var "A")) "," (Set (Var "B")) ($#k16_afinsq_1 :::"%>"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "A")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "n")) ")" ) ")" ) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "B")) ($#k4_nat_1 :::"*"::: ) (Set "(" ($#k3_pre_ff :::"Fusc"::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N")))) & "(" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "n")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Num 2) "," (Set (Var "n")) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" ")" )))) ; theorem :: FIB_FUSC:5 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#v5_relat_1 :::"-valued"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k3_fib_fusc :::"Fusc_Program"::: ) ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "N")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "s")) "being" (Set ($#k6_numbers :::"0"::: ) ) ($#v5_memstr_0 :::"-started"::: ) ($#m1_scm_1 :::"State-consisting"::: ) "of" (Set ($#k16_afinsq_1 :::"<%"::: ) (Num 2) "," (Set (Var "N")) "," (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k16_afinsq_1 :::"%>"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r1_extpro_1 :::"halts_on"::: ) (Set (Var "s"))) & (Bool (Set (Set "(" ($#k6_extpro_1 :::"Result"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Num 3) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_pre_ff :::"Fusc"::: ) (Set (Var "N")))) & "(" (Bool (Bool (Set (Var "N")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Set (Var "N")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 6) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set ($#k1_int_1 :::"[\"::: ) (Set "(" ($#k5_power :::"log"::: ) "(" (Num 2) "," (Set (Var "N")) ")" ")" ) ($#k1_int_1 :::"/]"::: ) ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Num 1))) ")" ")" )))) ;