# 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) )":