open util/integer
open gcdt[Int]

fun getPlus [n: Int]: Int one->one Int {
	{lhs, rhs: Int | rhs = lhs + n}
}

fun getTimes [n: Int]: Int one->one Int {
	{lhs, rhs: Int | rhs = mul[lhs][n]}
}

fun opPlus : CommutativeOp {
	{cop : CommutativeOp | cop.op = getPlus }
}

fun opTimes [n: Int]: PseudoCommutativeOp {
	{pcop : PseudoCommutativeOp | pcop.op = getTimes && pcop.right = n}
}

batchCommutes2: check {
	some dt: GCDT | all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
		all diff1, diff2, diff3: GCDTDiff | all opBase: Int |
		all batch1, batch2, batch3, batch4/*, batch5, batch6, batch7*/: GCDTBatch |
		//all batch8, batch9, batch10, batch11, batch12, batch13, batch14: GCDTBatch |
			(dt.cOps = cop1 + cop2 && dt.pcOps = pop) =>
			(diff1.op = cop1 && diff2.op = cop2 && diff3.op = pop) =>
			(batch1.type = dt && batch1.base = opBase && batch1.fold = iden) =>
			(batch1.ops = diff1 + diff2 + diff3) =>
		 		   batchStep[batch1,  batch2,  diff1]
				&& batchStep[batch2,  batch3,  diff2]
				&& batchStep[batch3,  batch4,  diff3]
				//&& batchStep[batch1,  batch5,  diff1]
				//&& batchStep[batch5,  batch6,  diff3]
				//&& batchStep[batch6,  batch4,  diff2]
				//&& batchStep[batch1,  batch7,  diff2]
				//&& batchStep[batch7,  batch8,  diff1]
				//&& batchStep[batch8,  batch4,  diff3]
				//&& batchStep[batch1,  batch9,  diff2]
				//&& batchStep[batch9,  batch10, diff3]
				//&& batchStep[batch10, batch4,  diff1]
				//&& batchStep[batch1,  batch11, diff3]
				//&& batchStep[batch11, batch12, diff1]
				//&& batchStep[batch12, batch4,  diff2]
				//&& batchStep[batch1,  batch13, diff3]
				//&& batchStep[batch13, batch14, diff2]
				//&& batchStep[batch14, batch2,  diff1]  -- FIXME: this is wrong. Should be batch4 
} for exactly 1 GCDT, 2 CommutativeOp, 1 PseudoCommutativeOp, 3 GCDTDiff, 6 Int, 4 GCDTBatch