[ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_hdtl" "tr_uni_tls" "tr_uni_pap" "tr_uni_compose" * ]
[ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
[ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "tr_compose_pap" "tr_compose_compose" * ]
- [ "tr_pap ( ?@⧣❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
- [ "tr_pushs ( ⫯*[?]? )" * ]
+ [ "tr_pap ( ?@⧣❨?❩ )" "tr_pap_eq" "tr_pap_hdtl" "tr_pap_hdtl_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
+ [ "tr_pushs ( ⫯*[?]? )" "tr_pushs_tls" * ]
[ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
[ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
}
[ "nat_le ( ?≤? )" "nat_le_pred" "nat_le_plus" "nat_le_minus" "nat_le_minus_plus" "nat_le_max" * ]
[ "nat_max ( ?∨? )" * ]
[ "nat_minus ( ?-? )" "nat_minus_plus" * ]
- [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" * ]
+ [ "nat_plus ( ?+? )" "nat_plus_pred" "nat_plus_rplus" "nat_plus_pplus" * ]
[ "nat_rplus ( ?+? )" "nat_rplus_pplus" "nat_rplus_succ" * ]
[ "nat_pred ( ↓? )" "nat_pred_succ" * ]
[ "nat_succ ( ↑? )" "nat_succ_iter" "nat_succ_tri" * ]