Mercurial > hg > Members > ryokka > HoareLogic

comparison whileTestPrimProof.agda @ 24:e668962ac31a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rename modules
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 25 Dec 2018 08:45:06 +0900
parents 3968822b9693
children 62dcb0ae2c94
comparison
equal deleted inserted replaced
23:3968822b9693 24:e668962ac31a
8 open import Relation.Binary.PropositionalEquality 8 open import Relation.Binary.PropositionalEquality
9 9
10 open import utilities hiding ( _/\_ ) 10 open import utilities hiding ( _/\_ )
11 open import whileTestPrim 11 open import whileTestPrim
12 12
13 open import HoareData PrimComm Cond Axiom Tautology _and_ neg 13 open import Hoare PrimComm Cond Axiom Tautology _and_ neg
14 14
15 open Env 15 open Env
16 16
17 initCond : Cond 17 initCond : Cond
18 initCond env = true 18 initCond env = true
259 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl 259 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) () ref | false | false | refl
260 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl 260 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | false | true | refl = refl
261 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | () 261 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | false | ()
262 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl 262 axiomValid {l} bPre pcm bPost ax s1 .(pcm s1) semPre ref | true | true | refl = refl
263 263
264 open import Hoare 264 open import HoareSoundness
265 Cond 265 Cond
266 PrimComm 266 PrimComm
267 neg 267 neg
268 _and_ 268 _and_
269 Tautology 269 Tautology