# commands for circular critical exponents of # pprefixes and pfactors of regular paperfolding sequence def prcrep1 "Aj ((j>=i)&(j+p P[j]=P[j+p]": def prcrep2 "Aj ((j>=i)&(j=s+n)&(j+p P[j]=P[(j+p)-n]": def prcrep3 "Aj ((j>=i)&(j>=s+n)&(j+p P[j-n]=P[(j+p)-n]": def pcrep "\$prcrep1(i,m,n,p,s) & \$prcrep2(i,m,n,p,s) & \$prcrep3(i,m,n,p,s)": def pcrep "(Aj ((j>=i)&(j+p P[j]=P[j+p]) & (Aj ((j>=i)&(j=s+n)&(j+p P[j]=P[(j+p)-n]) & (Aj ((j>=i)&(j>=s+n)&(j+p P[j-n]=P[(j+p)-n])": def pprefge11 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= p) & \$pcrep(i,m,n,p,0)": def pprefgt11 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > p) & \$pcrep(i,m,n,p,0)": def pprefeq11 "\$pprefge11(n) & ~\$pprefgt11(n)": def pprefge21 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 2*p) & \$pcrep(i,m,n,p,0)": def pprefgt21 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 2*p) & \$pcrep(i,m,n,p,0)": def pprefeq21 "\$pprefge21(n) & ~\$pprefgt21(n)": def pprefge73 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m >= 7*p) & \$pcrep(i,m,n,p,0)": def pprefgt73 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m > 7*p) & \$pcrep(i,m,n,p,0)": def pprefeq73 "\$pprefge73(n) & ~\$pprefgt73(n)": def pprefge31 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 3*p) & \$pcrep(i,m,n,p,0)": def pprefgt31 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 3*p) & \$pcrep(i,m,n,p,0)": def pprefeq31 "\$pprefge31(n) & ~\$pprefgt31(n)": def pprefge103 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m >= 10*p) & \$pcrep(i,m,n,p,0)": def pprefgt103 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m > 10*p) & \$pcrep(i,m,n,p,0)": def pprefeq103 "\$pprefge103(n) & ~\$pprefgt103(n)": def pprefge41 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 4*p) & \$pcrep(i,m,n,p,0)": def pprefgt41 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 4*p) & \$pcrep(i,m,n,p,0)": def pprefeq41 "\$pprefge41(n) & ~\$pprefgt41(n)": def pprefge133 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m >= 13*p) & \$pcrep(i,m,n,p,0)": def pprefgt133 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (3*m > 13*p) & \$pcrep(i,m,n,p,0)": def pprefeq133 "\$pprefge133(n) & ~\$pprefgt133(n)": def pprefge51 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m >= 5*p) & \$pcrep(i,m,n,p,0)": def pprefgt51 "E i,m,p (p >= 1) & (m <= n) & (i < n) & (m > 5*p) & \$pcrep(i,m,n,p,0)": def pprefeq51 "\$pprefge51(n) & ~\$pprefgt51(n)": eval testppref "An (n>=1) => (\$pprefeq11(n) | \$pprefeq21(n) | \$pprefeq73(n) | \$pprefeq31(n) | \$pprefeq103(n) | \$pprefeq41(n) | \$pprefeq133(n) | \$pprefeq51(n) )": def pfacge11 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= p) & \$pcrep(i,m,n,p,s)": def pfacgt11 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i p) & \$pcrep(i,m,n,p,s)": def pfaceq11 "\$pfacge11(n,s) & ~\$pfacgt11(n,s)": def pfacex11 "Es \$pfaceq11(n,s)": def pfacge21 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 2*p) & \$pcrep(i,m,n,p,s)": def pfacgt21 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 2*p) & \$pcrep(i,m,n,p,s)": def pfaceq21 "\$pfacge21(n,s) & ~\$pfacgt21(n,s)": def pfacex21 "Es \$pfaceq21(n,s)": def pfacge73 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 7*p) & \$pcrep(i,m,n,p,s)": def pfacgt73 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 7*p) & \$pcrep(i,m,n,p,s)": def pfaceq73 "\$pfacge73(n,s) & ~\$pfacgt73(n,s)": def pfacex73 "Es \$pfaceq73(n,s)": def pfacge52 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 5*p) & \$pcrep(i,m,n,p,s)": def pfacgt52 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 5*p) & \$pcrep(i,m,n,p,s)": def pfaceq52 "\$pfacge52(n,s) & ~\$pfacgt52(n,s)": def pfacex52 "Es \$pfaceq52(n,s)": def pfacge83 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 8*p) & \$pcrep(i,m,n,p,s)": def pfacgt83 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 8*p) & \$pcrep(i,m,n,p,s)": def pfaceq83 "\$pfacge83(n,s) & ~\$pfacgt83(n,s)": def pfacex83 "Es \$pfaceq83(n,s)": def pfacge31 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 3*p) & \$pcrep(i,m,n,p,s)": def pfacgt31 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 3*p) & \$pcrep(i,m,n,p,s)": def pfaceq31 "\$pfacge31(n,s) & ~\$pfacgt31(n,s)": def pfacex31 "Es \$pfaceq31(n,s)": def pfacge103 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 10*p) & \$pcrep(i,m,n,p,s)": def pfacgt103 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 10*p) & \$pcrep(i,m,n,p,s)": def pfaceq103 "\$pfacge103(n,s) & ~\$pfacgt103(n,s)": def pfacex103 "Es \$pfaceq103(n,s)": def pfacge72 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 7*p) & \$pcrep(i,m,n,p,s)": def pfacgt72 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 7*p) & \$pcrep(i,m,n,p,s)": def pfaceq72 "\$pfacge72(n,s) & ~\$pfacgt72(n,s)": def pfacex72 "Es \$pfaceq72(n,s)": def pfacge114 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 11*p) & \$pcrep(i,m,n,p,s)": def pfacgt114 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 11*p) & \$pcrep(i,m,n,p,s)": def pfaceq114 "\$pfacge114(n,s) & ~\$pfacgt114(n,s)": def pfacex114 "Es \$pfaceq114(n,s)": def pfacge41 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 4*p) & \$pcrep(i,m,n,p,s)": def pfacgt41 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 4*p) & \$pcrep(i,m,n,p,s)": def pfaceq41 "\$pfacge41(n,s) & ~\$pfacgt41(n,s)": def pfacex41 "Es \$pfaceq41(n,s)": def pfacge51 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 5*p) & \$pcrep(i,m,n,p,s)": def pfacgt51 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 5*p) & \$pcrep(i,m,n,p,s)": def pfaceq51 "\$pfacge51(n,s) & ~\$pfacgt51(n,s)": def pfacex51 "Es \$pfaceq51(n,s)": def pfacge61 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 6*p) & \$pcrep(i,m,n,p,s)": def pfacgt61 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 6*p) & \$pcrep(i,m,n,p,s)": def pfaceq61 "\$pfacge61(n,s) & ~\$pfacgt61(n,s)": def pfacex61 "Es \$pfaceq61(n,s)": def pfacge133 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i= 13*p) & \$pcrep(i,m,n,p,s)": def pfacgt133 "E i,m,p (p>=1) & (m <= n) & (i>=s) & (i 13*p) & \$pcrep(i,m,n,p,s)": def pfaceq133 "\$pfacge133(n,s) & ~\$pfacgt133(n,s)": def pfacex133 "Es \$pfaceq133(n,s)": eval testpfac "An (n>=1) => (As (\$pfaceq11(n,s) | \$pfaceq21(n,s) | \$pfaceq73(n,s) | \$pfaceq52(n,s) | \$pfaceq83(n,s) | \$pfaceq114(n,s) | \$pfaceq31(n,s) | \$pfaceq103(n,s) | \$pfaceq72(n,s) | \$pfaceq41(n,s) | \$pfaceq133(n,s) | \$pfaceq51(n,s) | \$pfaceq61(n,s) ))": def pfacex11 "Es \$pfaceq11(n,s)": def pfacex21 "Es \$pfaceq21(n,s)": def pfacex73 "Es \$pfaceq73(n,s)": def pfacex52 "Es \$pfaceq52(n,s)": def pfacex83 "Es \$pfaceq83(n,s)": def pfacex114 "Es \$pfaceq114(n,s)": def pfacex31 "Es \$pfaceq31(n,s)": def pfacsmall11 "\$pfacex11(n) & (As \$pfacge11(n,s))": def pfacsmall21 "\$pfacex21(n) & (As \$pfacge21(n,s))": def pfacsmall73 "\$pfacex73(n) & (As \$pfacge73(n,s))": def pfacsmall52 "\$pfacex52(n) & (As \$pfacge52(n,s))": def pfacsmall83 "\$pfacex83(n) & (As \$pfacge83(n,s))": def pfacsmall114 "\$pfacex114(n) & (As \$pfacge114(n,s))": def pfacsmall31 "\$pfacex31(n) & (As \$pfacge31(n,s))": eval smallpfactest "An (n>=1) => (\$pfacsmall11(n) | \$pfacsmall21(n) | \$pfacsmall73(n) | \$pfacsmall52(n) | \$pfacsmall83(n)) | \$pfacsmall114(n) | \$pfacsmall31(n)": def pfaclarge11 "\$pfacex11(n) & (As ~\$pfacgt11(n,s))": def pfaclarge21 "\$pfacex21(n) & (As ~\$pfacgt21(n,s))": def pfaclarge31 "\$pfacex31(n) & (As ~\$pfacgt31(n,s))": def pfaclarge41 "\$pfacex41(n) & (As ~\$pfacgt41(n,s))": def pfaclarge51 "\$pfacex51(n) & (As ~\$pfacgt51(n,s))": def pfaclarge61 "\$pfacex61(n) & (As ~\$pfacgt61(n,s))": eval largepfactest "An (n>=1) => (\$pfaclarge11(n) | \$pfaclarge21(n) | \$pfaclarge31(n) | \$pfaclarge41(n) | \$pfaclarge51(n) | \$pfaclarge61(n) )":