64
(a) §
(b) §
In each of the following, replace p by
〈x: int→ 〈y: int→ 〈z: int→ x≥0 ∧ x2≤y ∧ ∀z: int· z2≤y ⇒ z≤x〉〉〉
and simplify, assuming x, y, z, u, w: int .
(c) §
= =
= = =
= =
p (x+y) (2×u + w) z
〈x: int→ 〈y: int→ 〈z: int→ x≥0 ∧ x2≤y ∧ ∀z: int· z2≤y ⇒ z≤x〉〉〉 (x+y) (2×u + w) z
Variables x , y , and z appear both locally and nonlocally. Variable z is introduced twice locally. To avoid confusion, I will rename the local variables to a , b , c , and d .
(Since the first local z is unused, I don’t need to rename it to c , but I will anyway.) 〈a: int→ 〈b: int→ 〈c: int→ a≥0 ∧ a2≤b ∧ ∀d: int· d2≤b ⇒ d≤a〉〉〉 (x+y) (2×u + w) z apply 3 times
x+y≥0 ∧ (x+y)2 ≤2×u+w ∧ ∀d:int·d2 ≤2×u+w⇒d≤x+y
p (x+y) (2×u + w)
〈x: int→ 〈y: int→ 〈z: int→ x≥0 ∧ x2≤y ∧ ∀z: int· z2≤y ⇒ z≤x〉〉〉 (x+y) (2×u + w)
Variables x , y , and z appear both locally and nonlocally. Variable z is introduced twice locally. To avoid confusion, I will rename the local variables to a , b , c , and d .
(Since the first local z is unused, I don’t need to rename it to c , but I will anyway.) 〈a: int→ 〈b: int→ 〈c: int→ a≥0 ∧ a2≤b ∧ ∀d: int· d2≤b ⇒ d≤a〉〉〉 (x+y) (2×u + w)
apply 2 times 〈c:int→x+y≥0∧(x+y)2≤2×u+w ∧∀d:int·d2≤2×u+w ⇒ d≤x+y〉
note that c is unused. int→(x+y≥0 ∧ (x+y)2 ≤2×u+w ∧ ∀d:int·d2 ≤2×u+w ⇒ d≤x+y)
p (x+z) (y+y) (2+z)
〈x: int→ 〈y: int→ 〈z: int→ x≥0 ∧ x2≤y ∧ ∀z: int· z2≤y ⇒ z≤x〉〉〉 (x+z) (y+y) (2+z)
Variables x , y , and z appear both locally and nonlocally. Variable z is introduced twice locally. To avoid confusion, I will rename the local variables to a , b , c , and d .
(Since the first local z is unused, I don’t need to rename it to c , but I will anyway.) 〈a: int→ 〈b: int→ 〈c: int→ a≥0 ∧ a2≤b ∧ ∀d: int· d2≤b ⇒ d≤a〉〉〉 (x+z) (y+y) (2+z) apply 3 times
x+z≥0∧(x+z)2 ≤y+y∧∀d:int·d2 ≤y+y ⇒ d≤x+z