n1=sc(n0) n2=sc(n1) n3=sc(n2) n4=sc(n3) n5=sc(n4) n6=sc(n5) n7=sc(n6) n8=sc(n7) n9=sc(n8) n10=sc(n9) n11=sc(n10) n12=sc(n11) n13=sc(n12) n14=sc(n13) n15=sc(n14) n16=sc(n15) n17=sc(n16) n18=sc(n17) n19=sc(n18) n20=sc(n19) n21=sc(n20) n22=sc(n21) n23=sc(n22) n24=sc(n23) n25=sc(n24) n26=sc(n25) n27=sc(n26) n28=sc(n27) n29=sc(n28) n30=sc(n29) n31=sc(n30) n32=sc(n31) n33=sc(n32) n34=sc(n33) n35=sc(n34) n36=sc(n35) n37=sc(n36) n38=sc(n37) n39=sc(n38) n40=sc(n39) n41=sc(n40) n42=sc(n41) n43=sc(n42) n44=sc(n43) n45=sc(n44) n46=sc(n45) n47=sc(n46) n48=sc(n47) n49=sc(n48) n50=sc(n49) n51=sc(n50) n52=sc(n51) n53=sc(n52) n54=sc(n53) n55=sc(n54) n56=sc(n55) n57=sc(n56) n58=sc(n57) n59=sc(n58) n60=sc(n59) n61=sc(n60) n62=sc(n61) n63=sc(n62) n64=sc(n63) n65=sc(n64) n66=sc(n65) n67=sc(n66) n68=sc(n67) n69=sc(n68) n70=sc(n69) n71=sc(n70) n72=sc(n71) n73=sc(n72) n74=sc(n73) n75=sc(n74) n76=sc(n75) n77=sc(n76) n78=sc(n77) n79=sc(n78) n80=sc(n79) n81=sc(n80) n82=sc(n81) n83=sc(n82) n84=sc(n83) n85=sc(n84) n86=sc(n85) n87=sc(n86) n88=sc(n87) n89=sc(n88) n90=sc(n89) n91=sc(n90) n92=sc(n91) n93=sc(n92) n94=sc(n93) n95=sc(n94) n96=sc(n95) n97=sc(n96) n98=sc(n97) n99=sc(n98) n100=sc(n99) n101=sc(n100) n102=sc(n101) n103=sc(n102) n104=sc(n103) n105=sc(n104) n106=sc(n105) n107=sc(n106) n108=sc(n107) n109=sc(n108) n110=sc(n109) n111=sc(n110) n112=sc(n111) n113=sc(n112) n114=sc(n113) n115=sc(n114) n116=sc(n115) n117=sc(n116) n118=sc(n117) n119=sc(n118) n120=sc(n119) n121=sc(n120) n122=sc(n121) n123=sc(n122) n124=sc(n123) n125=sc(n124) n126=sc(n125) n127=sc(n126) n128=sc(n127) n129=sc(n128) n130=sc(n129) n131=sc(n130) n132=sc(n131) n133=sc(n132) n134=sc(n133) n135=sc(n134) n136=sc(n135) n137=sc(n136) n138=sc(n137) n139=sc(n138) n140=sc(n139) n141=sc(n140) n142=sc(n141) n143=sc(n142) n144=sc(n143) n145=sc(n144) n146=sc(n145) n147=sc(n146) n148=sc(n147) n149=sc(n148) n150=sc(n149) n151=sc(n150) n152=sc(n151) n153=sc(n152) n154=sc(n153) n155=sc(n154) n156=sc(n155) n157=sc(n156) n158=sc(n157) n159=sc(n158) n160=sc(n159) n161=sc(n160) n162=sc(n161) n163=sc(n162) n164=sc(n163) n165=sc(n164) n166=sc(n165) n167=sc(n166) n168=sc(n167) n169=sc(n168) n170=sc(n169) n171=sc(n170) n172=sc(n171) n173=sc(n172) n174=sc(n173) n175=sc(n174) n176=sc(n175) n177=sc(n176) n178=sc(n177) n179=sc(n178) n180=sc(n179) n181=sc(n180) n182=sc(n181) n183=sc(n182) n184=sc(n183) n185=sc(n184) n186=sc(n185) n187=sc(n186) n188=sc(n187) n189=sc(n188) n190=sc(n189) n191=sc(n190) n192=sc(n191) n193=sc(n192) n194=sc(n193) n195=sc(n194) n196=sc(n195) n197=sc(n196) n198=sc(n197) n199=sc(n198) n200=sc(n199) n201=sc(n200) n202=sc(n201) n203=sc(n202) n204=sc(n203) n205=sc(n204) n206=sc(n205) n207=sc(n206) n208=sc(n207) n209=sc(n208) n210=sc(n209) n211=sc(n210) n212=sc(n211) n213=sc(n212) n214=sc(n213) n215=sc(n214) n216=sc(n215) n217=sc(n216) n218=sc(n217) n219=sc(n218) n220=sc(n219) n221=sc(n220) n222=sc(n221) n223=sc(n222) n224=sc(n223) n225=sc(n224) n226=sc(n225) n227=sc(n226) n228=sc(n227) n229=sc(n228) n230=sc(n229) n231=sc(n230) n232=sc(n231) n233=sc(n232) n234=sc(n233) n235=sc(n234) n236=sc(n235) n237=sc(n236) n238=sc(n237) n239=sc(n238) n240=sc(n239) n241=sc(n240) n242=sc(n241) n243=sc(n242) n244=sc(n243) n245=sc(n244) n246=sc(n245) n247=sc(n246) n248=sc(n247) n249=sc(n248) n250=sc(n249) n251=sc(n250) n252=sc(n251) n253=sc(n252) n254=sc(n253) n255=sc(n254) n256=sc(n255) Definition of ac (antecessor function - with assert for 0): Python asserts: n!=0 ac(n0)= n0 ac(sc(n))= n Definition of acfull (antecessor function - without assert for 0): acfull(n0)= n0 acfull(sc(n))= n Definition of zero (1 for n=0, else 0): zero(n0)= n1 zero(sc(n))= n0 Definition of notzero (0 for n=0, else 1): notzero(n0)= n0 notzero(sc(n))= n1 Definition of minus_rev (proper subtraction b-a): minus_rev(n0,b)= b minus_rev(sc(a),b)= acfull(minus_rev(a,b)) Definition of minus (subtraction): Python asserts: a >= b Python fast computation: a-b minus(a,b)= minus_rev(b,a) Definition of minusfull (proper subtraction): Python fast computation: a-b if a >= b else 0 minusfull(a,b)= minus_rev(b,a) Definition of and_f (logical and): and_f(a,b)= mu(notzero(a),notzero(b)) Definition of and_f3 (logical and): and_f3(a1,a2,a3)= and_f(a1, and_f(a2, a3) ) Definition of and_f4 (logical and): and_f4(a1,a2,a3,a4)= and_f(a1, and_f3(a2,a3,a4)) Definition of and_f5 (logical and): and_f5(a1,a2,a3,a4,a5)= and_f(a1, and_f4(a2,a3,a4,a5)) Definition of and_f6 (logical and): and_f6(a1,a2,a3,a4,a5,a6)= and_f(a1, and_f5(a2,a3,a4,a5,a6)) Definition of and_f7 (logical and): and_f7(a1,a2,a3,a4,a5,a6,a7)= and_f(a1, and_f6(a2,a3,a4,a5,a6,a7)) Definition of and_f8 (logical and): and_f8(a1,a2,a3,a4,a5,a6,a7,a8)= and_f(a1, and_f7(a2,a3,a4,a5,a6,a7,a8)) Definition of and_f9 (logical and): and_f9(a1,a2,a3,a4,a5,a6,a7,a8,a9)= and_f(a1, and_f8(a2,a3,a4,a5,a6,a7,a8,a9)) Definition of and_f10 (logical and): and_f10(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10)= and_f(a1, and_f9(a2, a3, a4, a5, a6, a7, a8, a9, a10) ) Definition of or_f (logical or): or_f(a,b)= notzero(ad(a,b)) Definition of or_f3 (logical or): or_f3(a1,a2,a3)= or_f(a1, or_f(a2, a3) ) Definition of or_f4 (logical or): or_f4(a1,a2,a3,a4)= or_f(a1, or_f3(a2,a3,a4)) Definition of or_f5 (logical or): or_f5(a1,a2,a3,a4,a5)= or_f(a1, or_f4(a2,a3,a4,a5)) Definition of or_f6 (logical or): or_f6(a1,a2,a3,a4,a5,a6)= or_f(a1, or_f5(a2,a3,a4,a5,a6)) Definition of or_f7 (logical or): or_f7(a1,a2,a3,a4,a5,a6,a7)= or_f(a1, or_f6(a2,a3,a4,a5,a6,a7)) Definition of or_f8 (logical or): or_f8(a1,a2,a3,a4,a5,a6,a7,a8)= or_f(a1, or_f7(a2,a3,a4,a5,a6,a7,a8)) Definition of or_f9 (logical or): or_f9(a1,a2,a3,a4,a5,a6,a7,a8,a9)= or_f(a1, or_f8(a2,a3,a4,a5,a6,a7,a8,a9)) Definition of or_f10 (logical or): or_f10(a1,a2,a3,a4,a5,a6,a7,a8,a9,a10)= or_f(a1, or_f9(a2, a3, a4, a5, a6, a7, a8, a9, a10) ) Definition of not_f (logical not): not_f(a)= zero(a) Definition of cond (returns a if c != 0, else b): Python fast computation: b if c==0 else a cond(c,a,b)= ad(mu(notzero(c),a),mu(zero(c),b)) Definition of ifzero (returns a if a!=0, else b): ifzero(a,b)= cond(a, a, b) Definition of smallereq (a smaller or equal b): Python fast computation: 1 if a<=b else 0 smallereq(a,b)= zero(minusfull(a,b)) Definition of smaller (1 if a smaller b, else 0): Python fast computation: 1 if a < b else 0 smaller(a,b)= not_f(smallereq(b,a)) Definition of equal (1 if a==b, else 0): Python fast computation: 1 if a == b else 0 equal(a,b)= and_f( smallereq(a,b), smallereq(b,a)) Definition of relation_div (part of definition for div): relation_div(x,a,b)= zero(smallereq(mu(sc(x),b),a)) Definition of argmin_div (part of definition for div): argmin_div(n0,a,b)= n0 argmin_div(sc(x),a,b)= ifzero( argmin_div(x,a,b), cond( relation_div(sc(x),a,b), sc(x), n0) ) Definition of div (division): Python asserts: b!=0 Python fast computation: a / b div(a,b)= argmin_div(a,a,b) Definition of modulo (modulo operator): Python asserts: b!=0 Python fast computation: a % b modulo(a,b)= minus(a,mu(div(a,b),b)) Definition of pow_rev (b**a): Python fast computation: b**a pow_rev(n0,b)= n1 pow_rev(sc(a),b)= mu(b,pow_rev(a,b)) Definition of pow (a**b): pow(a,b)= pow_rev(b,a) Definition of rshift (right shift by b bytes): rshift(a,b)= div(a,pow(n2,mu(n8,b))) Definition of lshift (left shift by b bytes): lshift(a,b)= mu(a,pow(n2,mu(n8,b))) Definition of relation_length (part of definition for length): relation_length(y,x)= zero(rshift(x,y)) Definition of argmin_length (part of definition for length): argmin_length(n0,x)= n0 argmin_length(sc(y),x)= ifzero( argmin_length(y,x), cond( relation_length(sc(y),x), sc(y), n0) ) Definition of length (length of a string): length(x)= argmin_length(x,x) Definition of item (n-th character of a string): item(n,x)= cond( smallereq(n,length(x)), minusfull( rshift(x,minusfull(length(x),n)), lshift(rshift(x,sc(minusfull(length(x),n))),n1)) , n0) Definition of concat (concatenation of strings): concat(x,y)= ad(lshift(x,length(y)),y) Definition of concat3 (concatenation of strings): concat3(x1,x2,x3)= concat(x1,concat(x2,x3)) Definition of concat4 (concatenation of strings): concat4(x1,x2,x3,x4)= concat(x1,concat3(x2,x3,x4)) Definition of concat5 (concatenation of strings): concat5(x1,x2,x3,x4,x5)= concat(x1,concat4(x2,x3,x4,x5)) Definition of concat6 (concatenation of strings): concat6(x1,x2,x3,x4,x5,x6)= concat(x1,concat5(x2,x3,x4,x5,x6)) Definition of left (substring of x ending at position a): left(a,x)= rshift(x,minusfull(length(x),a)) Definition of right (substring of x starting at position a): Python asserts: a!=0 right(a,x)= minus(x,lshift(left(ac(a),x),minusfull(length(x),ac(a)))) Definition of slice (substring of x starting at position a and ending at position b): Python asserts: a!=0 slice(a,b,x)= left(minusfull(sc(b),a),right(a,x)) Definition of bitset (bit b of a is set (starting with bit 0)): bitset(a,b)= minus(div(a,pow(n2,b)),mu(div(a,pow(n2,sc(b))),n2)) Definition of bitslice (returns the number corresponding to bit b-c of a (from right to left starting with 0)): bitslice(a,b,c)= minusfull( div(a,pow(n2,b)), mu(div(a,pow(n2,sc(c))),pow(n2,minusfull(sc(c),b)))) Assume you want to define a primitive recursive relation r(x) like this: r(0) = expression returning 0 or 1 r(x) = expression returning 0 or 1 using r(a), r(b) where a,b < x This cannot be done with the primitive recursion scheme where r(x+1,...) is defined only in terms of r(x,...) - not some r(y,...) (y < x). This can be solved by defining a primitive recursive h(x) so that r(x) <-> bit x of h(x) is set. h(x) "codes" the information of r(y) for all values y <= x: h(0) = expression returning r(0) - which is 0 or 1 h(x+1) = h(x) + f(x+1,h(x))*(2**(x+1)) recursive_r(y,x) = bitset(y,x) f(x,y) = expression returning r(x) using recursive_r(y,a) where a < x Assume you want to define a primitive recursive function r(x) like this: r(0) = expression r(x) = expression using r(a), r(b) where a,b < x This is like the recursive relation r(x) mentioned above, but returns arbitrary values instead of 0 or 1. We can reduce this to primitice recursive functions by defining a function h that codes arbitrary values using several bits at once instead of a single bit. This is done by calculating the maximum length in bits of the result for any given input. bitstart(0) = 0 bitstart(x+1) = bitstart(x) + expression calculating length of r(x) in bits h(0) = expression calculating value for r(0) h(x+1) = h(x) + f(x+1,h(x))*(2**bitstart(x+1)) recursive_r(y,x) = bitslice(y,bitstart(x),bitstart(x+1)-1) f(x,y) = expression calculating the value for r(x) using recursive_r(y,a) where a < x r(x) = recursive_r(h(x),x) Definition of isalphalc (x is a-z): isalphalc(x)= and_f( smaller(n96,x), smaller(x,n123)) Definition of isalphauc (x is A-Z): isalphauc(x)= and_f( smaller(n64,x), smaller(x,n91)) Definition of isdigit (x is 0-9): isdigit(x)= and_f( smaller(n47,x), smaller(x,n58)) Definition of isalnumlc (x is a-z or 0-9 or _): isalnumlc(x)= or_f3(equal(x,n95),isalphalc(x),isdigit(x)) Definition of isalnumuc (x is A-Z or 0-9 or _): isalnumuc(x)= or_f3(equal(x,n95),isalphauc(x),isdigit(x)) Definition of recursive_isnamelc (part of definition for isnamelc): recursive_isnamelc(y,x)= bitset(y,x) Definition of f_isnamelc (part of definition for isnamelc): f_isnamelc(x,y)= or_f( isalphalc(x), and_f( isalnumlc(item(length(x),x)), recursive_isnamelc(y,slice(n1,ac(length(x)),x))) ) Definition of h_isnamelc (part of definition for isnamelc): h_isnamelc(n0)= n0 h_isnamelc(sc(x))= ad( h_isnamelc(x), mu(f_isnamelc(sc(x),h_isnamelc(x)),pow(n2,sc(x)))) Definition of isnamelc (lower case name [0-9,a-z,_] starting with a-z): isnamelc(x)= bitset(h_isnamelc(x),x) Definition of recursive_isnameuc (part of definition for isnameuc): recursive_isnameuc(y,x)= bitset(y,x) Definition of f_isnameuc (part of definition for isnameuc): f_isnameuc(x,y)= or_f( isalphauc(x), and_f( isalnumuc(item(length(x),x)), recursive_isnameuc(y,slice(n1,ac(length(x)),x))) ) Definition of h_isnameuc (part of definition for isnameuc): h_isnameuc(n0)= n0 h_isnameuc(sc(x))= ad( h_isnameuc(x), mu(f_isnameuc(sc(x),h_isnameuc(x)),pow(n2,sc(x)))) Definition of isnameuc (upper case name [0-9,A-Z,_] starting with A-Z): isnameuc(x)= bitset(h_isnameuc(x),x) Definition of relation_istermlist1 (part of definition for istermlist1): relation_istermlist1(pos,x,termcode,termlistcode)= and_f3( equal(item(pos,x),n44), recursive_istermlist_help(termlistcode, slice(n1,acfull(pos),x), termcode) , recursive_isterm(termcode,slice(sc(pos),length(x),x))) Definition of argmin_istermlist1 (part of definition for istermlist1): argmin_istermlist1(n0,x,termcode,termlistcode)= n0 argmin_istermlist1(sc(pos),x,termcode,termlistcode)= ifzero( argmin_istermlist1(pos,x,termcode,termlistcode), cond( relation_istermlist1(sc(pos),x,termcode,termlistcode), sc(pos), n0) ) Definition of istermlist1 (returns position of , if x has the form istermlist , isterm): istermlist1(x,termcode,termlistcode)= argmin_istermlist1( length(x), x, termcode, termlistcode) Definition of recursive_istermlist_help (part of definition for istermlist_help): recursive_istermlist_help(y,x,termcode)= bitset(y,x) Definition of f_istermlist_help (part of definition for istermlist_help): f_istermlist_help(x,termcode,y)= or_f( recursive_isterm(termcode,x), notzero(istermlist1(x,termcode,y))) Definition of h_istermlist_help (part of definition for istermlist_help): h_istermlist_help(n0,termcode)= n0 h_istermlist_help(sc(x),termcode)= ad( h_istermlist_help(x,termcode), mu( f_istermlist_help(sc(x),termcode,h_istermlist_help(x,termcode)), pow(n2,sc(x))) ) Definition of istermlist_help (x is a comma separated list of terms): istermlist_help(x,termcode)= bitset(h_istermlist_help(x,termcode),x) Definition of relation_isterm1 (part of definition for isterm1): relation_isterm1(pos,x,termcode)= and_f4( equal(item(length(x),x),n41), equal(item(pos,x),n40), isnamelc(slice(n1,acfull(pos),x)), istermlist_help(slice(sc(pos),acfull(length(x)),x),termcode)) Definition of argmin_isterm1 (part of definition for isterm1): argmin_isterm1(n0,x,termcode)= n0 argmin_isterm1(sc(pos),x,termcode)= ifzero( argmin_isterm1(pos,x,termcode), cond( relation_isterm1( sc(pos), x, termcode) , sc(pos), n0) ) Definition of isterm1 (returns position of ( if x has the form isnamelc ( istermlist )): isterm1(x,termcode)= argmin_isterm1(length(x),x,termcode) Definition of recursive_isterm (part of definition for isterm): recursive_isterm(y,x)= bitset(y,x) Definition of f_isterm (part of definition for isterm): f_isterm(x,y)= or_f( isnamelc(x), notzero(isterm1(x,y))) Definition of h_isterm (part of definition for isterm): h_isterm(n0)= n0 h_isterm(sc(x))= ad(h_isterm(x),mu(f_isterm(sc(x),h_isterm(x)),pow(n2,sc(x)))) Definition of isterm (x is a term): isterm(x)= bitset(h_isterm(x),x) Definition of relation_istermlist2 (part of definition for istermlist2): relation_istermlist2(pos,x,termlistcode)= and_f3( equal(item(pos,x),n44), recursive_istermlist(termlistcode,slice(n1,acfull(pos),x)), isterm(slice(sc(pos),length(x),x))) Definition of argmin_istermlist2 (part of definition for istermlist2): argmin_istermlist2(n0,x,termlistcode)= n0 argmin_istermlist2(sc(pos),x,termlistcode)= ifzero( argmin_istermlist2(pos,x,termlistcode), cond( relation_istermlist2(sc(pos),x,termlistcode), sc(pos), n0) ) Definition of istermlist2 (returns position of , if x has the form istermlist , isterm (using the now defined isterm)): istermlist2(x,termlistcode)= argmin_istermlist2(length(x),x,termlistcode) Definition of recursive_istermlist (part of definition for istermlist): recursive_istermlist(y,x)= bitset(y,x) Definition of f_istermlist (part of definition for istermlist): f_istermlist(x,y)= or_f( isterm(x), notzero(istermlist2(x,y))) Definition of h_istermlist (part of definition for istermlist): h_istermlist(n0)= n0 h_istermlist(sc(x))= ad( h_istermlist(x), mu(f_istermlist(sc(x),h_istermlist(x)),pow(n2,sc(x)))) Definition of istermlist (x is a comma separated list of terms (using the now defined isterm)): istermlist(x)= bitset(h_istermlist(x),x) Definition of relation_termlistpos (part of definition for termlistpos): relation_termlistpos(pos,x)= and_f4( equal(item(length(x),x),n41), equal(item(pos,x),n40), isnamelc(slice(n1,acfull(pos),x)), istermlist( slice( sc(pos), acfull(length(x)), x) ) ) Definition of argmin_termlistpos (part of definition for termlistpos): argmin_termlistpos(n0,x)= n0 argmin_termlistpos(sc(pos),x)= ifzero( argmin_termlistpos(pos,x), cond( relation_termlistpos(sc(pos),x), sc(pos), n0) ) Definition of termlistpos (returns position of ( if x has the form isnamelc ( istermlist )): termlistpos(x)= argmin_termlistpos(length(x),x) Definition of term_namelc (returns namelc if x has the form namelc ( termlist )): term_namelc(x)= cond( notzero(termlistpos(x)), slice(n1,acfull(termlistpos(x)),x), n0) Definition of term_termlist (returns termlist if x has the form namelc ( termlist )): term_termlist(x)= cond( notzero(termlistpos(x)), slice(sc(termlistpos(x)),acfull(length(x)),x), n0) Definition of relation_lasttermpos (part of definition for lasttermpos): relation_lasttermpos(pos,x)= and_f3( equal(item(pos,x),n44), istermlist(slice(n1,acfull(pos),x)), isterm(slice(sc(pos),length(x),x))) Definition of argmin_lasttermpos (part of definition for lasttermpos): argmin_lasttermpos(n0,x)= n0 argmin_lasttermpos(sc(pos),x)= ifzero( argmin_lasttermpos(pos,x), cond( relation_lasttermpos(sc(pos),x), sc(pos), n0) ) Definition of lasttermpos (returns position of , if x has the form termlist , term): lasttermpos(x)= argmin_lasttermpos(length(x),x) Definition of termlist_start (returns termlist if x has the form termlist, term): termlist_start(x)= cond( notzero(lasttermpos(x)), slice(n1,acfull(lasttermpos(x)),x), n0) Definition of termlist_end (returns term if x has the form termlist, term): termlist_end(x)= cond( notzero(lasttermpos(x)), slice(ad(n2,acfull(lasttermpos(x))),length(x),x), n0) Definition of relation_isproposition1 (part of definition for isproposition1): relation_isproposition1(pos,x)= and_f4( equal(item(length(x),x),n41), equal(item(pos,x),n40), isnameuc(slice(n1,acfull(pos),x)), istermlist( slice( sc(pos), acfull(length(x)), x) ) ) Definition of argmin_isproposition1 (part of definition for isproposition1): argmin_isproposition1(n0,x)= n0 argmin_isproposition1(sc(pos),x)= ifzero( argmin_isproposition1(pos,x), cond( relation_isproposition1( sc(pos), x) , sc(pos), n0) ) Definition of isproposition1 (returns position of ( if x has the form isnameuc ( termlist )): isproposition1(x)= argmin_isproposition1(length(x),x) Definition of isproposition (x is a proposition): isproposition(x)= notzero(isproposition1(x)) Definition of proposition_nameuc (returns nameuc if x has the form nameuc ( termlist )): proposition_nameuc(x)= cond( isproposition(x), slice(n1,acfull(isproposition1(x)),x), n0) Definition of proposition_termlist (returns termlist if x has the form nameuc ( termlist )): proposition_termlist(x)= cond( isproposition(x), slice(sc(isproposition1(x)),acfull(length(x)),x), n0) Definition of relation_isequation1 (part of definition for isequation1): relation_isequation1(pos,x)= and_f3( equal(item(pos,x),n61), isterm(slice(n1,acfull(pos),x)), isterm(slice(sc(pos),length(x),x))) Definition of argmin_isequation1 (part of definition for isequation1): argmin_isequation1(n0,x)= n0 argmin_isequation1(sc(pos),x)= ifzero( argmin_isequation1(pos,x), cond( relation_isequation1(sc(pos),x), sc(pos), n0) ) Definition of isequation1 (returns position of = if x has the form term = term): isequation1(x)= argmin_isequation1(length(x),x) Definition of isequation (x is an equation): isequation(x)= notzero(isequation1(x)) Definition of equation_term1 (returns term1 if x has the form term1 = term2): equation_term1(x)= cond( isequation(x), slice(n1,acfull(isequation1(x)),x), n0) Definition of equation_term2 (returns term2 if x has the form term1 = term2): equation_term2(x)= cond( isequation(x), slice(sc(isequation1(x)),length(x),x), n0) Definition of isnegation_help (x has the form ~ formula (is a negation)): isnegation_help(x,formulacode)= and_f( equal(item(n1,x),n126), recursive_isformula(formulacode, slice(n2, length(x), x) ) ) Definition of relation_isconjunction1_help (part of definition for isconjunction1_help): relation_isconjunction1_help(pos,x,formulacode)= and_f5( equal(item(n1,x),n40), equal(item(length(x),x),n41), equal(item(pos,x),n38), recursive_isformula(formulacode,slice(n2,acfull(pos),x)), recursive_isformula(formulacode, slice(ad(n2,acfull(pos)),acfull(length(x)),x)) ) Definition of argmin_isconjunction1_help (part of definition for isconjunction1_help): argmin_isconjunction1_help(n0,x,formulacode)= n0 argmin_isconjunction1_help(sc(pos),x,formulacode)= ifzero( argmin_isconjunction1_help(pos,x,formulacode), cond( relation_isconjunction1_help(sc(pos),x,formulacode), sc(pos), n0) ) Definition of isconjunction1_help (returns position of & if x has the form ( formula & formula )): isconjunction1_help(x,formulacode)= argmin_isconjunction1_help( length(x), x, formulacode) Definition of isconjunction_help (x is a conjunction): isconjunction_help(x,formulacode)= notzero(isconjunction1_help(x,formulacode)) Definition of relation_isgeneralization1_help (part of definition for isgeneralization1_help): relation_isgeneralization1_help(pos,x,formulacode)= and_f4( equal(item(n1,x),n33), equal(item(pos,x),n58), isnamelc(slice(n2,acfull(pos),x)), recursive_isformula(formulacode,slice(ad(n2,acfull(pos)),length(x),x))) Definition of argmin_isgeneralization1_help (part of definition for isgeneralization1_help): argmin_isgeneralization1_help(n0,x,formulacode)= n0 argmin_isgeneralization1_help(sc(pos),x,formulacode)= ifzero( argmin_isgeneralization1_help(pos,x,formulacode), cond( relation_isgeneralization1_help(sc(pos),x,formulacode), sc(pos), n0) ) Definition of isgeneralization1_help (returns position of : if x has the form ! isnamelc : formula): isgeneralization1_help(x,formulacode)= argmin_isgeneralization1_help(length(x),x,formulacode) Definition of isgeneralization_help (x is a generalization): isgeneralization_help(x,formulacode)= notzero(isgeneralization1_help(x,formulacode)) Definition of recursive_isformula (part of definition for isformula): recursive_isformula(y,x)= bitset(y,x) Definition of f_isformula (part of definition for isformula): f_isformula(x,y)= or_f5( isproposition(x), isequation(x), isnegation_help(x,y), isconjunction_help(x,y), isgeneralization_help(x,y)) Definition of h_isformula (part of definition for isformula): h_isformula(n0)= n0 h_isformula(sc(x))= ad( h_isformula(x), mu(f_isformula(sc(x),h_isformula(x)),pow(n2,sc(x)))) Definition of isformula (x is a formula (proposition|equation|negation|conjunction|generalization)): isformula(x)= bitset(h_isformula(x),x) Definition of isnegation (x has the form ~ formula (is a negation)): isnegation(x)= and_f( equal(item(n1,x),n126), isformula(slice(n2,length(x),x))) Definition of relation_isconjunction1 (part of definition for isconjunction1): relation_isconjunction1(pos,x)= and_f5( equal(item(n1,x),n40), equal(item(length(x),x),n41), equal(item(pos,x),n38), isformula(slice(n2,acfull(pos),x)), isformula( slice( ad(n2,acfull(pos)), acfull(length(x)), x) ) ) Definition of argmin_isconjunction1 (part of definition for isconjunction1): argmin_isconjunction1(n0,x)= n0 argmin_isconjunction1(sc(pos),x)= ifzero( argmin_isconjunction1(pos,x), cond( relation_isconjunction1( sc(pos), x) , sc(pos), n0) ) Definition of isconjunction1 (returns position of & if x has the form ( formula & formula )): isconjunction1(x)= argmin_isconjunction1(length(x),x) Definition of isconjunction (x is a conjunction): isconjunction(x)= notzero(isconjunction1(x)) Definition of relation_isgeneralization1 (part of definition for isgeneralization1): relation_isgeneralization1(pos,x)= and_f4( equal(item(n1,x),n33), equal(item(pos,x),n58), isnamelc(slice(n2,acfull(pos),x)), isformula( slice( ad(n2,acfull(pos)), length(x), x) ) ) Definition of argmin_isgeneralization1 (part of definition for isgeneralization1): argmin_isgeneralization1(n0,x)= n0 argmin_isgeneralization1(sc(pos),x)= ifzero( argmin_isgeneralization1(pos,x), cond( relation_isgeneralization1(sc(pos),x), sc(pos), n0) ) Definition of isgeneralization1 (returns position of : if x has the form ! isnamelc : formula): isgeneralization1(x)= argmin_isgeneralization1(length(x),x) Definition of isgeneralization (x is a generalization): isgeneralization(x)= notzero(isgeneralization1(x)) Definition of negation_formula (returns formula if x has the form ~ formula): negation_formula(x)= cond( isnegation(x), slice(n2,length(x),x), n0) Definition of conjunction_formula1 (returns formula1 if x has the form ( formula1 & formula2 )): conjunction_formula1(x)= cond( isconjunction(x), slice(n2,acfull(isconjunction1(x)),x), n0) Definition of conjunction_formula2 (returns formula2 if x has the form ( formula1 & formula2 )): conjunction_formula2(x)= cond( isconjunction(x), slice( ad(n2,acfull(isconjunction1(x))), acfull(length(x)), x) , n0) Definition of generalization_namelc (returns namelc if x has the form ! isnamelc : formula): generalization_namelc(x)= cond( isgeneralization(x), slice(n2,acfull(isgeneralization1(x)),x), n0) Definition of generalization_formula (returns formula if x has the form ! isnamelc : formula): generalization_formula(x)= cond( isgeneralization(x), slice( ad(n2,acfull(isgeneralization1(x))), length(x), x) , n0) Definition of getsuccx (returns sc(x) as term (x is supposed to be a term)): getsuccx(x)= concat5(n115,n99,n40,x,n41) Definition of number (returns x as term expressed with n0 and sc()): number(n0)= concat(n110,n48) number(sc(x))= getsuccx(number(x)) Definition of isfreeinterm_help (variable x is free in term t): isfreeinterm_help(freeintermlistcode,x,t)= and_f( isterm(t), or_f( equal(x,t), recursive_isfreeintermlist(freeintermlistcode,term_termlist(t),x)) ) Definition of recursive_isfreeintermlist (part of definition for isfreeintermlist): recursive_isfreeintermlist(y,termlist,x)= bitset(y,termlist) Definition of f_isfreeintermlist (part of definition for isfreeintermlist): f_isfreeintermlist(termlist,x,y)= or_f3( isfreeinterm_help(y,x,termlist), recursive_isfreeintermlist(y,termlist_start(termlist),x), isfreeinterm_help(y,x,termlist_end(termlist))) Definition of h_isfreeintermlist (part of definition for isfreeintermlist): h_isfreeintermlist(n0,x)= n0 h_isfreeintermlist(sc(termlist),x)= ad( h_isfreeintermlist(termlist,x), mu( f_isfreeintermlist(sc(termlist),x,h_isfreeintermlist(termlist,x)), pow(n2,sc(termlist))) ) Definition of isfreeintermlist (x is a free variable of termlist): isfreeintermlist(termlist,x)= bitset(h_isfreeintermlist(termlist,x),termlist) Definition of isfreeinterm (variable x is free in term t): isfreeinterm(t,x)= and_f( isterm(t), or_f( equal(x,t), isfreeintermlist(term_termlist(t),x)) ) Definition of isfreeinproposition (variable x is free in proposition t): isfreeinproposition(t,x)= isfreeintermlist(proposition_termlist(t),x) Definition of isfreeinequation (variable x is free in equation t): isfreeinequation(t,x)= or_f( isfreeinterm(equation_term1(t),x), isfreeinterm(equation_term2(t),x)) Definition of isfreeinnegation (variable y is free in negation x): isfreeinnegation(x,y,isfreeinformulacode)= recursive_isfreeinformula(isfreeinformulacode,negation_formula(x),y) Definition of isfreeinconjunction (variable y is free in conjunction x): isfreeinconjunction(x,y,isfreeinformulacode)= or_f( recursive_isfreeinformula(isfreeinformulacode,conjunction_formula1(x),y), recursive_isfreeinformula(isfreeinformulacode,conjunction_formula2(x),y)) Definition of isfreeingeneralization (variable y is free in generalization x): isfreeingeneralization(x,y,isfreeinformulacode)= and_f( not_f(equal(generalization_namelc(x),y)), recursive_isfreeinformula(isfreeinformulacode, generalization_formula(x), y) ) Definition of recursive_isfreeinformula (part of definition for isfreeinformula): recursive_isfreeinformula(y,x,z)= bitset(y,x) Definition of f_isfreeinformula (part of definition for isfreeinformula): f_isfreeinformula(x,z,y)= and_f( isformula(x), or_f5( isfreeinproposition(x,z), isfreeinequation(x,z), isfreeinnegation(x,z,y), isfreeinconjunction(x,z,y), isfreeingeneralization(x,z,y)) ) Definition of h_isfreeinformula (part of definition for isfreeinformula): h_isfreeinformula(n0,z)= n0 h_isfreeinformula(sc(x),z)= ad( h_isfreeinformula(x,z), mu( f_isfreeinformula( sc(x), z, h_isfreeinformula(x,z)) , pow(n2,sc(x))) ) Definition of isfreeinformula (variable z is free in formula x): isfreeinformula(x,z)= bitset(h_isfreeinformula(x,z),x) Definition of subst_term_help (return substitution of t for x in term n): subst_term_help(subst_termlistcode,n,x,t)= cond( isterm(n), cond( isnamelc(n), cond( equal(n,x), t, n) , concat( term_namelc(n), concat(n40, concat( recursive_subst_termlist(subst_termlistcode, term_termlist(n), x, t) , n41) ) ) ) , n0) Definition of bitstart_subst_termlist (part of definition for subst_termlist): bitstart_subst_termlist(n0,x,t)= n0 bitstart_subst_termlist(sc(n),x,t)= ad( sc(mu(n8,mu(length(n),length(t)))), bitstart_subst_termlist(n,x,t)) Definition of recursive_subst_termlist (part of definition for subst_termlist): recursive_subst_termlist(y,n,x,t)= bitslice(y, bitstart_subst_termlist(n,x,t), acfull(bitstart_subst_termlist(sc(n),x,t))) Definition of f_subst_termlist (part of definition for subst_termlist): f_subst_termlist(n,x,t,y)= cond( and_f3(isnamelc(x),isterm(t),istermlist(n)), cond( isterm(n), subst_term_help(y,n,x,t), concat3( recursive_subst_termlist(y,termlist_start(n),x,t), n44, subst_term_help(y,termlist_end(n),x,t)) ) , n0) Definition of h_subst_termlist (part of definition for subst_termlist): h_subst_termlist(n0,x,t)= n0 h_subst_termlist(sc(n),x,t)= ad( h_subst_termlist(n,x,t), mu( f_subst_termlist( sc(n), x, t, h_subst_termlist(n,x,t)) , pow(n2,bitstart_subst_termlist(sc(n),x,t))) ) Definition of subst_termlist (returns substitution of t for x in termlist n): subst_termlist(n,x,t)= recursive_subst_termlist(h_subst_termlist(n,x,t),n,x,t) Definition of subst_term (returns substitution of t for x in term n): subst_term(n,x,t)= cond( isterm(n), cond( isnamelc(n), cond( equal(n,x), t, n) , concat4( term_namelc(n), n40, subst_termlist(term_termlist(n),x,t), n41) ) , n0) Definition of subst_proposition (returns substitution of t for x in proposition n): subst_proposition(n,x,t)= cond( isproposition(n), concat4( proposition_nameuc(n), n40, subst_termlist( proposition_termlist(n), x, t) , n41) , n0) Definition of subst_equation (returns substitution of t for x in equation n): subst_equation(n,x,t)= cond( isequation(n), concat3( subst_term(equation_term1(n),x,t), n61, subst_term(equation_term2(n),x,t)) , n0) Definition of subst_negation (return substitution of t for x in negation n): subst_negation(subst_formulacode,n,x,t)= cond( isnegation(n), concat(n126, recursive_subst_formula(subst_formulacode, negation_formula(n), x, t) ) , n0) Definition of subst_conjunction (returns substitution of t for x in conjunction n): subst_conjunction(subst_formulacode,n,x,t)= cond( isconjunction(n), concat5(n40, recursive_subst_formula(subst_formulacode, conjunction_formula1(n), x, t) , n38, recursive_subst_formula(subst_formulacode, conjunction_formula2(n), x, t) , n41) , n0) Definition of subst_generalization (returns substitution of t for x in generalization n): subst_generalization(subst_formulacode,n,x,t)= cond( isgeneralization(n), cond( isfreeinformula(n,x), cond( isfreeinterm(t,generalization_namelc(n)), n0, concat4(n33, generalization_namelc(n), n58, recursive_subst_formula(subst_formulacode, generalization_formula(n), x, t) ) ) , n) , n0) Definition of bitstart_subst_formula (part of definition for subst_formula): bitstart_subst_formula(n0,x,t)= n0 bitstart_subst_formula(sc(n),x,t)= ad( sc(mu(n8,mu(length(n),length(t)))), bitstart_subst_formula(n,x,t)) Definition of recursive_subst_formula (part of definition for subst_formula): recursive_subst_formula(y,n,x,t)= bitslice(y, bitstart_subst_formula(n,x,t), acfull( bitstart_subst_formula( sc(n), x, t) ) ) Definition of f_subst_formula (part of definition for subst_formula): f_subst_formula(n,x,t,y)= cond( and_f3(isnamelc(x),isterm(t),isformula(n)), ad( subst_proposition(n,x,t), ad( subst_equation(n,x,t), ad( subst_negation(y,n,x,t), ad( subst_conjunction(y,n,x,t), subst_generalization(y,n,x,t)) ) ) ) , n0) Definition of h_subst_formula (part of definition for subst_formula): h_subst_formula(n0,x,t)= n0 h_subst_formula(sc(n),x,t)= ad( h_subst_formula(n,x,t), mu( f_subst_formula( sc(n), x, t, h_subst_formula(n,x,t)) , pow(n2,bitstart_subst_formula(sc(n),x,t))) ) Definition of subst_formula (returns substitution of t for x in formula n): subst_formula(n,x,t)= recursive_subst_formula(h_subst_formula(n,x,t),n,x,t) Definition of relation_find_pos (part of definition for find_pos): relation_find_pos(y,a,x,p)= and_f( equal(item(y,x),a), smaller(p,y)) Definition of argmin_find_pos (part of definition for find_pos): argmin_find_pos(n0,a,x,p)= n0 argmin_find_pos(sc(y),a,x,p)= ifzero( argmin_find_pos(y,a,x,p), cond( relation_find_pos(sc(y),a,x,p), sc(y), n0) ) Definition of find_pos (position of occurence of a in x, starting with p+1 - 0 if not found): find_pos(a,x,p)= argmin_find_pos(length(x),a,x,p) Definition of find (position of nth occurence of a in x - 0 if not found): find(n0,a,x)= n0 find(sc(n),a,x)= find_pos(a,x,find(n,a,x)) Definition of relation_occur (part of definition for occur): relation_occur(n,a,x)= zero(find(sc(n),a,x)) Definition of argmin_occur (part of definition for occur): argmin_occur(n0,a,x)= n0 argmin_occur(sc(n),a,x)= ifzero( argmin_occur(n,a,x), cond( relation_occur(sc(n),a,x), sc(n), n0) ) Definition of occur (how often character a occurs in x): occur(a,x)= argmin_occur(length(x),a,x) Definition of sitem (nth statement in formula sequence x delimited by ;): sitem(n,x)= slice(sc(find(acfull(n),n59,x)),acfull(find(n,n59,x)),x) Definition of slength (length of sequence n): slength(n)= occur(n59,n) Definition of sequence_end (returns last item of a sequence): sequence_end(n)= sitem(slength(n),n) Definition of sequence_start (returns all but last item of a sequence, 0 if sequence has length 1): sequence_start(n)= slice(n1,find(acfull(slength(n)),n59,n),n) Definition of recursive_issequence (part of definition for issequence): recursive_issequence(y,n)= bitset(y,n) Definition of f_issequence (part of definition for issequence): f_issequence(n,y)= and_f3( equal(item(length(n),n),n59), isformula(sequence_end(n)), or_f( zero(sequence_start(n)), recursive_issequence(y,sequence_start(n))) ) Definition of h_issequence (part of definition for issequence): h_issequence(n0)= n0 h_issequence(sc(n))= ad( h_issequence(n), mu(f_issequence(sc(n),h_issequence(n)),pow(n2,sc(n)))) Definition of issequence (n is a valid nonempty sequence of formulae ending with ;): issequence(n)= bitset(h_issequence(n),n) Definition of recursive_freeinsequence (part of definition for freeinsequence): recursive_freeinsequence(y,n,x)= bitset(y,n) Definition of f_freeinsequence (part of definition for freeinsequence): f_freeinsequence(n,x,y)= or_f( isfreeinformula(sequence_end(n),x), recursive_freeinsequence(y,sequence_start(n),x)) Definition of h_freeinsequence (part of definition for freeinsequence): h_freeinsequence(n0,x)= n0 h_freeinsequence(sc(n),x)= ad( h_freeinsequence(n,x), mu( f_freeinsequence( sc(n), x, h_freeinsequence(n,x)) , pow(n2,sc(n))) ) Definition of freeinsequence (x is free in sequence n): freeinsequence(n,x)= bitset(h_freeinsequence(n,x),n) Definition of leftfromslash (return string1 if x has the form string1 / string2): leftfromslash(x)= cond( smaller(find_pos(n47,x,n0),length(x)), slice(n1,acfull(find_pos(n47,x,n0)),x), n0) Definition of rightfromslash (return string2 if x has the form string1 / string2): rightfromslash(x)= cond( smaller(n1,find_pos(n47,x,n0)), slice(sc(find_pos(n47,x,n0)),length(x),x), n0) Definition of recombine (return a / b): recombine(a,b)= cond( and_f( notzero(a), notzero(b)) , concat(concat(a,n47),b), n0) Definition of recursive_subst_sequence (part of definition for subst_sequence): recursive_subst_sequence(y,n,x,t)= bitset(y,n) Definition of f_subst_sequence (part of definition for subst_sequence): f_subst_sequence(n,x,t,y)= and_f4( issequence(leftfromslash(n)), issequence(rightfromslash(n)), equal( subst_formula(sequence_end(leftfromslash(n)),x,t), sequence_end(rightfromslash(n))) , or_f( and_f( zero(sequence_start(leftfromslash(n))), zero(sequence_start(rightfromslash(n)))) , recursive_subst_sequence(y, recombine( sequence_start( leftfromslash(n)) , sequence_start( rightfromslash(n)) ) , x, t) ) ) Definition of h_subst_sequence (part of definition for subst_sequence): h_subst_sequence(n0,x,t)= n0 h_subst_sequence(sc(n),x,t)= ad( h_subst_sequence(n,x,t), mu( f_subst_sequence( sc(n), x, t, h_subst_sequence(n,x,t)) , pow(n2,sc(n))) ) Definition of subst_sequence (n has the form sequence1 / sequence2 and sequence2 is a substitution of t for x in sequence1): subst_sequence(n,x,t)= bitset(h_subst_sequence(n,x,t),n) Definition of recursive_subst_sequence_termlist1 (part of definition for subst_sequence_termlist1): recursive_subst_sequence_termlist1(y,t,n,x)= bitset(y,t) Definition of f_subst_sequence_termlist1 (part of definition for subst_sequence_termlist1): f_subst_sequence_termlist1(t,n,x,y)= cond( isterm(t), or_f( subst_sequence(n,x,t), recursive_subst_sequence_termlist1(y,term_termlist(t),n,x)) , or_f3( subst_sequence(n,x,termlist_end(t)), recursive_subst_sequence_termlist1(y, term_termlist(termlist_end(t)), n, x) , recursive_subst_sequence_termlist1(y,termlist_start(t),n,x)) ) Definition of h_subst_sequence_termlist1 (part of definition for subst_sequence_termlist1): h_subst_sequence_termlist1(n0,n,x)= n0 h_subst_sequence_termlist1(sc(t),n,x)= ad( h_subst_sequence_termlist1(t,n,x), mu( f_subst_sequence_termlist1(sc(t),n,x,h_subst_sequence_termlist1(t,n,x)), pow(n2,sc(t))) ) Definition of subst_sequence_termlist1 (returns 1 if subst_sequence(n,x,t1) for any term t1 in t): subst_sequence_termlist1(t,n,x)= bitset(h_subst_sequence_termlist1(t,n,x),t) Definition of recursive_subst_sequence_formula1 (part of definition for subst_sequence_formula1): recursive_subst_sequence_formula1(y,f,n,x)= bitset(y,f) Definition of f_subst_sequence_formula1 (part of definition for subst_sequence_formula1): f_subst_sequence_formula1(f,n,x,y)= or_f7( subst_sequence_termlist1(proposition_termlist(f),n,x), subst_sequence_termlist1(equation_term1(f),n,x), subst_sequence_termlist1(equation_term2(f),n,x), recursive_subst_sequence_formula1(y,negation_formula(f),n,x), recursive_subst_sequence_formula1(y,conjunction_formula1(f),n,x), recursive_subst_sequence_formula1(y,conjunction_formula2(f),n,x), recursive_subst_sequence_formula1(y,generalization_formula(f),n,x)) Definition of h_subst_sequence_formula1 (part of definition for subst_sequence_formula1): h_subst_sequence_formula1(n0,n,x)= n0 h_subst_sequence_formula1(sc(f),n,x)= ad( h_subst_sequence_formula1(f,n,x), mu( f_subst_sequence_formula1(sc(f),n,x,h_subst_sequence_formula1(f,n,x)), pow(n2,sc(f))) ) Definition of subst_sequence_formula1 (returns 1 if subst_sequence(n,x,t1) for any term t1 in f): subst_sequence_formula1(f,n,x)= bitset(h_subst_sequence_formula1(f,n,x),f) Definition of recursive_subst_sequence_sequence1 (part of definition for subst_sequence_sequence1): recursive_subst_sequence_sequence1(y,s,n,x)= bitset(y,s) Definition of f_subst_sequence_sequence1 (part of definition for subst_sequence_sequence1): f_subst_sequence_sequence1(s,n,x,y)= or_f( subst_sequence_formula1(sequence_end(s),n,x), recursive_subst_sequence_sequence1(y,sequence_start(s),n,x)) Definition of h_subst_sequence_sequence1 (part of definition for subst_sequence_sequence1): h_subst_sequence_sequence1(n0,n,x)= n0 h_subst_sequence_sequence1(sc(s),n,x)= ad( h_subst_sequence_sequence1(s,n,x), mu( f_subst_sequence_sequence1(sc(s),n,x,h_subst_sequence_sequence1(s,n,x)), pow(n2,sc(s))) ) Definition of subst_sequence_sequence1 (returns 1 if subst_sequence(n,x,t1) for any term t1 in s): subst_sequence_sequence1(s,n,x)= bitset(h_subst_sequence_sequence1(s,n,x),s) Definition of recursive_subst_sequence_termlist (part of definition for subst_sequence_termlist): recursive_subst_sequence_termlist(y,t,s,n)= bitset(y,t) Definition of f_subst_sequence_termlist (part of definition for subst_sequence_termlist): f_subst_sequence_termlist(t,s,n,y)= cond( isterm(t), or_f( subst_sequence_sequence1(s,n,t), recursive_subst_sequence_termlist(y,term_termlist(t),s,n)) , or_f3( subst_sequence_sequence1(s,n,termlist_end(t)), recursive_subst_sequence_termlist(y, term_termlist(termlist_end(t)), s, n) , recursive_subst_sequence_termlist(y,termlist_start(t),s,n)) ) Definition of h_subst_sequence_termlist (part of definition for subst_sequence_termlist): h_subst_sequence_termlist(n0,s,n)= n0 h_subst_sequence_termlist(sc(t),s,n)= ad( h_subst_sequence_termlist(t,s,n), mu( f_subst_sequence_termlist(sc(t),s,n,h_subst_sequence_termlist(t,s,n)), pow(n2,sc(t))) ) Definition of subst_sequence_termlist (returns 1 if subst_sequence_sequence1(s,n,x) for any variable x in t): subst_sequence_termlist(t,s,n)= bitset(h_subst_sequence_termlist(t,s,n),t) Definition of recursive_subst_sequence_formula (part of definition for subst_sequence_formula): recursive_subst_sequence_formula(y,f,s,n)= bitset(y,f) Definition of f_subst_sequence_formula (part of definition for subst_sequence_formula): f_subst_sequence_formula(f,s,n,y)= or_f7( subst_sequence_termlist(proposition_termlist(f),s,n), subst_sequence_termlist(equation_term1(f),s,n), subst_sequence_termlist(equation_term2(f),s,n), recursive_subst_sequence_formula(y,negation_formula(f),s,n), recursive_subst_sequence_formula(y,conjunction_formula1(f),s,n), recursive_subst_sequence_formula(y,conjunction_formula2(f),s,n), recursive_subst_sequence_formula(y,generalization_formula(f),s,n)) Definition of h_subst_sequence_formula (part of definition for subst_sequence_formula): h_subst_sequence_formula(n0,s,n)= n0 h_subst_sequence_formula(sc(f),s,n)= ad( h_subst_sequence_formula(f,s,n), mu( f_subst_sequence_formula(sc(f),s,n,h_subst_sequence_formula(f,s,n)), pow(n2,sc(f))) ) Definition of subst_sequence_formula (returns 1 if subst_sequence_sequence1(s,n,x) for any variable x in f): subst_sequence_formula(f,s,n)= bitset(h_subst_sequence_formula(f,s,n),f) Definition of recursive_subst_sequence_sequence (part of definition for subst_sequence_sequence): recursive_subst_sequence_sequence(y,s,s1,n)= bitset(y,s) Definition of f_subst_sequence_sequence (part of definition for subst_sequence_sequence): f_subst_sequence_sequence(s,s1,n,y)= or_f( subst_sequence_formula(sequence_end(s),s1,n), recursive_subst_sequence_sequence(y,sequence_start(s),s1,n)) Definition of h_subst_sequence_sequence (part of definition for subst_sequence_sequence): h_subst_sequence_sequence(n0,s1,n)= n0 h_subst_sequence_sequence(sc(s),s1,n)= ad( h_subst_sequence_sequence(s,s1,n), mu( f_subst_sequence_sequence(sc(s),s1,n,h_subst_sequence_sequence(s,s1,n)), pow(n2,sc(s))) ) Definition of subst_sequence_sequence (returns 1 if subst_sequence_sequence1(s1,n,x) for any variable x in s): subst_sequence_sequence(s,s1,n)= bitset(h_subst_sequence_sequence(s,s1,n),s) Definition of subst_sequence_any (returns 1 if sequence2 is a substitution of any term in sequence2 for any variable in sequence 1): subst_sequence_any(sequence1,sequence2)= subst_sequence_sequence(sequence1,sequence2,recombine(sequence1,sequence2)) Definition of recursive_isinsequence (part of definition for isinsequence): recursive_isinsequence(y,s,f)= bitset(y,s) Definition of f_isinsequence (part of definition for isinsequence): f_isinsequence(s,f,y)= or_f( equal(f,sequence_end(s)), recursive_isinsequence(y,sequence_start(s),f)) Definition of h_isinsequence (part of definition for isinsequence): h_isinsequence(n0,f)= n0 h_isinsequence(sc(s),f)= ad( h_isinsequence(s,f), mu( f_isinsequence(sc(s),f,h_isinsequence(s,f)), pow(n2,sc(s))) ) Definition of isinsequence (returns 1 if formula f is in sequence s): isinsequence(s,f)= bitset(h_isinsequence(s,f),s) Definition of recursive_allof (part of definition for allof): recursive_allof(y,a,b)= bitset(y,a) Definition of f_allof (part of definition for allof): f_allof(a,b,y)= and_f( isinsequence(b,sequence_end(a)), recursive_allof(y,sequence_start(a),b)) Definition of h_allof (part of definition for allof): h_allof(n0,b)= n1 h_allof(sc(a),b)= ad( h_allof(a,b), mu(f_allof(sc(a),b,h_allof(a,b)),pow(n2,sc(a)))) Definition of allof (returns 1 if sequence b contains all formulae of sequence a): allof(a,b)= bitset(h_allof(a,b),a) Definition of sequal (returns 1 if sequences a and b contain the same formulae): sequal(a,b)= and_f( allof(a,b), allof(b,a)) Definition of isimplies_itself (x is a sequence of the form formula formula): isimplies_itself(x)= and_f3( issequence(x), equal(slength(x),n2), equal(sitem(n1,x),sitem(n2,x))) Definition of istautologicalequation (x is a sequence of the form term = term): istautologicalequation(x)= and_f4( issequence(x), equal(slength(x),n1), isequation(sitem(n1,x)), equal( equation_term1(sitem(n1,x)), equation_term2(sitem(n1,x))) ) Definition of isintroductionofconjunction (x is a sequence ... a, y is a sequence --- b, z is ... --- ( a & b )): isintroductionofconjunction(x,y,z)= and_f7( issequence(x), issequence(y), issequence(z), isconjunction(sequence_end(z)), sequal(sequence_start(z),concat(sequence_start(x),sequence_start(y))), equal(conjunction_formula1(sequence_end(z)),sequence_end(x)), equal(conjunction_formula2(sequence_end(z)),sequence_end(y))) Definition of isdeletionofconjunction1 (x is a sequence ... ( a & b ), y is a sequence ... a): isdeletionofconjunction1(x,y)= and_f4( issequence(x), isconjunction(sequence_end(x)), sequal(sequence_start(x),sequence_start(y)), equal(sequence_end(y),conjunction_formula1(sequence_end(x)))) Definition of isdeletionofconjunction2 (x is a sequence ... ( a & b ), y is a sequence ... b): isdeletionofconjunction2(x,y)= and_f4( issequence(x), isconjunction(sequence_end(x)), sequal(sequence_start(x),sequence_start(y)), equal(sequence_end(y),conjunction_formula2(sequence_end(x)))) Definition of isexhaustion (x is a sequence ... a b, y is a sequence --- ~a b, z is a sequence ... --- b): isexhaustion(x,y,z)= and_f10( issequence(x), issequence(y), issequence(z), smaller(n1,slength(x)), smaller(n1,slength(y)), isnegation(sitem(acfull(slength(y)),y)), equal( negation_formula( sitem( acfull(slength(y)), y) ) , sitem(acfull(slength(x)),x)) , equal(sequence_end(x),sequence_end(y)), equal(sequence_end(x),sequence_end(z)), sequal( sequence_start(z), concat( sequence_start(sequence_start(x)), sequence_start(sequence_start(y))) ) ) Definition of isquodlibet (x is a sequence ... a, y is a sequence --- ~a, z is a sequence ... --- b): isquodlibet(x,y,z)= and_f6( issequence(x), issequence(y), issequence(z), isnegation(sequence_end(y)), equal( negation_formula(sequence_end(y)), sequence_end(x)) , sequal( sequence_start(z), concat(sequence_start(x),sequence_start(y))) ) Definition of isremovalofgeneralization (x is a sequence ... !x:a, y is a sequence ... a): isremovalofgeneralization(x,y)= and_f5( issequence(x), issequence(y), isgeneralization(sequence_end(x)), sequal(sequence_start(x),sequence_start(y)), equal(generalization_formula(sequence_end(x)),sequence_end(y))) Definition of isintroductionofgeneralization (x is a sequence ... a, y is a sequence ... !x:a, x is not free in ...): isintroductionofgeneralization(x,y)= and_f6( issequence(x), issequence(y), isgeneralization(sequence_end(y)), sequal(sequence_start(x),sequence_start(y)), equal(sequence_end(x),generalization_formula(sequence_end(y))), or_f( zero(sequence_start(x)), not_f( freeinsequence( sequence_start(x), generalization_namelc(sequence_end(y))) ) ) ) Definition of issubstitution (x is a sequence, y is a sequence, y is a substitution of a term in y for a variable in x in x): issubstitution(x,y)= and_f4( issequence(x), issequence(y), not_f(equal(x,y)), subst_sequence_any(x,y)) Definition of issubstitutionwithidentity (x is a sequence ... a, y is a sequence --- x=t b, b is a substitution of t for x in a): issubstitutionwithidentity(x,y)= and_f5( issequence(x), issequence(y), smaller(n1,slength(y)), isequation(sequence_end(sequence_start(y))), equal( sequence_end(y), subst_formula( sequence_end(x), equation_term1(sequence_end(sequence_start(y))), equation_term2(sequence_end(sequence_start(y)))) ) ) Definition of ispermutation (x is a sequence ... a, y is a sequence ... a): ispermutation(x,y)= and_f5( issequence(x), issequence(y), smaller(n2,slength(x)), equal(sequence_end(x),sequence_end(y)), sequal(sequence_start(x),sequence_start(y))) Definition of slice_safe (like slice(a,b,x), but returns slice(1,b,x) if a = 0): slice_safe(a,b,x)= left( minusfull(sc(b),ifzero(a, n1) ), right(ifzero(a, n1) ,x)) Definition of relation_isgeneralization2_help (part of definition for isgeneralization2_help): relation_isgeneralization2_help(pos,x,y)= and_f5( equal(item(n1,x),n33), equal(item(pos,x),n58), isnamelc(slice(n2,acfull(pos),x)), not_f(equal(slice(n2,acfull(pos),x),concat(n110,n48))), not_f(equal(slice(n2,acfull(pos),x),y))) Definition of argmin_isgeneralization2_help (part of definition for isgeneralization2_help): argmin_isgeneralization2_help(n0,x,y)= n0 argmin_isgeneralization2_help(sc(pos),x,y)= ifzero( argmin_isgeneralization2_help(pos,x,y), cond( relation_isgeneralization2_help(sc(pos),x,y), sc(pos), n0) ) Definition of isgeneralization2_help (returns position of : if x has the form ! isnamelc : ... and isnamelc != y and isnamelc != n0): isgeneralization2_help(x,y)= argmin_isgeneralization2_help(length(x),x,y) Definition of recursive_isgeneralizationlistnotusing (part of definition for isgeneralizationlistnotusing): recursive_isgeneralizationlistnotusing(y,s,x)= bitset(y,s) Definition of f_isgeneralizationlistnotusing (part of definition for isgeneralizationlistnotusing): f_isgeneralizationlistnotusing(s,x,y)= and_f( notzero(isgeneralization2_help(s,x)), recursive_isgeneralizationlistnotusing(y, slice( sc( ifzero( isgeneralization2_help(s, x) , length(s)) ) , length(s), s) , x) ) Definition of h_isgeneralizationlistnotusing (part of definition for isgeneralizationlistnotusing): h_isgeneralizationlistnotusing(n0,x)= n1 h_isgeneralizationlistnotusing(sc(s),x)= ad( h_isgeneralizationlistnotusing(s,x), mu( f_isgeneralizationlistnotusing( sc(s), x, h_isgeneralizationlistnotusing(s,x)) , pow(n2,sc(s))) ) Definition of isgeneralizationlistnotusing (s is a list of generalizations not using variable x or n0): isgeneralizationlistnotusing(s,x)= bitset( h_isgeneralizationlistnotusing(s,x), s) Definition of isinductionpremise (f has the form (A & !x~(B&~C)) where n0 is free in A, B = subst_formula(A,n0,x) = f1, C = subst_formula(A,n0,sc(x))): isinductionpremise(f,x,f1)= and_f( and_f10( isconjunction(f), isnamelc(x), isfreeinformula(conjunction_formula1(f),concat(n110,n48)), isgeneralization(conjunction_formula2(f)), equal(generalization_namelc(conjunction_formula2(f)),x), isnegation(generalization_formula(conjunction_formula2(f))), isconjunction( negation_formula( generalization_formula( conjunction_formula2(f)) ) ) , equal( subst_formula(conjunction_formula1(f),concat(n110,n48),x), conjunction_formula1( negation_formula( generalization_formula( conjunction_formula2(f)) ) ) ) , isnegation( conjunction_formula2( negation_formula( generalization_formula( conjunction_formula2(f)) ) ) ) , equal( subst_formula( conjunction_formula1(f), concat(n110,n48), getsuccx(x)) , negation_formula( conjunction_formula2( negation_formula( generalization_formula( conjunction_formula2(f)) ) ) ) ) ) , equal(subst_formula(conjunction_formula1(f),concat(n110,n48),x),f1)) Definition of induction_leftformula (get ( formula ) from sequence --- ( formula ) ; ... (--- does not contain "(")): induction_leftformula(s)= slice_safe( find_pos(n40,sitem(n1,s),n0), length(sitem(n1,s)), sitem(n1,s)) Definition of induction_leftgeneralizations (get --- from sequence --- ( formula ) ; ... (--- does not contain "(")): induction_leftgeneralizations(s)= slice(n1, acfull(find_pos(n40,sitem(n1,s),n0)), sitem(n1,s)) Definition of induction_rightformula (get string from sequence --- ( formula ) ; --- string (--- does not contain "(")): induction_rightformula(s)= slice_safe( sc(length(induction_leftgeneralizations(s))), length(sequence_end(s)), sequence_end(s)) Definition of induction_rightgeneralizations (get right --- from sequence --- ( formula ) ; --- string (--- does not contain "(")): induction_rightgeneralizations(s)= slice(n1,length(induction_leftgeneralizations(s)),sequence_end(s)) Definition of isinduction (s is a sequence of the form --- (A&!x:~(B&~C)) ; --- !x:B where n0 is free in A, B = subst_formula(A,n0,x), C = subst_formula(A,n0,sc(x)), --- is empty or a list of generalizations not containing variable x or n0): isinduction(s)= and_f7( issequence(s), equal(slength(s),n2), isgeneralization(induction_rightformula(s)), isproposition(generalization_formula(induction_rightformula(s))), equal( induction_rightgeneralizations(s), induction_leftgeneralizations(s)) , isgeneralizationlistnotusing( induction_rightgeneralizations(s), generalization_namelc( induction_rightformula(s)) ) , isinductionpremise( induction_leftformula(s), generalization_namelc(induction_rightformula(s)), generalization_formula(induction_rightformula(s))) ) Definition of isbasicpeanoaxiom (s is a sequence of one of the six peano axioms): isbasicpeanoaxiom(s)= or_f6( equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( mu(n59,pow(n256,n0)), mu(n41,pow(n256,n1))) , mu(n120,pow(n256,n2))) , mu(n40,pow(n256,n3))) , mu(n99,pow(n256,n4))) , mu(n115,pow(n256,n5))) , mu(n61,pow(n256,n6))) , mu(n48,pow(n256,n7))) , mu(n110,pow(n256,n8))) , mu(n126,pow(n256,n9))) , mu(n58,pow(n256,n10))) , mu(n120,pow(n256,n11))) , mu(n33,pow(n256,n12))) ) , equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad(ad(ad(ad(ad(ad(ad(mu(n59,pow(n256,n0)),mu(n41,pow(n256,n1))),mu(n121,pow(n256,n2))),mu(n61,pow(n256,n3))),mu(n120,pow(n256,n4))),mu(n126,pow(n256,n5))),mu(n38,pow(n256,n6))),mu(n41,pow(n256,n7))), mu(n121,pow(n256,n8))) , mu(n40, pow(n256,n9)) ) , mu(n99, pow(n256,n10)) ) , mu(n115, pow(n256,n11)) ) , mu(n61,pow(n256,n12))) , mu(n41,pow(n256,n13))) , mu(n120,pow(n256,n14))) , mu(n40,pow(n256,n15))) , mu(n99,pow(n256,n16))) , mu(n115,pow(n256,n17))) , mu(n40,pow(n256,n18))) , mu(n126,pow(n256,n19))) , mu(n58,pow(n256,n20))) , mu(n121,pow(n256,n21))) , mu(n33,pow(n256,n22))) , mu(n58,pow(n256,n23))) , mu(n120,pow(n256,n24))) , mu(n33,pow(n256,n25))) ) , equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( mu(n59,pow(n256,n0)), mu(n120,pow(n256,n1))) , mu(n61,pow(n256,n2))) , mu(n41,pow(n256,n3))) , mu(n48,pow(n256,n4))) , mu(n110,pow(n256,n5))) , mu(n44,pow(n256,n6))) , mu(n120,pow(n256,n7))) , mu(n40,pow(n256,n8))) , mu(n100,pow(n256,n9))) , mu(n97,pow(n256,n10))) , mu(n58,pow(n256,n11))) , mu(n120,pow(n256,n12))) , mu(n33,pow(n256,n13))) ) , equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(mu(n59,pow(n256,n0)),mu(n41,pow(n256,n1))),mu(n41,pow(n256,n2))),mu(n121,pow(n256,n3))),mu(n44,pow(n256,n4))),mu(n120,pow(n256,n5))),mu(n40,pow(n256,n6))),mu(n100,pow(n256,n7))),mu(n97,pow(n256,n8))),mu(n40,pow(n256,n9))),mu(n99,pow(n256,n10))),mu(n115,pow(n256,n11))), mu(n61,pow(n256,n12))) , mu(n41, pow(n256,n13)) ) , mu(n41, pow(n256,n14)) ) , mu(n121, pow(n256,n15)) ) , mu(n40,pow(n256,n16))) , mu(n99,pow(n256,n17))) , mu(n115,pow(n256,n18))) , mu(n44,pow(n256,n19))) , mu(n120,pow(n256,n20))) , mu(n40,pow(n256,n21))) , mu(n100,pow(n256,n22))) , mu(n97,pow(n256,n23))) , mu(n58,pow(n256,n24))) , mu(n121,pow(n256,n25))) , mu(n33,pow(n256,n26))) , mu(n58,pow(n256,n27))) , mu(n120,pow(n256,n28))) , mu(n33,pow(n256,n29))) ) , equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( mu(n59,pow(n256,n0)), mu(n48,pow(n256,n1))) , mu(n110,pow(n256,n2))) , mu(n61,pow(n256,n3))) , mu(n41,pow(n256,n4))) , mu(n48,pow(n256,n5))) , mu(n110,pow(n256,n6))) , mu(n44,pow(n256,n7))) , mu(n120,pow(n256,n8))) , mu(n40,pow(n256,n9))) , mu(n117,pow(n256,n10))) , mu(n109,pow(n256,n11))) , mu(n58,pow(n256,n12))) , mu(n120,pow(n256,n13))) , mu(n33,pow(n256,n14))) ) , equal(s, ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad( ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(ad(mu(n59,pow(n256,n0)),mu(n41,pow(n256,n1))),mu(n120,pow(n256,n2))),mu(n44,pow(n256,n3))),mu(n41,pow(n256,n4))),mu(n121,pow(n256,n5))),mu(n44,pow(n256,n6))),mu(n120,pow(n256,n7))),mu(n40,pow(n256,n8))),mu(n117,pow(n256,n9))),mu(n109,pow(n256,n10))),mu(n40,pow(n256,n11))),mu(n100,pow(n256,n12))),mu(n97,pow(n256,n13))), mu(n61,pow(n256,n14))) , mu(n41, pow(n256,n15)) ) , mu(n41, pow(n256,n16)) ) , mu(n121, pow(n256,n17)) ) , mu(n40,pow(n256,n18))) , mu(n99,pow(n256,n19))) , mu(n115,pow(n256,n20))) , mu(n44,pow(n256,n21))) , mu(n120,pow(n256,n22))) , mu(n40,pow(n256,n23))) , mu(n117,pow(n256,n24))) , mu(n109,pow(n256,n25))) , mu(n58,pow(n256,n26))) , mu(n121,pow(n256,n27))) , mu(n33,pow(n256,n28))) , mu(n58,pow(n256,n29))) , mu(n120,pow(n256,n30))) , mu(n33,pow(n256,n31))) ) ) Definition of ispeanoaxiom (x is a peano axiom): ispeanoaxiom(x)= or_f( isbasicpeanoaxiom(x), isinduction(x)) Definition of istautology (x is a tautological sequence): istautology(x)= or_f( isimplies_itself(x), istautologicalequation(x)) Definition of isimplicationfromonesequence (sequence y is an implication of sequence x): isimplicationfromonesequence(x,y)= or_f7( ispermutation(x,y), isdeletionofconjunction1(x,y), isdeletionofconjunction2(x,y), isremovalofgeneralization(x,y), isintroductionofgeneralization(x,y), issubstitution(x,y), issubstitutionwithidentity(x,y)) Definition of isimplicationfromtwosequences (sequence z is an implication of sequence x and y): isimplicationfromtwosequences(x,y,z)= or_f3( isintroductionofconjunction(x,y,z), isexhaustion(x,y,z), isquodlibet(x,y,z)) Definition of proofitem (nth statement in sequence of sequences x delimited by \n): proofitem(n,x)= slice(sc(find(acfull(n),n10,x)),acfull(find(n,n10,x)),x) Definition of prooflength (length of sequence of sequences n): prooflength(n)= occur(n10,n) Definition of proof_end (returns last item of a sequence of sequences): proof_end(n)= proofitem(prooflength(n),n) Definition of proof_start (returns all but last item of a sequence of sequences, 0 if sequence of sequences has length 1): proof_start(n)= slice(n1,find(acfull(prooflength(n)),n10,n),n) Definition of recursive_isproof (part of definition for isproof): recursive_isproof(y,n)= bitset(y,n) Definition of f_isproof (part of definition for isproof): f_isproof(n,y)= and_f3( equal(item(length(n),n),n10), issequence(proof_end(n)), or_f( zero(proof_start(n)), recursive_isproof(y,proof_start(n))) ) Definition of h_isproof (part of definition for isproof): h_isproof(n0)= n0 h_isproof(sc(n))= ad( h_isproof(n), mu(f_isproof(sc(n),h_isproof(n)),pow(n2,sc(n)))) Definition of isproof (n is a valid nonempty sequence of sequences ending with \n): isproof(n)= bitset(h_isproof(n),n) Definition of relation_issimplyimplicatedbyone1 (part of definition for issimplyimplicatedbyone1): relation_issimplyimplicatedbyone1(nr,x,y)= isimplicationfromonesequence(proofitem(nr,x),y) Definition of argmin_issimplyimplicatedbyone1 (part of definition for issimplyimplicatedbyone1): argmin_issimplyimplicatedbyone1(n0,x,y)= n0 argmin_issimplyimplicatedbyone1(sc(nr),x,y)= ifzero( argmin_issimplyimplicatedbyone1(nr,x,y), cond( relation_issimplyimplicatedbyone1(sc(nr),x,y), sc(nr), n0) ) Definition of issimplyimplicatedbyone1 (returns a positive number if sequence y is implicated by one sequence in proof x): issimplyimplicatedbyone1(x,y)= argmin_issimplyimplicatedbyone1( prooflength(x), x, y) Definition of issimplyimplicatedbyone (returns 1 if sequence y is implicated by one sequence in proof x): issimplyimplicatedbyone(x,y)= notzero(issimplyimplicatedbyone1(x,y)) Definition of relation_issimplyimplicatedbytwo1 (part of definition for issimplyimplicatedbytwo1): relation_issimplyimplicatedbytwo1(nr,x,y,z)= isimplicationfromtwosequences(proofitem(nr,x),y,z) Definition of argmin_issimplyimplicatedbytwo1 (part of definition for issimplyimplicatedbytwo1): argmin_issimplyimplicatedbytwo1(n0,x,y,z)= n0 argmin_issimplyimplicatedbytwo1(sc(nr),x,y,z)= ifzero( argmin_issimplyimplicatedbytwo1(nr,x,y,z), cond( relation_issimplyimplicatedbytwo1(sc(nr),x,y,z), sc(nr), n0) ) Definition of issimplyimplicatedbytwo1 (returns a positive number if sequence z is implicated by one sequence in proof x and sequence y): issimplyimplicatedbytwo1(x,y,z)= argmin_issimplyimplicatedbytwo1(prooflength(x),x,y,z) Definition of relation_issimplyimplicatedbytwo2 (part of definition for issimplyimplicatedbytwo2): relation_issimplyimplicatedbytwo2(nr,x,y)= notzero(issimplyimplicatedbytwo1(x,proofitem(nr,x),y)) Definition of argmin_issimplyimplicatedbytwo2 (part of definition for issimplyimplicatedbytwo2): argmin_issimplyimplicatedbytwo2(n0,x,y)= n0 argmin_issimplyimplicatedbytwo2(sc(nr),x,y)= ifzero( argmin_issimplyimplicatedbytwo2(nr,x,y), cond( relation_issimplyimplicatedbytwo2(sc(nr),x,y), sc(nr), n0) ) Definition of issimplyimplicatedbytwo2 (returns a positive number if sequence y is implicated by two sequences in proof x): issimplyimplicatedbytwo2(x,y)= argmin_issimplyimplicatedbytwo2( prooflength(x), x, y) Definition of issimplyimplicatedbytwo (returns 1 if sequence y is implicated by two sequences in proof x): issimplyimplicatedbytwo(x,y)= notzero(issimplyimplicatedbytwo2(x,y)) Definition of recursive_isvalidproof (part of definition for isvalidproof): recursive_isvalidproof(y,x)= bitset(y,x) Definition of f_isvalidproof (part of definition for isvalidproof): f_isvalidproof(x,y)= and_f3( isproof(x), or_f4( ispeanoaxiom(proof_end(x)), istautology(proof_end(x)), issimplyimplicatedbyone( proof_start(x), proof_end(x)) , issimplyimplicatedbytwo( proof_start(x), proof_end(x)) ) , or_f( zero(proof_start(x)), recursive_isvalidproof(y,proof_start(x))) ) Definition of h_isvalidproof (part of definition for isvalidproof): h_isvalidproof(n0)= n0 h_isvalidproof(sc(x))= ad( h_isvalidproof(x), mu( f_isvalidproof(sc(x),h_isvalidproof(x)), pow(n2,sc(x))) ) Definition of isvalidproof (x is a valid proof (every sequence follows directly from zero, one or two preceding sequences)): isvalidproof(x)= bitset(h_isvalidproof(x),x) Definition of isvalidprooffor (x is a valid proof for y): isvalidprooffor(x,y)= and_f3( isvalidproof(x), isformula(y), equal(proof_end(x),concat(y,n59)))