Mercurial > hg > Papers > 2021 > soto-thesis

view paper/src/axiom-taut.agda.replaced @ 4:bf1f62556b81

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add while_test_init_imple
author soto
date Thu, 11 Feb 2021 17:03:31 +0900
parents 959f4b34d6f4
children
line wrap: on
line source

_@$\Rightarrow$@_ : Bool @$\rightarrow$@ Bool @$\rightarrow$@ Bool
false  @$\Rightarrow$@  _ = true
true  @$\Rightarrow$@  true = true
true  @$\Rightarrow$@  false = false

Axiom : Cond @$\rightarrow$@ PrimComm @$\rightarrow$@ Cond @$\rightarrow$@ Set
Axiom pre comm post = @$\forall$@ (env : Env) @$\rightarrow$@  (pre env) @$\Rightarrow$@ ( post (comm env)) @$\equiv$@ true

Tautology : Cond @$\rightarrow$@ Cond @$\rightarrow$@ Set
Tautology pre post = @$\forall$@ (env : Env) @$\rightarrow$@  (pre env)  @$\Rightarrow$@ (post env) @$\equiv$@ true