mb

1 files changed, 4 insertions, 8 deletions

diff --git a/tempo.md b/tempo.md
index 15fa531..f180598 100644
--- a/tempo.md
+++ b/tempo.md
@@ -162,11 +162,6 @@ def | `[x] A=. A<x A` (| B)
 ^^ separate:
 the object(s) preceeding the combination of an input object. breaks down an input into its creating parts. using this on a static atomic object will return either itself.
 
-def ^ `[x y] |y=.+x` (A ^ B)
-^^ inside:
-shows that an axiom is part of another one.
-alternative definition: `[x y] (.+x)=y`
-
 def ! `.*0`
 ^^ ???:
 an indescribable, unknown, and paradoxical axiom.
@@ -261,7 +256,8 @@ any mind that is able to receive the information of this current axiom.
 
 def \comprehend\ `[x] A=x A=.\type\\listener\ B=\axiom\. C=@A @A = B+A @A\neq\C` (D \comprehend\)
 ^^ comprehension:
-indicates an axiom being transmitted to a listener, resulting in the change of the listener. it resolves to a `T`/`F` value, indicating whether the listener's mind has changed in comparison to an outcome in which the listener did not receive the axiom.
+indicates an axiom being transmitted to a listener, resulting in the change of the listener.
+it resolves to a `T`/`F` value, indicating whether the listener's mind has changed in comparison to an outcome in which the listener did not receive the axiom.
 this is also the first axiom, up to this point, to come *after* its generic argument.
 
 def \dawn\ `\inf\ * @\beginning\`
@@ -321,14 +317,14 @@ the axiom created from the void of comprehension.
 
 **note to all**: do not try to define love. poetry is not definition.
 
-def \all\ `[x y] -(A=.\type\x -(A^y))` (\all\ B C)
+def \all\ `[x y] -(A=.\type\x -(A\prop\y))` (\all\ B C)
 ^^ all:
 for all axioms of type B, every one of them exists inside C.
 
 def \some\ `[x y] -(\all\ x -y)` (\some\ A B)
 ^^ some:
 there exists an axiom of type A which is inside of B.
-alternative definition: `[x y] A=.\type\x A^y`
+alternative definition: `[x y] A=.\type\x A\prop\y`
 
 ## update log