for z being non zero Nat holds (2 |^ (2 |^ z)) mod 3 = 1