proofs/containers/intrusive_doubly_linked_list/edits.bend
bend-collections-laws-containers@1.0.0.0 · 108 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/containers/intrusive_doubly_linked_list/model.bend as G
3import bend-collections-laws-containers@1.0.0.0/proofs/containers/intrusive_doubly_linked_list/shape.bend as S
4
5
6# Prepend preserves a whole reciprocal, unique chain. Identity comparison is
7# proof-only; the production algorithm still performs only its field accesses.
8def prepend_valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +un: G.unique(~N,~eq,xs), +away: G.away(~N,~eq,n,xs), +detached: {G.prev(~N, ~R, ~P, ~eq,g,n) == None{} : Maybe<&2,N>}, good: G.segment(~N, ~R, ~P, ~eq,g,None{},xs,None{})) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.attach(~N, ~R, ~P,g,r,n,G.first(~N,xs,None{})),r,Con{n,xs}):
9 match xs un away:
10 case Nil{} _ _:
11 ((Unit{},Unit{}),
12 (S.head_sh_self(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,g,n,None{}),r,Some{n},rsame),
13 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,None{}),r,Some{n}),n),G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,None{}),n),None{},S.prev_sh(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,None{}),r,Some{n},n),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,None{}),n),G.prev(~N, ~R, ~P, ~eq,g,n),None{},S.prev_sn(~N, ~R, ~P, ~eq,g,n,None{},n),detached)),
14 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,None{}),r,Some{n}),n),G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,None{}),n),None{},S.next_sh(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,None{}),r,Some{n},n),S.next_sn_self(~N, ~R, ~P, ~eq,g,n,None{},reflex(n))),Unit{}))))
15 case Con{+h,+tail} Tuple{+ah,+ut} Tuple{Tuple{+nh,+hn},+at}:
16 (((((nh,hn),at)),(ah,ut)),
17 (S.head_sh_self(~N, ~R, ~P,~req,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n},rsame),
18 (Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n}),n),G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),n),None{},S.prev_sh(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n},n),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),n),G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),n),None{},S.prev_sp_other(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n},n,hn),Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),n),G.prev(~N, ~R, ~P, ~eq,g,n),None{},S.prev_sn(~N, ~R, ~P, ~eq,g,n,Some{h},n),detached))),
19 (Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n}),n),G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),n),Some{h},S.next_sh(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n},n),Equal.trans(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),n),G.next(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),n),Some{h},S.next_sp(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n},n),S.next_sn_self(~N, ~R, ~P, ~eq,g,n,Some{h},reflex(n)))),
20 S.segment_sh_frame(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,g,n,Some{h}),h,Some{n}),r,Some{n},Con{h,tail},Some{n},None{},S.segment_first_prev(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,g,n,Some{h}),h,tail,None{},None{},Some{n},reflex(h),ah,S.segment_sn_frame(~N, ~R, ~P, ~eq,g,n,Some{h},Con{h,tail},None{},None{},((nh,hn),at),good)))))))
21
22
23def remove_head_valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, +rsame: {req(r,r) == True{} : Bool}, +un: G.unique(~N,~eq,xs), away: G.away(~N,~eq,n,xs), good: G.segment(~N, ~R, ~P, ~eq,g,Some{n},xs,None{})) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,None{},G.first(~N,xs,None{})),r,xs):
24 match xs un:
25 case Nil{} _:
26 (Unit{},(Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,G.sh(~N, ~R, ~P,g,r,None{}),n,None{}),r),G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,None{}),r),None{},S.head_sn(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,g,r,None{}),n,None{},r),S.head_sh_self(~N, ~R, ~P,~req,g,r,None{},rsame)),Unit{}))
27 case Con{+h,+tail} Tuple{+ah,+ut}:
28 ((ah,ut),
29 (Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,G.first(~N,xs,None{})),n,None{}),r),G.head(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,G.first(~N,xs,None{})),r),Some{h},S.head_sn(~N, ~R, ~P,~req,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,G.first(~N,xs,None{})),n,None{},r),S.head_sh_self(~N, ~R, ~P,~req,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,Some{h},rsame)),
30 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.sh(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,G.first(~N,xs,None{})),n,None{},Con{h,tail},None{},None{},away,S.segment_sh_frame(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,G.first(~N,xs,None{}),None{}),r,Some{h},Con{h,tail},None{},None{},S.segment_first_prev(~N, ~R, ~P, ~eq,g,h,tail,Some{n},None{},None{},reflex(h),ah,good)))))
31
32def optional_prefix(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +g: G.Graph<N,R,P>, +prefix: List<&2,N>, +suffix: List<&2,N>, +p: N, +n: N, dis: G.disjoint(~N,~eq,prefix,suffix), good: G.segment(~N, ~R, ~P, ~eq,g,None{},prefix,Some{n})) -> G.segment(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,G.first(~N,suffix,None{}),Some{p}),None{},prefix,Some{n}):
33 match suffix:
34 case Nil{}: good
35 case Con{+h,+tail}: S.segment_sp_frame(~N, ~R, ~P, ~eq,g,h,Some{p},prefix,None{},Some{n},S.disjoint_head(~N,~eq,prefix,h,tail,dis),good)
36
37def optional_suffix(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +suffix: List<&2,N>, +p: N, +n: N, un: G.unique(~N,~eq,suffix), good: G.segment(~N, ~R, ~P, ~eq,g,Some{n},suffix,None{})) -> G.segment(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,G.first(~N,suffix,None{}),Some{p}),Some{p},suffix,None{}):
38 match suffix un:
39 case Nil{} _: Unit{}
40 case Con{+h,+tail} Tuple{ah,ut}: S.segment_first_prev(~N, ~R, ~P, ~eq,g,h,tail,Some{n},None{},Some{p},reflex(h),ah,good)
41
42def cut_nonhead_root(~N: Data, ~R: Data, ~P: Data, ~req: R -> R -> Bool, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: N, +q: Maybe<&2,N>, +x: R) -> {G.head(~N, ~R, ~P,~req,G.cut(~N, ~R, ~P,g,r,n,Some{p},q),x) == G.head(~N, ~R, ~P,~req,g,x) : Maybe<&2,N>}:
43 match g q:
44 case G.Graph{ns,ps,rs,f} None{}: {==}
45 case G.Graph{ns,ps,rs,f} Some{h}: {==}
46
47def join_last(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, +a: List<&2,N>, +g: G.Graph<N,R,P>, +p: N, +b: List<&2,N>, ga: G.segment(~N, ~R, ~P, ~eq,g,None{},G.append(~N,a,Con{p,Nil{}}),G.first(~N,b,None{})), gb: G.segment(~N, ~R, ~P, ~eq,g,Some{p},b,None{})) -> G.segment(~N, ~R, ~P, ~eq,g,None{},G.append(~N,G.append(~N,a,Con{p,Nil{}}),b),None{}):
48 S.segment_join(~N, ~R, ~P, ~eq,G.append(~N,a,Con{p,Nil{}}),g,b,None{},None{},ga,
49 %Equal.sym(Maybe<&2,N>,G.last(~N,G.append(~N,a,Con{p,Nil{}}),None{}),Some{p},S.last_end(~N,a,p,None{})) : G.segment(~N, ~R, ~P, ~eq,g,_,b,None{})
50 gb)
51
52
53# The input is a zipper around the known member. Its premises are exactly
54# separate, unique prefix/member/suffix identities and their old field facts;
55# no postcondition is assumed. Prefix and suffix can have arbitrary lengths.
56def remove_nonhead_valid(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +a: List<&2,N>, +p: N, +b: List<&2,N>, +up: G.unique(~N,~eq,G.append(~N,a,Con{p,Nil{}})), +ub: G.unique(~N,~eq,b), +dis: G.disjoint(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b), +np: G.away(~N,~eq,n,G.append(~N,a,Con{p,Nil{}})), +nb: G.away(~N,~eq,n,b), root: {G.head(~N, ~R, ~P,~req,g,r) == G.first(~N,G.append(~N,a,Con{p,Nil{}}),None{}) : Maybe<&2,N>}, prefix: G.segment(~N, ~R, ~P, ~eq,g,None{},G.append(~N,a,Con{p,Nil{}}),Some{n}), suffix: G.segment(~N, ~R, ~P, ~eq,g,Some{n},b,None{})) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,Some{p},G.first(~N,b,None{})),r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b)):
57 (S.unique_join(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,up,ub,dis),
58 (Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,G.sn(~N, ~R, ~P,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{}),n,None{}),r),G.head(~N, ~R, ~P,~req,g,r),G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b),None{}),cut_nonhead_root(~N, ~R, ~P,~req,g,r,n,p,G.first(~N,b,None{}),r),
59 Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,g,r),G.first(~N,G.append(~N,a,Con{p,Nil{}}),None{}),G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b),None{}),root,
60 Equal.trans(Maybe<&2,N>,G.first(~N,G.append(~N,a,Con{p,Nil{}}),None{}),G.first(~N,G.append(~N,a,Con{p,Nil{}}),G.first(~N,b,None{})),G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b),None{}),S.first_end(~N,a,p,None{},G.first(~N,b,None{})),Equal.sym(Maybe<&2,N>,G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b),None{}),G.first(~N,G.append(~N,a,Con{p,Nil{}}),G.first(~N,b,None{})),S.first_append(~N,G.append(~N,a,Con{p,Nil{}}),b,None{}))))),
61 join_last(~N, ~R, ~P, ~eq,a,G.sn(~N, ~R, ~P,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{}),n,None{}),p,b,
62 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{}),n,None{},G.append(~N,a,Con{p,Nil{}}),None{},G.first(~N,b,None{}),np,
63 S.segment_sp_frame(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{},G.append(~N,a,Con{p,Nil{}}),None{},G.first(~N,b,None{}),np,
64 S.segment_last_next(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),a,p,None{},Some{n},G.first(~N,b,None{}),reflex(p),up,optional_prefix(~N, ~R, ~P, ~eq,g,G.append(~N,a,Con{p,Nil{}}),b,p,n,dis,prefix)))),
65 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.sp(~N, ~R, ~P,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{}),n,None{},b,Some{p},None{},nb,
66 S.segment_sp_frame(~N, ~R, ~P, ~eq,G.sn(~N, ~R, ~P,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{})),n,None{},b,Some{p},None{},nb,
67 S.segment_sn_frame(~N, ~R, ~P, ~eq,G.optional_prev(~N, ~R, ~P,g,G.first(~N,b,None{}),Some{p}),p,G.first(~N,b,None{}),b,Some{p},None{},S.disjoint_last(~N,~eq,a,p,b,dis),optional_suffix(~N, ~R, ~P, ~eq,~reflex,g,b,p,n,ub,suffix)))))))
68
69# Public semantic statements: all input facts are taken from valid(g,order).
70def prepend_preserves(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, rsame: {req(r,r) == True{} : Bool}, away: G.away(~N,~eq,n,xs), detached: {G.prev(~N, ~R, ~P, ~eq,g,n) == None{} : Maybe<&2,N>}, valid: G.valid(~N, ~R, ~P, ~eq, ~req,g,r,xs)) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.prepend(~N, ~R, ~P,~req,g,r,n),r,Con{n,xs}):
71 match valid:
72 case Tuple{un,Tuple{root,good}}:
73 %Equal.sym(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,g,r),G.first(~N,xs,None{}),root) : G.valid(~N, ~R, ~P, ~eq, ~req,G.attach(~N, ~R, ~P,g,r,n,_),r,Con{n,xs})
74 prepend_valid(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,xs,rsame,un,away,detached,good)
75
76def remove_head_preserves(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +xs: List<&2,N>, rsame: {req(r,r) == True{} : Bool}, valid: G.valid(~N, ~R, ~P, ~eq, ~req,g,r,Con{n,xs})) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.remove(~N, ~R, ~P, ~eq,g,r,n),r,xs):
77 match valid:
78 case Tuple{Tuple{away,un},Tuple{root,Tuple{hp,Tuple{hn,good}}}}:
79 %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,g,n),None{},hp) : G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,_,G.next(~N, ~R, ~P, ~eq,g,n)),r,xs)
80 %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,n),G.first(~N,xs,None{}),hn) : G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,None{},_),r,xs)
81 remove_head_valid(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,xs,rsame,un,away,good)
82
83def remove_nonhead_preserves(~N: Data, ~R: Data, ~P: Data, ~eq: N -> N -> Bool, ~req: R -> R -> Bool, ~reflex: @x: N -> {eq(x,x) == True{} : Bool}, +g: G.Graph<N,R,P>, +r: R, +n: N, +a: List<&2,N>, +p: N, +b: List<&2,N>, valid: G.valid(~N, ~R, ~P, ~eq, ~req,g,r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}))) -> G.valid(~N, ~R, ~P, ~eq, ~req,G.remove(~N, ~R, ~P, ~eq,g,r,n),r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b)):
84 match valid:
85 case Tuple{un0,Tuple{root,good0}}:
86 +un : G.unique(~N,~eq,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b})) = un0
87 +good : G.segment(~N, ~R, ~P, ~eq,g,None{},G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}),None{}) = good0
88 +remaining : G.unique(~N,~eq,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b)) = S.unique_delete(~N,~eq,G.append(~N,a,Con{p,Nil{}}),n,b,un)
89 +away : G.away(~N,~eq,n,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b)) = S.deleted_away(~N,~eq,G.append(~N,a,Con{p,Nil{}}),n,b,un)
90 %Equal.sym(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,g,n),Some{p},Equal.trans(Maybe<&2,N>,G.prev(~N, ~R, ~P, ~eq,g,n),G.last(~N,G.append(~N,a,Con{p,Nil{}}),None{}),Some{p},S.member_prev(~N, ~R, ~P, ~eq,G.append(~N,a,Con{p,Nil{}}),g,n,b,None{},None{},good),S.last_end(~N,a,p,None{}))) : G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,_,G.next(~N, ~R, ~P, ~eq,g,n)),r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b))
91 %Equal.sym(Maybe<&2,N>,G.next(~N, ~R, ~P, ~eq,g,n),G.first(~N,b,None{}),S.member_next(~N, ~R, ~P, ~eq,G.append(~N,a,Con{p,Nil{}}),g,n,b,None{},None{},good)) : G.valid(~N, ~R, ~P, ~eq, ~req,G.cut(~N, ~R, ~P,g,r,n,Some{p},_),r,G.append(~N,G.append(~N,a,Con{p,Nil{}}),b))
92 remove_nonhead_valid(~N, ~R, ~P, ~eq, ~req,~reflex,g,r,n,a,p,b,
93 S.unique_left(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,remaining),S.unique_right(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,remaining),S.disjoint_unique(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,remaining),
94 S.away_left(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,n,away),S.away_right(~N,~eq,G.append(~N,a,Con{p,Nil{}}),b,n,away),
95 Equal.trans(Maybe<&2,N>,G.head(~N, ~R, ~P,~req,g,r),G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}),None{}),G.first(~N,G.append(~N,a,Con{p,Nil{}}),None{}),root,Equal.trans(Maybe<&2,N>,G.first(~N,G.append(~N,G.append(~N,a,Con{p,Nil{}}),Con{n,b}),None{}),G.first(~N,G.append(~N,a,Con{p,Nil{}}),Some{n}),G.first(~N,G.append(~N,a,Con{p,Nil{}}),None{}),S.first_middle(~N,G.append(~N,a,Con{p,Nil{}}),n,b,None{}),S.first_end(~N,a,p,Some{n},None{}))),
96 S.prefix_segment(~N, ~R, ~P, ~eq,G.append(~N,a,Con{p,Nil{}}),g,n,b,None{},None{},good),S.suffix_segment(~N, ~R, ~P, ~eq,G.append(~N,a,Con{p,Nil{}}),g,n,b,None{},None{},good))
97
98def attach_frame(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +r: R, +n: N, +h: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.attach(~N, ~R, ~P,g,r,n,h)) == G.frame(~N, ~R, ~P,g) : P}:
99 match g h:
100 case G.Graph{ns,ps,rs,f} None{}: {==}
101 case G.Graph{ns,ps,rs,f} Some{x}: {==}
102
103def cut_frame(~N: Data, ~R: Data, ~P: Data, +g: G.Graph<N,R,P>, +r: R, +n: N, +p: Maybe<&2,N>, +q: Maybe<&2,N>) -> {G.frame(~N, ~R, ~P,G.cut(~N, ~R, ~P,g,r,n,p,q)) == G.frame(~N, ~R, ~P,g) : P}:
104 match g p q:
105 case G.Graph{ns,ps,rs,f} None{} None{}: {==}
106 case G.Graph{ns,ps,rs,f} None{} Some{x}: {==}
107 case G.Graph{ns,ps,rs,f} Some{x} None{}: {==}
108 case G.Graph{ns,ps,rs,f} Some{x} Some{y}: {==}