Mercurial > hg > Members > ryokka > HoareLogic

changeset 51:3f4f93ac841d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author ryokka
date Wed, 18 Dec 2019 20:34:00 +0900
parents 2edb44c5bf52
children 0bde332e1215
files whileTestGears.agda
diffstat 1 files changed, 10 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/whileTestGears.agda	Wed Dec 18 20:08:58 2019 +0900
+++ b/whileTestGears.agda	Wed Dec 18 20:34:00 2019 +0900
@@ -94,6 +94,7 @@
 proofGears : {c10 :  ℕ } → Set
 proofGears {c10} = whileTest' {_} {_} {c10} (λ n p1 →  conversion1 n p1 (λ n1 p2 → whileLoop' n1 p2 (λ n2 →  ( vari n2 ≡ c10 )))) 
 
+
 -- proofGearsMeta : {c10 :  ℕ } →  proofGears {c10}
 -- proofGearsMeta {c10} = {!!} -- net yet done
 
@@ -144,8 +145,15 @@
 s3 : (e : EnvP) → varn (env e) ≡ 0 → vari (env e) ≡ c10 e
 s3 record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl = {!!}
 
-proofs : (c : ℕ) (e : EnvP) → vari (env e) ≡ c10 e
-proofs c e = s3 (s2 (s1 {!!}) {!!} {!!}) {!!}
+s1ors2 : (e : EnvP) → EnvP
+s1ors2 e = {!!}
+
+proofs : (c : ℕ) → (λ e → vari (env e) ≡ c10 e ) (s2 {!!} {!!} {!!})
+proofs c = {!!} -- s3 (s2 ({!!}) {!!} {!!}) {!!}
+
+s3' : (e : EnvP) → varn (env e) ≡ 0 → (ℕ → EnvP → vari (env e) ≡ c10 e) → vari (env e) ≡ c10 e
+s3' record { env = record { varn = .0 ; vari = vari₁ } ; c10 = c11 ; cx = cx₁ } refl proof = {!!}
+
 
 
 whileTestPwithProof : {l : Level} {t : Set l} → (c10 : ℕ ) → (next : (e : EnvP ) → t) → t