# HG changeset patch
# User ryokka
# Date 1579158299 -32400
# Node ID 0927df986552bf9d5c2e3e1ed73d9bfe50fc325a
# Parent  4bbeb8d9e25049aff8215cc21c17babe6690001d
fix

diff -r 4bbeb8d9e250 -r 0927df986552 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Wed Jan 15 20:50:50 2020 +0900
+++ b/hoareBinaryTree.agda	Thu Jan 16 16:04:59 2020 +0900
@@ -95,6 +95,13 @@
 reverse した stack を使って find をチェックするかんじ?
 --}
 
+tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} →  (tree mtree : bt' A tn )
+  → (stack : List (bt'-path A )) → Set n
+tree+stack tree mtree [] = tree ≡ mtree
+tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-left key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack)
+tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack)
+-- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう
+
 tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} →  (tree mtree : bt' A tn )
   → (stack : List (bt'-path A )) →  (reverse stack) ≡ {!!}
 tree+stack≡tree tree (bt'-leaf key) stack = {!!}