|
5
|
1 pop-n-push-type : !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! SingleLinkedStack !$\mathbb{N}$! !$\rightarrow$! Set!$\_{1}$!
|
|
0
|
2 pop-n-push-type n cn ce s = M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) meta
|
|
5
|
3 !$\equiv$! M.exec (n-push n) meta
|
|
0
|
4 where
|
|
|
5 meta = id-meta cn ce s
|
|
|
6
|
|
5
|
7 pop-n-push : (n cn ce : !$\mathbb{N}$!) !$\rightarrow$! (s : SingleLinkedStack !$\mathbb{N}$!) !$\rightarrow$! pop-n-push-type n cn ce s
|
|
0
|
8 pop-n-push zero cn ce s = refl
|
|
|
9 pop-n-push (suc n) cn ce s = begin
|
|
|
10 M.exec (M.csComp (M.cs popOnce) (n-push (suc (suc n)))) (id-meta cn ce s)
|
|
5
|
11 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
12 M.exec (M.csComp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce))) (id-meta cn ce s)
|
|
5
|
13 !$\equiv$!!$\langle$! exec-comp (M.cs popOnce) (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s) !$\rangle$!
|
|
0
|
14 M.exec (M.cs popOnce) (M.exec (M.csComp (n-push (suc n)) (M.cs pushOnce)) (id-meta cn ce s))
|
|
5
|
15 !$\equiv$!!$\langle$! cong (\x !$\rightarrow$! M.exec (M.cs popOnce) x) (exec-comp (n-push (suc n)) (M.cs pushOnce) (id-meta cn ce s)) !$\rangle$!
|
|
0
|
16 M.exec (M.cs popOnce) (M.exec (n-push (suc n))(M.exec (M.cs pushOnce) (id-meta cn ce s)))
|
|
5
|
17 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
18 M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))})))
|
|
5
|
19 !$\equiv$!!$\langle$! sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))) !$\rangle$!
|
|
0
|
20 M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
|
|
5
|
21 !$\equiv$!!$\langle$! pop-n-push n cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}) !$\rangle$!
|
|
0
|
22 M.exec (n-push n) (id-meta cn ce (record {top = just (cons ce (SingleLinkedStack.top s))}))
|
|
5
|
23 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
24 M.exec (n-push n) (pushOnce (id-meta cn ce s))
|
|
5
|
25 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
26 M.exec (n-push n) (M.exec (M.cs pushOnce) (id-meta cn ce s))
|
|
5
|
27 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
28 M.exec (n-push (suc n)) (id-meta cn ce s)
|
|
5
|
29 !$\blacksquare$!
|
|
0
|
30
|
|
|
31
|
|
|
32
|
|
5
|
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
|
|
0
|
35 where
|
|
|
36 meta = id-meta cn ce st
|
|
|
37
|
|
5
|
38 n-push-pop : (n cn ce : !$\mathbb{N}$!) !$\rightarrow$! (s : SingleLinkedStack !$\mathbb{N}$!) !$\rightarrow$! n-push-pop-type n cn ce s
|
|
0
|
39 n-push-pop zero cn ce s = refl
|
|
|
40 n-push-pop (suc n) cn ce s = begin
|
|
|
41 M.exec (M.csComp (n-pop (suc n)) (n-push (suc n))) (id-meta cn ce s)
|
|
5
|
42 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
|
43 M.exec (M.csComp (M.cs (\m !$\rightarrow$! M.exec (n-pop n) (popOnce m))) (n-push (suc n))) (id-meta cn ce s)
|
|
|
44 !$\equiv$!!$\langle$! exec-comp (M.cs (\m !$\rightarrow$! M.exec (n-pop n) (popOnce m))) (n-push (suc n)) (id-meta cn ce s) !$\rangle$!
|
|
|
45 M.exec (M.cs (\m !$\rightarrow$! M.exec (n-pop n) (popOnce m))) (M.exec (n-push (suc n)) (id-meta cn ce s))
|
|
|
46 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
47 M.exec (n-pop n) (popOnce (M.exec (n-push (suc n)) (id-meta cn ce s)))
|
|
5
|
48 !$\equiv$!!$\langle$! refl !$\rangle$!
|
|
0
|
49 M.exec (n-pop n) (M.exec (M.cs popOnce) (M.exec (n-push (suc n)) (id-meta cn ce s)))
|
|
5
|
50 !$\equiv$!!$\langle$! cong (\x !$\rightarrow$! M.exec (n-pop n) x) (sym (exec-comp (M.cs popOnce) (n-push (suc n)) (id-meta cn ce s))) !$\rangle$!
|
|
0
|
51 M.exec (n-pop n) (M.exec (M.csComp (M.cs popOnce) (n-push (suc n))) (id-meta cn ce s))
|
|
5
|
52 !$\equiv$!!$\langle$! cong (\x !$\rightarrow$! M.exec (n-pop n) x) (pop-n-push n cn ce s) !$\rangle$!
|
|
0
|
53 M.exec (n-pop n) (M.exec (n-push n) (id-meta cn ce s))
|
|
5
|
54 !$\equiv$!!$\langle$! sym (exec-comp (n-pop n) (n-push n) (id-meta cn ce s)) !$\rangle$!
|
|
0
|
55 M.exec (M.csComp (n-pop n) (n-push n)) (id-meta cn ce s)
|
|
5
|
56 !$\equiv$!!$\langle$! n-push-pop n cn ce s !$\rangle$!
|
|
0
|
57 id-meta cn ce s
|
|
5
|
58 !$\blacksquare$!
|
