[ { "finite relocation with pairs" * } {
[ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
[ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
- [ "fr2_append ( ?@@? )" * ]
+ [ "fr2_append ( ?●? )" * ]
[ "fr2_plus ( ?+? )" * ]
- [ "fr2_map ( ◊ ) ( ❨?,?❩;? )" * ]
+ [ "fr2_map ( 𝐞 ) ( ❨?,?❩◗? )" * ]
}
]
[ { "total relocation" * } {
- [ "tr_map ( 𝐭❨?❩ )" "tr_nexts" "tr_eq" * ]
+ [ "tr_uni ( 𝐮❨?❩ )" * ]
+ [ "tr_id ( 𝐢 ) " * ]
+ [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
+ [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
+ [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
+ [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
}
]
[ { "partial relocation" * } {
[ "stream ( ? ⨮{?} ? )" * ]
}
]
+ [ { "lists" * } {
+ [ "list_append ( ?⨁{?}? )" "list_rcons ( ?⨭{?}? )" * ]
+ [ "list_length ( |?| )" * ]
+ [ "list ( ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" * ]
+ }
+ ]
[ { "" * } {
- [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" "list_length ( |?| )" * ]
[ "bool ( Ⓕ ) ( Ⓣ )" "bool_or" "bool_and" * ]
[ "ltc" "ltc_ctc" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "lstar_2a" * ]