Mercurial > hg > Papers > 2020 > ryokka-master

comparison paper/src/AgdaNPushNPopProof.agda.replaced @ 5:196ba119ca89

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix, and add mindmap->pdf
author ryokka
date Mon, 03 Feb 2020 21:47:43 +0900
parents c7acb9211784
children
comparison
equal deleted inserted replaced
4:b5fffa8ae875 5:196ba119ca89
1 pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ 1 pop-n-push-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@
2 pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta 2 pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta
3 @$\equiv$@ M.exec (n-push n) meta 3 @$\equiv$@ M.exec (n-push n) meta
4 where 4 where
5 meta = id-meta cn ce s 5 meta = id-meta cn ce s
6 6
28 M.exec (n-push (suc n)) (id-meta cn ce s) 28 M.exec (n-push (suc n)) (id-meta cn ce s)
29 @$\blacksquare$@ 29 @$\blacksquare$@
30 30
31 31
32 32
33 n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\text{1}$@ 33 n-push-pop-type : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@ @$\rightarrow$@ SingleLinkedStack @$\mathbb{N}$@ @$\rightarrow$@ Set@$\_{1}$@
34 n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta @$\equiv$@ meta 34 n-push-pop-type n cn ce st = M.exec (M.csComp (n-pop n) (n-push n)) meta @$\equiv$@ meta
35 where 35 where
36 meta = id-meta cn ce st 36 meta = id-meta cn ce st
37 37
38 n-push-pop : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ n-push-pop-type n cn ce s 38 n-push-pop : (n cn ce : @$\mathbb{N}$@) @$\rightarrow$@ (s : SingleLinkedStack @$\mathbb{N}$@) @$\rightarrow$@ n-push-pop-type n cn ce s