Properties
Properties are true expressions. They are used to prove theorems
a = a
(a + b) + c = a + (b + c)
a + b = b + a
a + 0 = a
a - b = a + (b ⋅ (-1))
a + (a ⋅ (-1)) = 0
(a ⋅ b) ⋅ c = a ⋅ (b ⋅ c)
a ⋅ b = b ⋅ a
a ⋅ 0 = 0
a ⋅ 1 = a
a / 1 = a
a / b = a ⋅ (1 / b)
a ⋅ (b + c) = (a ⋅ b) + (a ⋅ c)
1 + 2 = 3
value of cell 0 at time t = 0
expression a + b =
__add__(a, b)expression a * b =
__mul__(a, b)expression a == b =
__eq__(a, b)expression a > b =
__gt__(a, b)expression a < b =
__lt__(a, b)type of
x = e = "assign"type of
elif e: = "elif"type of
else: = "else"(pair ("while", x)) describes a loop = True
(pair ("if", x)) describes a loop = False
byte at ID: x, cell #0 at time t = 0
"A" in decimal = 65
"B" in decimal = 66
target_1.target_2 =
getattr(target1, target2)getattr(target_1, target_2) = value = setattr(target_1, target_2, value)object[key] = __getitem__(object, key)__getitem__(object, key) = value = __setitem__(object, key, value)the first token in (pair (name, some)) = name
(trio ("for", line, ex)) describes a loop = True
sum of unsigned integers [ 0, [ ] ] and [ 1, [ ] ] = [ 1, [ ] ]
reverse of s = result of dumping s to [ ]
reverse of remaining stack [ x, [ ] ] and already reversed stack ys = [ x, ys ]
reverse of remaining stack [ x, xs ] and already reversed stack ys = reverse of remaining stack xs and already reversed stack [ x, ys ]
reverse of remaining stack [ ] and already reversed stack [ ] = [ ]
reverse of xs = reverse of remaining stack xs and already reversed stack [ ]
result of dumping [ y, ys ] to xs = result of dumping ys to [ y, xs ]
result of dumping [ y, [ ] ] to xs = [ y, xs ]
result of dumping [ ] to xs = xs
result of appending y to xs = result of dumping (result of dumping xs to [ ]) to [ y, [ ] ]
result of appending y to xs = reverse of [ y, reverse of xs ]
compare bit 0 and bit 0 = [ 1, [ 0, [ ] ] ]
compare bit 1 and bit 0 = [ 0, [ 1, [ ] ] ]
compare bit 0 and bit 1 = [ 0, [ 0, [ ] ] ]
compare bit 1 and bit 1 = [ 1, [ 0, [ ] ] ]
compare bit stack [ x, [ ] ] and bit stack [ y, [ ] ] = compare bit x and bit y
minimum value of stack [ x, [ ] ] = x
maximum value in stack [ x, [ ] ] = x
[] = []
index of value value in numbers = index of value value in numbers with current index [ 0, [ ] ]
index of value v in els = index of value v in els with current index 0
index of value v in els = output of the index_compute function where the input stack is els, value is v, and index is 0
index of value val in els = index of value val in els with current index 0
index of the mininum value in stack els = index of value (minimum value of stack els) in els
index of the maximum value in stack els = index of value (maximum value in stack els) in els
bit xs minus bit 0 = xs
bit [ 1, xs ] minus bit 1 = [ 0, xs ]
bit [ 0, xs ] minus bit 1 = [ 1, bit xs minus bit 1 ]
remaining elements after xs is popped at index idx = remaining elements after xs is popped at index idx and visited stack is [ ]
remaining elements after [ x, xs ] is popped at index [ 0, [ ] ] and visited stack is ys = result of dumping xs to ys
remaining elements after [ x, xs ] is popped at index [ 1, [ ] ] and visited stack is result = remaining elements after xs is popped at index [ 0, [ ] ] and visited stack is [ x, result ]
remaining elements after [ x, xs ] is popped at index [ y0, [ y1, ys ] ] and visited stack is result = remaining elements after xs is popped at index (bit [ y0, [ y1, ys ] ] minus bit 1) and visited stack is [ x, result ]
remaining elements after [ x, xs ] is popped at index 0 and visited stack is ys = reverse of (result of dumping xs to ys)
remaining elements after [ x, xs ] is popped at index 0 and visited stack is ys = result of dumping ys to xs
remaining elements after [ x, xs ] is popped at index idx and visited stack is v = remaining elements after xs is popped at index (idx - 1) and visited stack is [ x, v ]
stack after popping a value from stack xs at index idx = reverse of (stack after popping a value from stack xs at index idx in traversed elements: [ ])
stack after popping a value from stack [ x, xs ] at index 0 in traversed elements: result = result of dumping xs to result
stack after popping a value from stack [ x, xs ] at index idx in traversed elements: result = stack after popping a value from stack xs at index (idx - 1) in traversed elements: [ x, result ]
result of sorting [ ] with sorted stack sl = sl
result of sorting [ el, rem ] with sorted stack sl = result of sorting (remaining elements after [ el, rem ] is popped at index (index of the maximum value in stack [ el, rem ])) with sorted stack [ maximum value in stack [ el, rem ], sl ]
result of sorting els = result of sorting els with sorted stack [ ]
the element at index 0 of stack [ x, y ] = x
the element at index i of stack [ x, y ] = the element at index (i - 1) of stack y
result of storing value at index idx of stack elements = set index idx of remaining stack elements to value with visited : [ ]
set index 0 of remaining stack [ x, rest ] to value with visited : visited = result of dumping [ value, visited ] to rest
set index idx of remaining stack [ x, rest ] to value with visited : y = set index (idx - 1) of remaining stack rest to value with visited : [ x, y ]
length of stack xs = length of remaining stack xs with count 0
length of remaining stack [ ] with count count = count
length of remaining stack [ x, y ] with count count = length of remaining stack y with count (count + 1)
stack [ ] contains x = False
result of storing value at key: key in map: entries = output of function store_compute where input key is key, value is value, map is entries, and processed map is [ ]
output of function store_compute where input key is key, value is value, map is [ ], and processed map is kvs = reverse of [ entry key: value, kvs ]
output of function store_compute where input key is key, value is value, map is [ ], and processed map is kvs = result of dumping kvs to [ entry key: value, [ ] ]
value at key in map [ pair (key, value), remaining ] = value
value at key in map [ pair (bad_key, value), remaining ] = value at key in map remaining
value at key in map [ entry key: value, remaining ] = value
value at key in map [ entry bad_key: value, remaining ] = value at key in map remaining
map [ entry key: value, remaining ] contains key key = True
map [ entry bad_key: value, remaining ] contains key key = map remaining contains key key
map [ ] contains key key = False
result of deleting the entry with key key from map entries = output of function delete_entry where input key is key, map is entries, and processed is [ ]
output of function delete_entry where input key is key, map is [ pair (key, value), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is kvs
output of function delete_entry where input key is key, map is [ pair (lkey, lvalue), remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ pair (lkey, lvalue), kvs ]
output of function delete_entry where input key is key, map is [ entry key: value, remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is kvs
output of function delete_entry where input key is key, map is [ entry lkey: lvalue, remaining ], and processed is kvs = output of function delete_entry where input key is key, map is remaining, and processed is [ entry lkey: lvalue, kvs ]
output of function delete_entry where input key is key, map is [ ], and processed is kvs = reverse of kvs
1
2