Cardano Updates

Uncomment QuiescentResult lemmas

Prove positiveAccounts

Fix formatting and wrap applyAllLoop_gtZero

Refactor ValidState proof to expose applyInput_preserves_valid_state

Proof of applyInput_gtZero

Proof of reduceContractUntilQuiescent_gtZero

Use “subgoal” to simplify proofs and fix newState variable name in declarations

Add declarations for gtZero proofs

Adapt QuiescentResult to include state (commented out)

Rename Refund to Close. (#38)

Rename Refund to Close.

Prove equivalence between both formulations

Make PositiveAccounts theorems strictly greater than 0

Rename Refund to Close.

Rename Refund to Close.

Prove computeTransaction preserves valid_state

Prove applyAllLoop preserves valid_state