open gcdt2[Int]

fun plusFn []: Int one->one (Int one->one Int) {
	{opl, opr, res: Int |
		res = opl + opr
	}
}

fun plusOp []: Commutative {
	{c: Commutative |
		c.fn = plusFn[]
	}
}

fun mulFn []: Int one->one (Int one->one Int) {
	{opl, opr, res: Int |
		res = mul[opl, opr]
	}
}

fun mulOp []: PseudoCommutative {
	{pc: PseudoCommutative |
		pc.fn = mulFn[]
	}
}

fun intType []: GCDT {
	{dt: GCDT |
		dt.universe = Int &&
		dt.operations = {plusOp[] + mulOp[]}
	}
}

run intType for 5

basicReduction: check {
	all dt: GCDT | all r0: Reducer | all f1, f2, f3: Frame |
	(dt = intType[] && r0 = baseReducer[0]) =>
	(f1.op = plusOp[] && f1.right = 1) =>
	(f2.op = mulOp[] && f2.right = 2) =>
	(f3.op = plusOp[] && f3.right = 2) =>
		reduceOnce[dt, f3, reduceOnce[dt, f2, reduceOnce[dt, f1, r0]]].base = 6
} for 20