More than 5 years have passed since last update.
WHILE_true.v
TheoremWHILE_true:forallbc,bequivbBTrue->cequiv(WHILEbDOcEND)(WHILEBTrueDOSKIPEND).Proof.move=>bcH.unfoldcequiv=>stst'.split=>HH.-destruct(WHILE_true_nontermbcstst'H).byassumption.-destruct(WHILE_true_nontermBTrueSKIPstst').-unfoldbequiv.byreflexivity.-byassumption.Qed.Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme