LoginSignup
1
0

More than 5 years have passed since last update.

@yoshihiro503in株式会社proof ninja

Equiv_Jの練習問題 WHILE_true

Posted at
WHILE_true.v
Theorem WHILE_true: forall b c,
     bequiv b BTrue  ->
     cequiv
       (WHILE b DO c END)
       (WHILE BTrue DO SKIP END).
Proof.
 move => b c H.
 unfold cequiv => st st'.
 split => HH.
  - destruct(WHILE_true_nonterm b c st st' H). by assumption.

  - destruct(WHILE_true_nonterm BTrue SKIP st st').
    - unfold bequiv. by reflexivity.

    - by assumption.
Qed.
1
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
1
0