(mod (((alice_preimage new_validation_hash alice_share junk1 junk2 total) (ALICE_IMAGE BOB_MOVE)) conditions)
    (include *standard-cl-22*)
    (include assert.clinc)
    (include curry.clinc)

    (assert
        (not
            (all
                (not new_validation_hash)
                (= ALICE_IMAGE (sha256 alice_preimage))
                (= alice_share
                    (assign 
                        (junk3 result) (divmod (- alice_preimage BOB_MOVE) 3)
                        (if (not result)
                            (/ total 2)
                            (if (= result 2)
                                0
                                total
                            )
                        )
                    )
                )
            )
        )
        conditions
    )
)