:: SCM_COMP semantic presentation begin definitionfunc :::"SCM-AE"::: -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lang1 :::"strict"::: ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) means :: SCM_COMP:def 1 (Bool "(" (Bool (Set ($#k6_dtconstr :::"Terminals"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) & (Bool (Set ($#k7_dtconstr :::"NonTerminals"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Num 1) "," (Num 5) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Symbol":::) "of" it "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_pre_poly :::"*>"::: ) )) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Num 1) "," (Num 5) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) ")" ) ")" ); end; :: deftheorem defines :::"SCM-AE"::: SCM_COMP:def 1 : (Bool "for" (Set (Var "b1")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_lang1 :::"strict"::: ) ($#v1_dtconstr :::"with_terminals"::: ) ($#v2_dtconstr :::"with_nonterminals"::: ) ($#v3_dtconstr :::"with_useful_nonterminals"::: ) ($#v3_bintree1 :::"binary"::: ) ($#l1_lang1 :::"DTConstrStr"::: ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) "iff" (Bool "(" (Bool (Set ($#k6_dtconstr :::"Terminals"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_ami_2 :::"SCM-Data-Loc"::: ) )) & (Bool (Set ($#k7_dtconstr :::"NonTerminals"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Num 1) "," (Num 5) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set (Var "b1")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_pre_poly :::"*>"::: ) )) "iff" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Num 1) "," (Num 5) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ) ")" ) ")" ) ")" )); definitionmode bin-term is ($#m1_dtconstr :::"Element"::: ) "of" (Set ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) )); end; definitionlet "nt" be ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); let "tl", "tr" be ($#m1_dtconstr :::"bin-term":::); :: original: :::"-tree"::: redefine func "nt" :::"-tree"::: "(" "tl" "," "tr" ")" -> ($#m1_dtconstr :::"bin-term":::); end; definitionlet "t" be ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); :: original: :::"root-tree"::: redefine func :::"root-tree"::: "t" -> ($#m1_dtconstr :::"bin-term":::); end; definitionlet "t" be ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); func :::"@"::: "t" -> ($#m1_subset_1 :::"Data-Location":::) equals :: SCM_COMP:def 2 "t"; end; :: deftheorem defines :::"@"::: SCM_COMP:def 2 : (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set ($#k4_scm_comp :::"@"::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Var "t")))); theorem :: SCM_COMP:1 (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool "(" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) )) "or" (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) )) ")" )) ; theorem :: SCM_COMP:2 (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) ) "is" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) )) ")" ) ; definitionlet "t1", "t2" be ($#m1_dtconstr :::"bin-term":::); func "t1" :::"+"::: "t2" -> ($#m1_dtconstr :::"bin-term":::) equals :: SCM_COMP:def 3 (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" "t1" "," "t2" ")" ); func "t1" :::"-"::: "t2" -> ($#m1_dtconstr :::"bin-term":::) equals :: SCM_COMP:def 4 (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" "t1" "," "t2" ")" ); func "t1" :::"*"::: "t2" -> ($#m1_dtconstr :::"bin-term":::) equals :: SCM_COMP:def 5 (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" "t1" "," "t2" ")" ); func "t1" :::"div"::: "t2" -> ($#m1_dtconstr :::"bin-term":::) equals :: SCM_COMP:def 6 (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" "t1" "," "t2" ")" ); func "t1" :::"mod"::: "t2" -> ($#m1_dtconstr :::"bin-term":::) equals :: SCM_COMP:def 7 (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" "t1" "," "t2" ")" ); end; :: deftheorem defines :::"+"::: SCM_COMP:def 3 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set (Var "t1")) ($#k5_scm_comp :::"+"::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ))); :: deftheorem defines :::"-"::: SCM_COMP:def 4 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set (Var "t1")) ($#k6_scm_comp :::"-"::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ))); :: deftheorem defines :::"*"::: SCM_COMP:def 5 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set (Var "t1")) ($#k7_scm_comp :::"*"::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ))); :: deftheorem defines :::"div"::: SCM_COMP:def 6 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set (Var "t1")) ($#k8_scm_comp :::"div"::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ))); :: deftheorem defines :::"mod"::: SCM_COMP:def 7 : (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set (Var "t1")) ($#k9_scm_comp :::"mod"::: ) (Set (Var "t2"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) ) ($#k6_trees_4 :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ))); theorem :: SCM_COMP:3 (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool "(" (Bool "ex" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t"))))) "or" (Bool "ex" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) "st" (Bool "(" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tl")) ($#k5_scm_comp :::"+"::: ) (Set (Var "tr")))) "or" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tl")) ($#k6_scm_comp :::"-"::: ) (Set (Var "tr")))) "or" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tl")) ($#k7_scm_comp :::"*"::: ) (Set (Var "tr")))) "or" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tl")) ($#k8_scm_comp :::"div"::: ) (Set (Var "tr")))) "or" (Bool (Set (Var "term")) ($#r1_hidden :::"="::: ) (Set (Set (Var "tl")) ($#k9_scm_comp :::"mod"::: ) (Set (Var "tr")))) ")" )) ")" )) ; definitionlet "o" be ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); let "i", "j" be ($#m1_hidden :::"Integer":::); func "o" :::"-Meaning_on"::: "(" "i" "," "j" ")" -> ($#m1_hidden :::"Integer":::) equals :: SCM_COMP:def 8 (Set "i" ($#k2_xcmplx_0 :::"+"::: ) "j") if (Bool "o" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) )) (Set "i" ($#k6_xcmplx_0 :::"-"::: ) "j") if (Bool "o" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) )) (Set "i" ($#k3_xcmplx_0 :::"*"::: ) "j") if (Bool "o" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) (Set "i" ($#k5_int_1 :::"div"::: ) "j") if (Bool "o" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) )) (Set "i" ($#k6_int_1 :::"mod"::: ) "j") if (Bool "o" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) )) ; end; :: deftheorem defines :::"-Meaning_on"::: SCM_COMP:def 8 : (Bool "for" (Set (Var "o")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set (Set (Var "o")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "j")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set (Set (Var "o")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "j")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set (Set (Var "o")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "j")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set (Set (Var "o")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k5_int_1 :::"div"::: ) (Set (Var "j")))) ")" & "(" (Bool (Bool (Set (Var "o")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set (Set (Var "o")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k6_int_1 :::"mod"::: ) (Set (Var "j")))) ")" ")" ))); registrationlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); let "t" be ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); cluster (Set "s" ($#k1_funct_1 :::"."::: ) "t") -> ($#v1_int_1 :::"integer"::: ) ; end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k4_numbers :::"INT"::: ) ) "," (Set (Const "D")); let "x" be ($#m1_hidden :::"Integer":::); :: original: :::"."::: redefine func "f" :::"."::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; definitionlet "s" be ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ); let "term" be ($#m1_dtconstr :::"bin-term":::); func "term" :::"@"::: "s" -> ($#m1_hidden :::"Integer":::) means :: SCM_COMP:def 9 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) "term")) & (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set "s" ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "nt")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" )); end; :: deftheorem defines :::"@"::: SCM_COMP:def 9 : (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "term")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "term")))) & (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_numbers :::"INT"::: ) ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "nt")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" )) ")" )))); theorem :: SCM_COMP:4 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set (Var "t")))))) ; theorem :: SCM_COMP:5 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "nt")) ($#k10_scm_comp :::"-Meaning_on"::: ) "(" (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) "," (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ")" ))))) ; theorem :: SCM_COMP:6 (Bool "for" (Set (Var "s")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "tl")) ($#k5_scm_comp :::"+"::: ) (Set (Var "tr")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" (Set (Var "tl")) ($#k6_scm_comp :::"-"::: ) (Set (Var "tr")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" (Set (Var "tl")) ($#k7_scm_comp :::"*"::: ) (Set (Var "tr")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" (Set (Var "tl")) ($#k8_scm_comp :::"div"::: ) (Set (Var "tr")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ($#k5_int_1 :::"div"::: ) (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ))) & (Bool (Set (Set "(" (Set (Var "tl")) ($#k9_scm_comp :::"mod"::: ) (Set (Var "tr")) ")" ) ($#k12_scm_comp :::"@"::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "tl")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ) ($#k6_int_1 :::"mod"::: ) (Set "(" (Set (Var "tr")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")) ")" ))) ")" ))) ; definitionlet "nt" be ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); let "n" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"Selfwork"::: "(" "nt" "," "n" ")" -> ($#m1_hidden :::"XFinSequence":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) equals :: SCM_COMP:def 10 (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) if (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) )) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) if (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) )) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) if (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) )) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) if (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) )) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) "n" ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" "n" ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_afinsq_1 :::"%>"::: ) ) if (Bool "nt" ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) )) ; end; :: deftheorem defines :::"Selfwork"::: SCM_COMP:def 10 : (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k3_ami_3 :::"AddTo"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 1) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k4_ami_3 :::"SubFrom"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 2) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k5_ami_3 :::"MultBy"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 3) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" & "(" (Bool (Bool (Set (Var "nt")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Num 4) ($#k4_tarski :::"]"::: ) ))) "implies" (Bool (Set ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_afinsq_1 :::"<%"::: ) (Set "(" ($#k6_ami_3 :::"Divide"::: ) "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ")" ) "," (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k6_afinsq_1 :::"%>"::: ) )) ")" ")" ))); definitionfunc :::"SCM-Compile"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ")" ) means :: SCM_COMP:def 11 (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k4_scm_comp :::"@"::: ) (Set (Var "t")) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k15_afinsq_1 :::"^"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ")" ))) ")" ) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"SCM-Compile"::: SCM_COMP:def 11 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k14_scm_comp :::"SCM-Compile"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" ))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k4_scm_comp :::"@"::: ) (Set (Var "t")) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )) ")" ) ")" )) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "ex" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "," (Set "(" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) ($#k8_afinsq_1 :::"^omega"::: ) ")" ) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ))) & (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t1")))) & (Bool (Set (Var "f2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "b1")) ($#k3_funct_2 :::"."::: ) (Set (Var "t2")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f1")) ($#k3_funct_2 :::"."::: ) (Set (Var "n")) ")" ) ($#k15_afinsq_1 :::"^"::: ) (Set "(" (Set (Var "f2")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ")" ))) ")" ) ")" )))) ")" ) ")" ) ")" )); definitionlet "term" be ($#m1_dtconstr :::"bin-term":::); let "aux" be ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); func :::"SCM-Compile"::: "(" "term" "," "aux" ")" -> ($#m1_hidden :::"XFinSequence":::) "of" (Set "the" ($#u1_compos_1 :::"InstructionsF"::: ) "of" (Set ($#k1_ami_3 :::"SCM"::: ) )) equals :: SCM_COMP:def 12 (Set (Set "(" (Set ($#k14_scm_comp :::"SCM-Compile"::: ) ) ($#k3_funct_2 :::"."::: ) "term" ")" ) ($#k1_funct_1 :::"."::: ) "aux"); end; :: deftheorem defines :::"SCM-Compile"::: SCM_COMP:def 12 : (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "aux")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "term")) "," (Set (Var "aux")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k14_scm_comp :::"SCM-Compile"::: ) ) ($#k3_funct_2 :::"."::: ) (Set (Var "term")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "aux")))))); theorem :: SCM_COMP:7 (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "n")) ")" ) ($#k2_ami_3 :::":="::: ) (Set "(" ($#k4_scm_comp :::"@"::: ) (Set (Var "t")) ")" ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) )))) ; theorem :: SCM_COMP:8 (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "t1")) "," (Set (Var "t2")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t1")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "t2")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool (Set ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "t1")) "," (Set (Var "t2")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "t1")) "," (Set (Var "n")) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "t2")) "," (Set "(" (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ")" ) ")" ) ($#k1_ordinal4 :::"^"::: ) (Set "(" ($#k13_scm_comp :::"Selfwork"::: ) "(" (Set (Var "nt")) "," (Set (Var "n")) ")" ")" ))))))) ; definitionlet "t" be ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ); func :::"d"."::: "t" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCM_COMP:def 13 (Bool (Set ($#k10_ami_3 :::"dl."::: ) it) ($#r1_hidden :::"="::: ) "t"); end; :: deftheorem defines :::"d"."::: SCM_COMP:def 13 : (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k16_scm_comp :::"d"."::: ) (Set (Var "t")))) "iff" (Bool (Set ($#k10_ami_3 :::"dl."::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Var "t"))) ")" ))); definitionlet "term" be ($#m1_dtconstr :::"bin-term":::); func :::"max_Data-Loc_in"::: "term" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) means :: SCM_COMP:def 14 (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) "term")) & (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_scm_comp :::"d"."::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" )); end; :: deftheorem defines :::"max_Data-Loc_in"::: SCM_COMP:def 14 : (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "b2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "term")))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_dtconstr :::"TS"::: ) (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) ")" ) "," (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "term")))) & (Bool "(" "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_scm_comp :::"d"."::: ) (Set (Var "t")))) ")" ) & (Bool "(" "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "rtl")) "," (Set (Var "rtr")) "being" ($#m1_subset_1 :::"Symbol":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "st" (Bool (Bool (Set (Var "rtl")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tl")))) & (Bool (Set (Var "rtr")) ($#r1_hidden :::"="::: ) (Set ($#k1_bintree1 :::"root-label"::: ) (Set (Var "tr")))) & (Bool (Set (Var "nt")) ($#r1_lang1 :::"==>"::: ) (Set ($#k4_pre_poly :::"<*"::: ) (Set (Var "rtl")) "," (Set (Var "rtr")) ($#k4_pre_poly :::"*>"::: ) ))) "holds" (Bool "for" (Set (Var "xl")) "," (Set (Var "xr")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "xl")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tl")))) & (Bool (Set (Var "xr")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "tr"))))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set (Var "xl")) "," (Set (Var "xr")) ")" ))))) ")" ) ")" )) ")" ))); theorem :: SCM_COMP:9 (Bool "for" (Set (Var "t")) "being" ($#m2_subset_1 :::"Terminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) "holds" (Bool (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set "(" ($#k3_scm_comp :::"root-tree"::: ) (Set (Var "t")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_scm_comp :::"d"."::: ) (Set (Var "t"))))) ; theorem :: SCM_COMP:10 (Bool "for" (Set (Var "nt")) "being" ($#m2_subset_1 :::"NonTerminal":::) "of" (Set ($#k1_scm_comp :::"SCM-AE"::: ) ) (Bool "for" (Set (Var "tl")) "," (Set (Var "tr")) "being" ($#m1_dtconstr :::"bin-term":::) "holds" (Bool (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set "(" (Set (Var "nt")) ($#k2_scm_comp :::"-tree"::: ) "(" (Set (Var "tl")) "," (Set (Var "tr")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_nat_1 :::"max"::: ) "(" (Set "(" ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "tl")) ")" ) "," (Set "(" ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "tr")) ")" ) ")" )))) ; theorem :: SCM_COMP:11 (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "s1")) "," (Set (Var "s2")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "dn")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "dn")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "term"))))) "holds" (Bool (Set (Set (Var "s1")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "dn")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "s2")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "dn")) ")" ))) ")" )) "holds" (Bool (Set (Set (Var "term")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "term")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s2")))))) ; theorem :: SCM_COMP:12 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "aux")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "term")) "," (Set (Var "aux")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "s")) "being" (Set (Var "b4")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "aux")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "term"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) )(Bool "ex" (Set (Var "u")) "being" ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool "(" (Bool (Set (Var "u")) ($#r1_hidden :::"="::: ) (Set ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ) ")" )) & (Bool (Set (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "term")) "," (Set (Var "aux")) ")" ")" ))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set "(" ($#k5_extpro_1 :::"Comput"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) "," (Set (Var "i")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set (Var "i")))) & (Bool (Set ($#k5_memstr_0 :::"IC"::: ) (Set (Var "u"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "n")) ($#k2_nat_1 :::"+"::: ) (Set "(" (Set (Var "i")) ($#k2_nat_1 :::"+"::: ) (Num 1) ")" ))) & (Bool (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "aux")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "term")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")))) & (Bool "(" "for" (Set (Var "dn")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "dn")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "aux")))) "holds" (Bool (Set (Set (Var "s")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "dn")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "u")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k10_ami_3 :::"dl."::: ) (Set (Var "dn")) ")" ))) ")" ) ")" ))))))) ; theorem :: SCM_COMP:13 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Instruction-Sequence":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) (Bool "for" (Set (Var "term")) "being" ($#m1_dtconstr :::"bin-term":::) (Bool "for" (Set (Var "aux")) "," (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "term")) "," (Set (Var "aux")) ")" ")" ) ($#k1_ordinal4 :::"^"::: ) (Set ($#k5_afinsq_1 :::"<%"::: ) (Set "(" ($#k2_compos_1 :::"halt"::: ) (Set ($#k1_ami_3 :::"SCM"::: ) ) ")" ) ($#k5_afinsq_1 :::"%>"::: ) ) ")" ) "," (Set (Var "n")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "s")) "being" (Set (Var "b4")) ($#v5_memstr_0 :::"-started"::: ) ($#m1_hidden :::"State":::) "of" (Set ($#k1_ami_3 :::"SCM"::: ) ) "st" (Bool (Bool (Set (Var "aux")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k17_scm_comp :::"max_Data-Loc_in"::: ) (Set (Var "term"))))) "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."::: ) (Set (Var "aux")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "term")) ($#k12_scm_comp :::"@"::: ) (Set (Var "s")))) & (Bool (Set ($#k8_extpro_1 :::"LifeSpan"::: ) "(" (Set (Var "F")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_afinsq_1 :::"len"::: ) (Set "(" ($#k15_scm_comp :::"SCM-Compile"::: ) "(" (Set (Var "term")) "," (Set (Var "aux")) ")" ")" ))) ")" ))))) ;