plus(2,2,4). succ(PredX, 2). -> PredX = 1 plus(1, 2, PredZ). succ(PredX, 1). -> PredX = 0 plus(0, 2, PredZ).