You can clone with
Cut the forward backward proof in half.
Add some code that does not work but is the right path.
Partial add of Loops.
Prove forward determinism of J1 statements.
Add loops and a mutual induction scheme for it.
Implement logical AND, OR.
Equality for expressions.
Add the operator of remainder.
Fix definition of Mul.
Introduce Janus1.v as the base for Janus1.
Update text and remove a completely wrong claim.
Document the statement inversion proof.
Prove correctness of statement inversion.
Fix the Janus0 definition.
Add the hide_write lemma on memories.
It is clever to make S_Skip part of Janus0.
Prove the expression equivalence *is* really an equivalence.
Add statement equivalence. Prove that it is reflexive, symmetric and …
…transitive. Prove semicolons as being associative.
Add the statement inverter.
Equivalence relation (i hope) on expressions.
Fixmes and backward determinism theorem.
More quick proof addons
Supply some more proofs on Memories.
Document forward determinism of j0 statements.
Finish proofs on Janus0.
Rename f_ext to equal_f.
Prove the forward direction.
Implement evaluation rules of Janus0
Style in BNF notation
Kill fixmes in the introduction.