Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestPrimProof.agda @ 63:222dd3869ab0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove wrong ==>
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 22 Dec 2019 09:15:44 +0900
parents 62dcb0ae2c94
children 9071e5a77a13
comparison
equal deleted inserted replaced
62:bfe7d83cf9ba 63:222dd3869ab0
204 _/\_ : Cond -> Cond -> Cond 204 _/\_ : Cond -> Cond -> Cond
205 b1 /\ b2 = b1 and b2 205 b1 /\ b2 = b1 and b2
206 206
207 _\/_ : Cond -> Cond -> Cond 207 _\/_ : Cond -> Cond -> Cond
208 b1 \/ b2 = neg (neg b1 /\ neg b2) 208 b1 \/ b2 = neg (neg b1 /\ neg b2)
209
210 _==>_ : Cond -> Cond -> Cond
211 b1 ==> b2 = neg (b1 \/ b2)
212 209
213 SemCond : Cond -> State -> Set 210 SemCond : Cond -> State -> Set
214 SemCond c p = c p ≡ true 211 SemCond c p = c p ≡ true
215 212
216 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 -> 213 tautValid : (b1 b2 : Cond) -> Tautology b1 b2 ->