|- ∀x s k0 k1. ShiftXor (x,s,k0,k1) = x ≪ 4 + k0 ⊕ x + s ⊕ x ≫ 5 + k1 |- ∀y z k0 k1 k2 k3 s. Round ((y,z),(k0,k1,k2,k3),s) = (let s' = s + 0x9E3779B9w in let y' = y + ShiftXor (z,s',k0,k1) in ((y',z + ShiftXor (y',s',k2,k3)),(k0,k1,k2,k3),s')) |- ∀y z k0 k1 k2 k3 sum. InvRound ((y,z),(k0,k1,k2,k3),sum) = ((y − ShiftXor (z − ShiftXor (y,sum,k2,k3),sum,k0,k1), z − ShiftXor (y,sum,k2,k3)),(k0,k1,k2,k3),sum − 0x9E3779B9w) |- ∀s n. Rounds (n,s) = if n = 0w then s else Rounds (n − 1w,Round s) |- ∀s n. InvRounds (n,s) = if n = 0w then s else InvRounds (n − 1w,InvRound s) |- ∀keys txt. teaEncrypt (keys,txt) = (let (cipheredtxt,keys,sum) = Rounds (32w,txt,keys,0w) in cipheredtxt) |- ∀keys txt. teaDecrypt (keys,txt) = (let (plaintxt,keys,sum) = InvRounds (32w,txt,keys,0x9E3779B9w ≪ 5) in plaintxt)