let sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c n = let (ca,c) = i 4 c in let f = if ca = 0 then (fun y z -> Ap(Ap(DB(m+n),y),z)) else if ca = 1 then (fun y z -> Ap(Ap(DB(b+n),y),z)) else if ca = 2 then (fun y z -> Ap(Ap(DB(s+n),y),z)) else if ca = 3 then (fun y z -> Ap(Ap(DB(k+n),y),z)) else if ca = 4 then (fun y z -> Ap(Ap(DB(s+n),Ap(Ap(DB(b+n),y),z)),y)) (** (y \ z) / y **) else if ca = 5 then (fun y z -> Ap(Ap(DB(b+n),y),Ap(Ap(DB(s+n),z),y))) (** y \ (z / y) **) else if ca = 6 then (fun y z -> Ap(Ap(DB(t+n),y),z)) else if ca = 7 then (fun y z -> Ap(Ap(DB(t+n),z),y)) else if ca = 8 then (fun y z -> Ap(Ap(DB(i1+n),y),z)) else if ca = 9 then (fun y z -> Ap(Ap(DB(i1+n),z),y)) else if ca = 10 then (fun y z -> Ap(Ap(DB(j1+n),y),z)) else if ca = 11 then (fun y z -> Ap(Ap(DB(j1+n),z),y)) else if ca = 12 then (fun y z -> Ap(Ap(DB(i2+n),y),z)) else if ca = 13 then (fun y z -> Ap(Ap(DB(i2+n),z),y)) else if ca = 14 then (fun y z -> Ap(Ap(DB(j2+n),y),z)) else (fun y z -> Ap(Ap(DB(j2+n),z),y)) in (f,c) (** return true if random number < 2^bits is < num, so return true num/2^bits of the time **) let sei_incl_prob (num,bits) i c = if bits = 0 then (0 < num,c) else let (k,c) = i bits c in (k < num,c) (* Use c to pseudorandomly choose inner mappings for assumed eqns that some inner mappings commute. *) let sei_aim_params (nb,pb,nc,pc,nd,pd,ne,pe,nf,pf) wrapf i c = let (j2,i2,j1,i1,r,l,t,a,k,e,s,b,m,x) = (0,1,2,3,4,5,6,7,8,9,10,11,12,13) in let relall n p = All(Base(0),Imp(Ap(Ap(Prim(7),DB(0)),DB(x+n)),p)) in let rec relallrec n p = if n > 0 then relallrec (n-1) (relall n p) else p in let q = ref (Prim(1)) in (* False *) let addid n lhs rhs = if not (lhs = rhs) then (** don't add if syntactically equal **) q := Imp(relallrec n (Eq(Base(0),lhs,rhs)),!q) in let cr = ref c in for j = 1 to nf do let c = !cr in let (incl,c) = sei_incl_prob pf i c in if incl then begin let (m1a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 7 in let (m1b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 7 in let (m1c,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 7 in let (m2a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 7 in let (m2b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 7 in let (bop1,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 7 in let (bop2,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 7 in let (bop3,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 7 in let (bop4,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 7 in cr := c; let m1f y z w u = Ap(Ap(Ap(m1a,bop1 y z),w),Ap(Ap(m1b,bop2 y w),Ap(Ap(m1c,z),u))) in let m2f y z w u = Ap(Ap(Ap(m2a,bop3 y z),w),Ap(Ap(m2b,bop4 z w),u)) in addid 7 (m1f (DB(6)) (DB(5)) (DB(4)) (m2f (DB(3)) (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(3)) (DB(2)) (DB(1)) (m1f (DB(6)) (DB(5)) (DB(4)) (DB(0)))) end else cr := c done; for j = 1 to ne do let c = !cr in let (incl,c) = sei_incl_prob pe i c in if incl then begin let (b,c) = i 1 c in if b = 0 then begin let (m1a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 6 in let (m1b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 6 in let (m2a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 6 in let (m2b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 6 in let (bop1,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop2,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop3,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop4,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in cr := c; let m1f y z w u = Ap(Ap(Ap(m1a,y),bop1 y z),Ap(Ap(m1b,bop2 y (bop3 z w)),u)) in let m2f y z u = Ap(Ap(Ap(m2a,y),z),Ap(Ap(m2b,bop4 y z),u)) in addid 6 (m1f (DB(5)) (DB(4)) (DB(3)) (m2f (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(2)) (DB(1)) (m1f (DB(5)) (DB(4)) (DB(3)) (DB(0)))) end else begin let (m1a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 6 in let (m1b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 6 in let (m2a,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 6 in let (m2b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 6 in let (bop1,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop2,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop3,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in let (bop4,c) = sei_aim_binop (j2,i2,j1,i1,r,l,t,k,s,b,m) i c 6 in cr := c; let m1f y z w u = Ap(Ap(Ap(m1a,y),bop1 z w),Ap(Ap(m1b,bop2 y w),u)) in let m2f y z u = Ap(Ap(m2a,bop3 y z),Ap(Ap(m2b,bop4 y z),u)) in addid 6 (m1f (DB(5)) (DB(4)) (DB(3)) (m2f (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(2)) (DB(1)) (m1f (DB(5)) (DB(4)) (DB(3)) (DB(0)))) end end else cr := c; done; let incl_ll () = let m1 = DB(l+5) in let m2 = DB(l+5) in let m1f y z u = Ap(Ap(Ap(m1,y),z),u) in let m2f y z u = Ap(Ap(Ap(m2,y),z),u) in addid 5 (m1f (DB(4)) (DB(3)) (m2f (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(2)) (DB(1)) (m1f (DB(4)) (DB(3)) (DB(0)))); in let incl_lr () = let m1 = DB(l+5) in let m2 = DB(r+5) in let m1f y z u = Ap(Ap(Ap(m1,y),z),u) in let m2f y z u = Ap(Ap(Ap(m2,y),z),u) in addid 5 (m1f (DB(4)) (DB(3)) (m2f (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(2)) (DB(1)) (m1f (DB(4)) (DB(3)) (DB(0)))); in let incl_rr () = let m1 = DB(r+5) in let m2 = DB(r+5) in let m1f y z u = Ap(Ap(Ap(m1,y),z),u) in let m2f y z u = Ap(Ap(Ap(m2,y),z),u) in addid 5 (m1f (DB(4)) (DB(3)) (m2f (DB(2)) (DB(1)) (DB(0)))) (m2f (DB(2)) (DB(1)) (m1f (DB(4)) (DB(3)) (DB(0)))); in let (dv,c) = i 3 c in let dinclfl = ref [] in if dv < 2 then dinclfl := [incl_ll;incl_lr;incl_rr] else if dv = 2 then dinclfl := [incl_ll;incl_rr;incl_lr] else if dv = 3 then dinclfl := [incl_lr;incl_ll;incl_rr] else if dv = 4 then dinclfl := [incl_lr;incl_rr;incl_ll] else if dv = 5 then dinclfl := [incl_rr;incl_ll;incl_lr] else dinclfl := [incl_rr;incl_lr;incl_ll]; for j = 1 to nd do match !dinclfl with | [] -> () | (df::dfr) -> let c = !cr in let (incl,c) = sei_incl_prob pd i c in cr := c; if incl then begin df(); dinclfl := dfr end done; for j = 1 to nc do let c = !cr in let (incl,c) = sei_incl_prob pc i c in if incl then begin let (m1,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 4 in let (m2,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 4 in let m1f y z u = Ap(Ap(Ap(m1,y),z),u) in let m2f y u = Ap(Ap(m2,y),u) in cr := c; addid 4 (m1f (DB(3)) (DB(2)) (m2f (DB(1)) (DB(0)))) (m2f (DB(1)) (m1f (DB(3)) (DB(2)) (DB(0)))); end else cr := c done; for j = 1 to nb do let c = !cr in let (incl,c) = sei_incl_prob pb i c in if incl then begin let (m1,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 3 in let (m2,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 3 in let m1f y u = Ap(Ap(m1,y),u) in let m2f y u = Ap(Ap(m2,y),u) in cr := c; addid 3 (m1f (DB(2)) (m2f (DB(1)) (DB(0)))) (m2f (DB(1)) (m1f (DB(2)) (DB(0)))); end else cr := c done; let c = !cr in let (b,c) = i 2 c in if b = 0 then let (m1,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 3 in let (m2a,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 3 in let (m2b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 3 in let m1f y z u = Ap(Ap(Ap(m1,y),z),u) in let m2f y z u = Ap(Ap(m2a,y),Ap(Ap(m2b,z),u)) in let m12f y z u = m1f y z (m2f y z u) in let rec m12fpow n y z u = if n > 0 then m12f y z (m12fpow (n-1) y z u) else u in let (b,c) = i 2 c in (** m12f has order b+2 [between 2 and 5] **) cr := c; addid 3 (m12fpow (b+2) (DB(2)) (DB(1)) (DB(0))) (DB(0)) else if b = 1 then let (m1a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 4 in let (m1b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 4 in let (m2a,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 4 in let (m2b,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 4 in let m1f y z w u = Ap(Ap(Ap(m1a,y),z),Ap(Ap(m1b,w),u)) in let m2f y z w u = Ap(Ap(m2a,y),Ap(Ap(Ap(m2b,z),w),u)) in let m12f y z w u = m1f y z w (m2f y z w u) in let rec m12fpow n y z w u = if n > 0 then m12f y z w (m12fpow (n-1) y z w u) else u in let (b,c) = i 2 c in (** m12f has order b+2 [between 2 and 5] **) cr := c; addid 4 (m12fpow (b+2) (DB(3)) (DB(2)) (DB(1)) (DB(0))) (DB(0)) else if b = 2 then let (m1a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 4 in let (m1b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 4 in let (m2a,c) = sei_aim_innmap2 (j2,i2,j1,i1,r,l,t) i c 4 in let (m2b,c) = sei_aim_innmap1 (j2,i2,j1,i1,r,l,t) i c 4 in let m1f y z w u = Ap(Ap(Ap(m1a,y),z),Ap(Ap(m1b,w),u)) in let m2f y z w u = Ap(Ap(Ap(m2a,y),z),Ap(Ap(m2b,w),u)) in let m12f y z w u = m1f y z w (m2f y z w u) in let rec m12fpow n y z w u = if n > 0 then m12f y z w (m12fpow (n-1) y z w u) else u in let (b,c) = i 2 c in (** m12f has order b+2 [between 2 and 5] **) cr := c; addid 4 (m12fpow (b+2) (DB(3)) (DB(2)) (DB(1)) (DB(0))) (DB(0)) else (** no extra eqn **) (); wrapf !q let aim_wrapper loopwithdefscex q = let (j2,i2,j1,i1,r,l,t,a,k,e,s,b,m,x) = (0,1,2,3,4,5,6,7,8,9,10,11,12,13) in let i = Base(0) in let ii = TpArr(i,i) in let iii = TpArr(i,ii) in let iiii = TpArr(i,iii) in let loophyp = Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(loopwithdefscex,DB(x)),DB(m)),DB(b)),DB(s)),DB(e)),DB(k)),DB(a)),DB(t)),DB(l)),DB(r)),DB(i1)),DB(j1)),DB(i2)),DB(j2)) in All(i,All(iii,All(iii,All(iii,All(i,All(iii,All(iiii,All(iii,All(iiii,All(iiii,All(iii,All(iii,All(iii,All(iii,Imp(loophyp,q))))))))))))))) let raim_wrapper loopwithdefscex (rr,rs,rn) q = let (j2,i2,j1,i1,r,l,t,a,k,e,s,b,m,x) = (0,1,2,3,4,5,6,7,8,9,10,11,12,13) in let i = Base(0) in let ii = TpArr(i,i) in let iii = TpArr(i,ii) in let iiii = TpArr(i,iii) in let neg w = Ap(Prim(3),w) in let conj w z = Ap(Ap(Prim(4),w),z) in let disj w z = Ap(Ap(Prim(5),w),z) in let mem w z = Ap(Ap(Prim(7),w),z) in let subq w z = Ap(Ap(Prim(8),w),z) in let setminus w z = Ap(Ap(Prim(50),w),z) in let sing w = Ap(Prim(43),w) in let atleastr w = Ap(Prim(12 + rr),w) in let atleasts w = Ap(Prim(12 + rs),w) in let cardhyp = Ap(Ap(Prim(54),DB(x)),bin_hf_rep (Int64.of_int rn)) in (** the carrier has cardinality rn **) let noclique = All(Base(0),Imp(subq (DB(0)) (DB(x+2)),Imp(atleastr (DB(0)),Ex(Base(0),conj (mem (DB(0)) (DB(1))) (Ex(Base(0),conj (mem (DB(0)) (setminus (DB(2)) (sing (DB(1))))) (neg (disj (mem (Ap(Ap(DB(s+4),DB(1)),DB(0))) (DB(3))) (mem (Ap(Ap(DB(s+4),DB(0)),DB(1))) (DB(3))))))))))) in let noanticlique = All(Base(0),Imp(subq (DB(0)) (DB(x+2)),Imp(atleasts (DB(0)),Ex(Base(0),conj (mem (DB(0)) (DB(1))) (Ex(Base(0),conj (mem (DB(0)) (setminus (DB(2)) (sing (DB(1))))) (disj (mem (Ap(Ap(DB(s+4),DB(1)),DB(0))) (DB(3))) (mem (Ap(Ap(DB(s+4),DB(0)),DB(1))) (DB(3)))))))))) in let ramseyhyp = Ex(Base(0),conj noclique noanticlique) in let loophyp = Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(Ap(loopwithdefscex,DB(x)),DB(m)),DB(b)),DB(s)),DB(e)),DB(k)),DB(a)),DB(t)),DB(l)),DB(r)),DB(i1)),DB(j1)),DB(i2)),DB(j2)) in All(i,All(iii,All(iii,All(iii,All(i,All(iii,All(iiii,All(iii,All(iiii,All(iiii,All(iii,All(iii,All(iii,All(iii,Imp(loophyp,Imp(cardhyp,Imp(ramseyhyp,q))))))))))))))))) let phaseparams = [| (3,(1,2),2,(1,2),2,(1,2),4,(1,0),3,(1,1)); (2,(1,1),3,(3,2),1,(1,1),4,(1,0),1,(1,1)); (3,(1,2),1,(1,2),1,(1,0),4,(1,0),2,(3,2)); (2,(1,2),3,(1,2),2,(1,0),4,(1,0),1,(1,1)); (1,(1,1),1,(1,2),3,(1,2),4,(1,0),2,(1,0)); (2,(1,0),1,(1,0),1,(1,0),4,(1,0),2,(1,1)); (3,(1,2),3,(3,2),3,(1,0),4,(1,0),2,(1,1)); (1,(1,0),3,(3,2),3,(1,0),4,(1,0),2,(1,1)); (3,(1,0),1,(1,0),2,(1,0),4,(1,0),1,(3,2)); (1,(1,0),1,(1,0),3,(1,1),4,(1,0),3,(1,0)); (3,(1,0),2,(3,2),3,(1,0),4,(1,0),2,(3,2)); (3,(1,1),2,(1,0),1,(1,0),4,(1,0),3,(1,0)); (1,(1,0),3,(1,0),3,(1,0),4,(1,0),1,(1,0)); (1,(3,2),1,(1,0),3,(1,0),4,(1,0),3,(1,0)); (2,(1,0),1,(3,2),3,(1,0),4,(1,0),3,(1,0)); |] let ramseya = [| (3,3,5);(3,4,6);(3,4,7);(3,4,8);(3,5,7);(3,5,8);(3,5,9);(3,5,10); (3,5,11);(3,5,12);(3,5,13);(3,6,8);(3,6,9);(3,6,10);(3,6,11);(3,6,12); (3,6,13);(3,6,14);(3,6,15);(3,6,16);(3,6,17);(4,4,7);(4,4,8);(4,4,9); (4,4,10);(4,4,11);(4,4,12);(4,4,13);(4,4,14);(4,4,15);(4,4,16);(4,4,17); (4,5,8);(4,5,9);(4,5,10);(4,5,11);(4,5,12);(4,5,13);(4,5,14);(4,5,15); (4,5,16);(4,5,17);(4,5,18);(4,5,19);(4,5,20);(4,5,21);(4,5,22);(4,5,23); (4,5,24);(4,6,9);(4,6,10);(4,6,11);(4,6,12);(4,6,13);(4,6,14);(4,6,15); (4,6,16);(4,6,17);(4,6,18);(4,6,19);(4,6,20);(4,6,21);(4,6,22);(4,6,23); (4,6,24);(4,6,25);(4,6,26);(4,6,27);(4,6,28);(4,6,29);(4,6,30);(4,6,31); (4,6,32);(4,6,33);(4,6,34);(4,6,35);(5,5,9);(5,5,10);(5,5,11);(5,5,12); (5,5,13);(5,5,14);(5,5,15);(5,5,16);(5,5,17);(5,5,18);(5,5,19);(5,5,20); (5,5,21);(5,5,22);(5,5,23);(5,5,24);(5,5,25);(5,5,26);(5,5,27);(5,5,28); (5,5,29);(5,5,30);(5,5,31);(5,5,32);(5,5,33);(5,5,34);(5,5,35);(5,5,36); (5,5,37);(5,5,38);(5,5,39);(5,5,40);(5,5,41);(5,5,42);(5,6,10);(5,6,11); (5,6,12);(5,6,13);(5,6,14);(5,6,15);(5,6,16);(5,6,17);(5,6,18);(5,6,19); (5,6,20);(5,6,21);(5,6,22);(5,6,23);(5,6,24);(5,6,25);(5,6,26);(5,6,27); (5,6,28);(5,6,29);(5,6,30);(5,6,31);(5,6,32);(5,6,33);(5,6,34);(5,6,35); (5,6,36);(5,6,37);(5,6,38);(5,6,39);(5,6,40);(5,6,41);(5,6,42);(5,6,43); (5,6,44);(5,6,45);(5,6,46);(5,6,47);(5,6,48);(5,6,49);(5,6,50);(5,6,51); (5,6,52);(5,6,53);(5,6,54);(5,6,55);(5,6,56);(5,6,57);(6,6,11);(6,6,12); (6,6,13);(6,6,14);(6,6,15);(6,6,16);(6,6,17);(6,6,18);(6,6,19);(6,6,20); (6,6,21);(6,6,22);(6,6,23);(6,6,24);(6,6,25);(6,6,26);(6,6,27);(6,6,28); (6,6,29);(6,6,30);(6,6,31);(6,6,32);(6,6,33);(6,6,34);(6,6,35);(6,6,36); (6,6,37);(6,6,38);(6,6,39);(6,6,40);(6,6,41);(6,6,42);(6,6,43);(6,6,44); (6,6,45);(6,6,46);(6,6,47);(6,6,48);(6,6,49);(6,6,50);(6,6,51);(6,6,52); (6,6,53);(6,6,54);(6,6,55);(6,6,56);(6,6,57);(6,6,58);(6,6,59);(6,6,60); (6,6,61);(6,6,62);(6,6,63);(6,6,64);(6,6,65);(6,6,66);(6,6,67);(6,6,68); (6,6,69);(6,6,70);(6,6,71);(6,6,72);(6,6,73);(6,6,74);(6,6,75);(6,6,76); (6,6,77);(6,6,78);(6,6,79);(6,6,80);(6,6,81);(6,6,82);(6,6,83);(6,6,84); (6,6,85);(6,6,86);(6,6,87);(6,6,88);(6,6,89);(6,6,90);(6,6,91);(6,6,92); (6,6,93);(6,6,94);(6,6,95);(6,6,96);(6,6,97);(6,6,98);(6,6,99);(6,6,100); (6,6,101);(4,6,36);(4,6,37);(4,6,38);(4,6,39);(4,6,40);(5,5,43);(5,5,44); (5,5,45);(5,5,46);(5,5,47);(5,6,58);(5,6,59);(5,6,60);(5,6,61);(5,6,62); (5,6,63);(5,6,64);(5,6,65);(5,6,66);(5,6,67);(5,6,68);(5,6,69);(5,6,70); (5,6,71);(5,6,72);(5,6,73);(5,6,74);(5,6,75);(5,6,76);(5,6,77);(5,6,78); (5,6,79);(5,6,80);(5,6,81);(5,6,82);(5,6,83);(5,6,84);(5,6,85);(5,6,86); (6,6,102);(6,6,103);(6,6,104);(6,6,105);(6,6,106);(6,6,107);(6,6,108);(6,6,109); (6,6,110);(6,6,111);(6,6,112);(6,6,113);(6,6,114);(6,6,115);(6,6,116);(6,6,117); (6,6,118);(6,6,119);(6,6,120);(6,6,121);(6,6,122);(6,6,123);(6,6,124);(6,6,125); (6,6,126);(6,6,127);(6,6,128);(6,6,129);(6,6,130);(6,6,131);(6,6,132);(6,6,133); (6,6,134);(6,6,135);(6,6,136);(6,6,137);(6,6,138);(6,6,139);(6,6,140);(6,6,141); (6,6,142);(6,6,143);(6,6,144);(6,6,145);(6,6,146);(6,6,147);(6,6,148);(6,6,149); (6,6,150);(6,6,151);(6,6,152);(6,6,153);(6,6,154);(6,6,155);(6,6,156);(6,6,157); (6,6,158);(6,6,159);(6,6,160);(6,6,161);(6,6,162);(6,6,163);(6,6,164) |] let sei_aim1_phase k i c = let loopwithdefscex1 = Prim(99) in sei_aim_params (phaseparams.(k-1)) (aim_wrapper loopwithdefscex1) i c let sei_aim2_phase k i c = let loopwithdefscex2 = Prim(100) in sei_aim_params (phaseparams.(k-1)) (aim_wrapper loopwithdefscex2) i c let sei_raim1_phase k i c = let loopwithdefscex1 = Prim(99) in let (j,c) = i 7 c in let base = if k = 1 then 0 else if k = 2 then 56 else if k = 3 then 112 else if k = 4 then 167 else 223 in let (r,s,n) = ramseya.(base+j) in sei_aim_params (phaseparams.(k-1)) (raim_wrapper loopwithdefscex1 (r,s,n)) i c let sei_raim2_phase k i c = let loopwithdefscex2 = Prim(100) in let (j,c) = i 7 c in let base = if k = 1 then 0 else if k = 2 then 56 else if k = 3 then 112 else if k = 4 then 167 else 223 in let (r,s,n) = ramseya.(base+j) in sei_aim_params (phaseparams.(k-1)) (raim_wrapper loopwithdefscex2 (r,s,n)) i c let phase blkh = if blkh > 75000L then 15 else Int64.to_int (Int64.div blkh 5000L) (** Sample calls from an updated reward_bounty_prop_main: (12,sei_raim1_phase (phase blkh) seis (s,2048,None,0,0)) (13,sei_raim2_phase (phase blkh) seis (s,2048,None,0,0)) (9,sei_aim1_phase (phase blkh) seis (s,2048,None,0,0)) (10,sei_aim2_phase (phase blkh) seis (s,2048,None,0,0)) **)