I would like to know how to compose or group terms under an uninterpreted function in cvc5 python base API. Given some dot struct {i,j}, how can I construct a function which accepts some dot and returns dot{1,3}? Towards the bottom I construct a term (and (= apply_fn update_i) (= apply_fn update_j)), however this does not work.

How can I group or concatenate multiple terms (i.e. multi-line statements) to then later assert equal to an uninterpreted function?

#!/usr/bin/python3

import cvc5
from cvc5 import Kind


if __name__ == "__main__":

    solver = cvc5.Solver()
    solver.setLogic("ALL")

    int_sort = solver.getIntegerSort()


    dot_decl = solver.mkDatatypeDecl("dot")
    fields = solver.mkDatatypeConstructorDecl("fields")

    fields.addSelector("i",int_sort)
    fields.addSelector("j",int_sort)

    dot_decl.addConstructor(fields)

    dot_sort = solver.mkDatatypeSort(dot_decl)
    dot_ctsr = dot_sort.getDatatype().getConstructor("fields")

    dot_term = solver.mkTerm(
        Kind.APPLY_CONSTRUCTOR,
        dot_ctsr.getTerm(),
        solver.mkInteger(0),solver.mkInteger(0)
    )
    print(dot_term)
    # dot {i:0,j:0}

    #create i update term
    i_updater_term =  
        dot_ctsr 
        .getSelector("i") 
        .getUpdaterTerm()
    
    restart_i_term = solver.mkTerm(
        Kind.APPLY_UPDATER,
        i_updater_term,
        dot_term,
        solver.mkInteger(1)
    )

    #create j update term
    j_updater_term =  
        dot_ctsr 
        .getSelector("j") 
        .getUpdaterTerm()
    
    restart_j_term = solver.mkTerm(
        Kind.APPLY_UPDATER,
        j_updater_term,
        dot_term,
        solver.mkInteger(3)
    )

    #make function, f(dot) -> dot
    move_dot_fn_sort = solver.mkFunctionSort(
        dot_sort,
        dot_sort
    )
    move_dot_fn = solver.mkConst(
        move_dot_fn_sort,
        "move_dot"
    )

    # apply function
    apply_fn = solver.mkTerm(
        Kind.APPLY_UF,
        move_dot_fn,
        dot_term
    )
    # f(dot_i)
    f_i = solver.mkTerm(
        Kind.EQUAL,
        apply_fn,
        restart_i_term
    )
    # f(dot_j)
    f_j = solver.mkTerm(
        Kind.EQUAL,
        apply_fn,
        restart_j_term
    )
    #term that says to combine function
    fn = solver.mkTerm(
        Kind.AND,
        solver.mkTerm(
            Kind.EQUAL,
            apply_fn,
            restart_i_term
        ),
        solver.mkTerm(
            Kind.EQUAL,
            apply_fn,
            restart_j_term
        )
    )

    solver.assertFormula(f_i)
    sat = solver.checkSat()
    print(sat)
    solver.assertFormula(f_j)
    sat = solver.checkSat()
    print(sat)
    sat = solver.assertFormula(fn)
    sat = solver.checkSat()
    print(sat)

Output:

(fields 0 0)
sat
unsat
unsat