A provenly correct translation of Fickle into Java