static int A:static_default (C a0, C a1, int a2) { guard = tt; ret(level()) = level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ obj_level(a0) ⊔ obj_level(a1); ret(obj_level(a0)) = ⊤; ret(obj_level(a1)) = ⊤; ret(a0.~>a0) = tt; ret(a0.~>a1) = tt; ret(a1.~>a0) = tt; ret(a1.~>a1) = tt; } int A:default (C a0, C a1, int a2) { guard = tt; ret(level()) = level(a0) ⊔ level(a1) ⊔ level(a2) ⊔ level(this) ⊔ obj_level(a0) ⊔ obj_level(a1) ⊔ obj_level(this); ret(obj_level(a0)) = ⊤; ret(obj_level(a1)) = ⊤; ret(obj_level(this)) = ⊤; ret(a0.~>a0) = tt; ret(a0.~>a1) = tt; ret(a1.~>a0) = tt; ret(a1.~>a1) = tt; } C (A a0, C a1, int a2) { guard = tt; ret(obj_level(a0)) = ⊤; ret(obj_level(a1)) = ⊤; ret(obj_level(this)) = ⊤; ret(a1.~>a1) = tt; ret(a1.~>this) = tt; ret(this.~>a1) = tt; ret(this.~>this) = tt; }