Trying to model Towers of Hanoi in SMT-LIB ( Using SMT-LIB is required for me!)

Question

I have been trying to model a towers of hanoi puzzle in SMT-LIB with z3 but have found it hard to keep track of how to follow each step and where each discs (goes speaking of rods)

I already have starter code which I think covers most of the needed logic but I am not sure how to model it the right way and also get the human-readable format at the end.

I am in need of assistance for SMT-Lib only solution as this is the point of my work

; timepoint for reached end state
(declare-const N Int)


; Define function for -> (disc step) rod)
(declare-fun D (Int Int) Int)

; How many discs are there
(declare-fun numDisc Int)

(assert (and

(= numDisc 2)

;start state
(forall ((discs Int))
    (imples (1 <= discs numDisc)
        (= (D discs 0) 0)
    )
)


;wanted end state
(forall ((discsEnd Int))
    (imples (1 <= discsEnd numDisc)
        (= (D discsEnd N) 2)
    )
)

(assert (forall ((t Int))
    (implies
        (and (>= t 0) (< t N)) ; for each time step t until N-1
        (exists (disc Int) (rodFrom Int) (rodTo Int)
            (and
                (and (>= disc 1) (<= disc numDisc)) ; disc is within the valid range
                (and (>= rodFrom 0) (<= rodFrom 2)) ; rodFrom is within the valid range
                (and (>= rodTo 0) (<= rodTo 2)) ; rodTo is within the valid range
                (distinct rodFrom rodTo) ; disc moves to a different rod
                (= (D disc t) rodFrom) ; disc is on rodFrom at time t
                (= (D disc (+ t 1)) rodTo) ; disc is on rodTo at time t+1
                ; Add constraints for other discs to remain the same
                (forall ((otherDisc Int))
                    (implies
                        (and (>= otherDisc 1) (<= otherDisc numDisc) (not (= otherDisc disc)))
                        (= (D otherDisc t) (D otherDisc (+ t 1)))
                    )
                )
                ; Add constraint for size (larger discs cannot be on top of smaller ones)
                (not
                    (> disc (+ disc 1))
                )
                ; This requires additional formulation
            )
        )
    )


)))

(check-sat)
(get-value (
    N
    (D 1 1)
))

I have not finished the get-value nor have I concluded on how to implement the checking at each step but I think this is a starter