mirror of
https://github.com/ganelson/inform.git
synced 2024-07-08 18:14:21 +03:00
7 lines
502 B
Plaintext
7 lines
502 B
Plaintext
'new unary even': ok
|
|
'set P to << Forall x IN< kind = number (x) IN>: (x == y) ^ Exists z: (y == z) >>': p set to << ForAll x IN< kind=number(x) IN> : (x == y) ^ Exists z : (y == z) >>
|
|
'variables in P': valid: x bound y free z bound
|
|
'binding of P': << Exists y : ForAll x IN< kind=number(x) IN> : (x == y) ^ Exists z : (y == z) >>
|
|
'variables in binding of P': valid: x bound y bound z bound
|
|
'substitution of y = 777 in P': << ForAll x IN< kind=number(x) IN> : (x == '777') ^ Exists z : ('777' == z) >>
|