1	import Base
2	import ./text.bend as X
3	import ./glob.bend as G
4	import ./perm.bend as P
5	import ./options.bend as O
6	import ./profile.bend as PR
7	import ./eval.bend as V
8	import ./transitions.bend as TR
9	import ./rule_file.bend as F
10	import ./rule_capability.bend as RC
11	import ./rule_network.bend as RN
12	import ./rule_signal.bend as RS
13	import ./rule_ptrace.bend as RP
14	import ./rule_mount.bend as RM
15	import ./rule_dbus.bend as RD
16	import ./rule_change_profile.bend as RX
17	import ./LAWS.bend as Laws
18	
19	# Bool algebra
20	
21	def b.or_assoc(+a: Bool, +b: Bool, +c: Bool) -> {Bool.or(Bool.or(a, b), c) == Bool.or(a, Bool.or(b, c)) : Bool}:
22	  match a:
23	    case True{}:
24	      {==}
25	    case False{}:
26	      {==}
27	
28	def b.or_false_r(+a: Bool) -> {Bool.or(a, False{}) == a : Bool}:
29	  match a:
30	    case True{}:
31	      {==}
32	    case False{}:
33	      {==}
34	
35	def b.and_false_r(+a: Bool) -> {Bool.and(a, False{}) == False{} : Bool}:
36	  match a:
37	    case True{}:
38	      {==}
39	    case False{}:
40	      {==}
41	
42	def b.and_true_r(+a: Bool) -> {Bool.and(a, True{}) == a : Bool}:
43	  match a:
44	    case True{}:
45	      {==}
46	    case False{}:
47	      {==}
48	
49	# (p and n and f) or (p and q) is p and ((n and f) or q)
50	def b.factor(+p: Bool, +n: Bool, +f: Bool, +q: Bool) -> {Bool.or(Bool.and(Bool.and(p, n), f), Bool.and(p, q)) == Bool.and(p, Bool.or(Bool.and(n, f), q)) : Bool}:
51	  match p:
52	    case True{}:
53	      {==}
54	    case False{}:
55	      {==}
56	
57	# Globs: the matcher and the list model
58	
59	def b.disc(+b: Bool) -> Type:
60	  match b:
61	    case False{}:
62	      Unit
63	    case True{}:
64	      Empty
65	
66	def b.ft(+e: {False{} == True{} : Bool}) -> b.disc(True{}):
67	  %e : b.disc(_)
68	  Unit{}
69	
70	def b.absurd(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}:
71	  Empty.absurd({x == y : T}, b.ft(e))
72	
73	def b.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}:
74	  Empty.absurd({x == y : T}, b.ft(Equal.sym(Bool, True{}, False{}, e)))
75	
76	# the pieces d fit the tokens r after an empty first piece
77	def fe(+r: List<&2, G.AaGTok>, d: List<&2, List<&2, U32>>) -> Bool:
78	  match d:
79	    case Nil{}:
80	      False{}
81	    case Con{p, ps}:
82	      Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps))
83	
84	def fe_any(+r: List<&2, G.AaGTok>, ds: List<&2, List<&2, List<&2, U32>>>) -> Bool:
85	  match ds:
86	    case Nil{}:
87	      False{}
88	    case Con{d, t}:
89	      Bool.or(fe(r, d), fe_any(r, t))
90	
91	def fa_app(+seq: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(seq, G.AaGCuts.append(xs, ys)) == Bool.or(G.AaGSeq.fits_any(seq, xs), G.AaGSeq.fits_any(seq, ys)) : Bool}:
92	  match xs:
93	    case Nil{}:
94	      {==}
95	    case Con{d, t}:
96	      %Equal.sym(Bool, G.AaGSeq.fits_any(seq, G.AaGCuts.append(t, ys)), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)), fa_app(seq, t, ys)) : {Bool.or(G.AaGSeq.fits(seq, d), _) == Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)) : Bool}
97	      Equal.sym(Bool, Bool.or(Bool.or(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t)), G.AaGSeq.fits_any(seq, ys)), Bool.or(G.AaGSeq.fits(seq, d), Bool.or(G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys))), b.or_assoc(G.AaGSeq.fits(seq, d), G.AaGSeq.fits_any(seq, t), G.AaGSeq.fits_any(seq, ys)))
98	
99	def fe_app(+r: List<&2, G.AaGTok>, +xs: List<&2, List<&2, List<&2, U32>>>, +ys: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.append(xs, ys)) == Bool.or(fe_any(r, xs), fe_any(r, ys)) : Bool}:
100	  match xs:
101	    case Nil{}:
102	      {==}
103	    case Con{d, t}:
104	      %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(t, ys)), Bool.or(fe_any(r, t), fe_any(r, ys)), fe_app(r, t, ys)) : {Bool.or(fe(r, d), _) == Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)) : Bool}
105	      Equal.sym(Bool, Bool.or(Bool.or(fe(r, d), fe_any(r, t)), fe_any(r, ys)), Bool.or(fe(r, d), Bool.or(fe_any(r, t), fe_any(r, ys))), b.or_assoc(fe(r, d), fe_any(r, t), fe_any(r, ys)))
106	
107	# an empty first piece: no single-byte token fits it
108	def ef_char(+c: U32, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
109	  match ds:
110	    case Nil{}:
111	      {==}
112	    case Con{d, t}:
113	      ef_char(c, r, t)
114	
115	def ef_any(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
116	  match ds:
117	    case Nil{}:
118	      {==}
119	    case Con{d, t}:
120	      ef_any(r, t)
121	
122	def ef_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(ds)) == False{} : Bool}:
123	  match ds:
124	    case Nil{}:
125	      {==}
126	    case Con{d, t}:
127	      ef_class(n, rs, r, t)
128	
129	# ... and a star takes it
130	def ef_star(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
131	  match ds:
132	    case Nil{}:
133	      {==}
134	    case Con{d, t}:
135	      %ef_star(r, t) : {Bool.or(G.AaGSeq.fits(r, d), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
136	      {==}
137	
138	def ef_star2(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
139	  match ds:
140	    case Nil{}:
141	      {==}
142	    case Con{d, t}:
143	      %ef_star2(r, t) : {Bool.or(G.AaGSeq.fits(r, d), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
144	      {==}
145	
146	# a first piece that starts with h: a single-byte token takes h and leaves
147	# an empty piece
148	def gr_char(+c: U32, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_eq(h, c), fe_any(r, ds)) : Bool}:
149	  match ds:
150	    case Nil{}:
151	      Equal.sym(Bool, Bool.and(U32.is_eq(h, c), False{}), False{}, b.and_false_r(U32.is_eq(h, c)))
152	    case Con{d, t}:
153	      match d:
154	        case Nil{}:
155	          gr_char(c, r, h, t)
156	        case Con{p, ps}:
157	          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_eq(h, c), fe_any(r, t)), gr_char(c, r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_eq(h, c), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_eq(h, c), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
158	          b.factor(U32.is_eq(h, c), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
159	
160	def gr_any(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), fe_any(r, ds)) : Bool}:
161	  match ds:
162	    case Nil{}:
163	      Equal.sym(Bool, Bool.and(U32.is_ne(h, 47), False{}), False{}, b.and_false_r(U32.is_ne(h, 47)))
164	    case Con{d, t}:
165	      match d:
166	        case Nil{}:
167	          gr_any(r, h, t)
168	        case Con{p, ps}:
169	          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_ne(h, 47), fe_any(r, t)), gr_any(r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_ne(h, 47), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_ne(h, 47), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
170	          b.factor(U32.is_ne(h, 47), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
171	
172	def gr_class(+n: Bool, +rs: List<&2, G.AaGRange>, +r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, ds)) : Bool}:
173	  match ds:
174	    case Nil{}:
175	      Equal.sym(Bool, Bool.and(G.AaGClass.has(n, rs, h), False{}), False{}, b.and_false_r(G.AaGClass.has(n, rs, h)))
176	    case Con{d, t}:
177	      match d:
178	        case Nil{}:
179	          gr_class(n, rs, r, h, t)
180	        case Con{p, ps}:
181	          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, t)), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, t)), gr_class(n, rs, r, h, t)) : {Bool.or(Bool.and(Bool.and(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(G.AaGClass.has(n, rs, h), Bool.or(Bool.and(X.AaText.is_nil(p), G.AaGSeq.fits(r, ps)), fe_any(r, t))) : Bool}
182	          b.factor(G.AaGClass.has(n, rs, h), X.AaText.is_nil(p), G.AaGSeq.fits(r, ps), fe_any(r, t))
183	
184	# ... a star takes h if it is not '/', and goes on
185	def gr_star(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, ds)) == Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, ds)) : Bool}:
186	  match ds:
187	    case Nil{}:
188	      Equal.sym(Bool, Bool.and(U32.is_ne(h, 47), False{}), False{}, b.and_false_r(U32.is_ne(h, 47)))
189	    case Con{d, t}:
190	      match d:
191	        case Nil{}:
192	          gr_star(r, h, t)
193	        case Con{p, ps}:
194	          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, t)), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t)), gr_star(r, h, t)) : {Bool.or(Bool.and(Bool.and(U32.is_ne(h, 47), G.AaGPiece.no_slash(p)), G.AaGSeq.fits(r, ps)), _) == Bool.and(U32.is_ne(h, 47), Bool.or(Bool.and(G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps)), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))) : Bool}
195	          b.factor(U32.is_ne(h, 47), G.AaGPiece.no_slash(p), G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, t))
196	
197	# ... a double star takes any h
198	def gr_star2(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, ds)) == G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, ds) : Bool}:
199	  match ds:
200	    case Nil{}:
201	      {==}
202	    case Con{d, t}:
203	      match d:
204	        case Nil{}:
205	          gr_star2(r, h, t)
206	        case Con{p, ps}:
207	          %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, t)), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t), gr_star2(r, h, t)) : {Bool.or(G.AaGSeq.fits(r, ps), _) == Bool.or(G.AaGSeq.fits(r, ps), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, t)) : Bool}
208	          {==}
209	
210	# cutting into one more piece and asking for an empty first piece is cutting into as many
211	def fe_ef(+r: List<&2, G.AaGTok>, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.empty_first(ds)) == G.AaGSeq.fits_any(r, ds) : Bool}:
212	  match ds:
213	    case Nil{}:
214	      {==}
215	    case Con{d, t}:
216	      %fe_ef(r, t) : {Bool.or(G.AaGSeq.fits(r, d), fe_any(r, G.AaGCuts.empty_first(t))) == Bool.or(G.AaGSeq.fits(r, d), _) : Bool}
217	      {==}
218	
219	def fe_gr(+r: List<&2, G.AaGTok>, +h: U32, +ds: List<&2, List<&2, List<&2, U32>>>) -> {fe_any(r, G.AaGCuts.grow(h, ds)) == False{} : Bool}:
220	  match ds:
221	    case Nil{}:
222	      {==}
223	    case Con{d, t}:
224	      match d:
225	        case Nil{}:
226	          fe_gr(r, h, t)
227	        case Con{p, ps}:
228	          fe_gr(r, h, t)
229	
230	def fe_cuts(+r: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), s)) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), s)) : Bool}:
231	  match s:
232	    case Nil{}:
233	      fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))
234	    case Con{h, t}:
235	      %Equal.sym(Bool, fe_any(r, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fe_app(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {_ == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
236	      %Equal.sym(Bool, fe_any(r, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), fe_ef(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(_, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
237	      %Equal.sym(Bool, fe_any(r, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), False{}, fe_gr(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) == G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})) : Bool}
238	      b.or_false_r(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})))
239	
240	# the matcher agrees with the list model: induction on the sequence, and on
241	# the path under a star
242	def glob.thm(+seq: List<&2, G.AaGTok>, +s: List<&2, U32>) -> {G.AaGSeq.matches(seq, s) == G.AaGSeq.model(seq, s) : Bool}:
243	  match seq:
244	    case Nil{}:
245	      match s:
246	        case Nil{}:
247	          {==}
248	        case Con{h, t}:
249	          {==}
250	    case Con{tok, r}:
251	      match tok:
252	        case G.AaGChar{c}:
253	          match s:
254	            case Nil{}:
255	              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
256	            case Con{h, t}:
257	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == _ : Bool}
258	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_char(c, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
259	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGChar{c}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_eq(h, c), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_char(c, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
260	              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
261	              %glob.thm(r, t) : {Bool.and(U32.is_eq(h, c), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_eq(h, c), _)) : Bool}
262	              {==}
263	        case G.AaGAny{}:
264	          match s:
265	            case Nil{}:
266	              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
267	            case Con{h, t}:
268	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == _ : Bool}
269	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
270	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGAny{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_any(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
271	              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
272	              %glob.thm(r, t) : {Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(U32.is_ne(h, 47), _)) : Bool}
273	              {==}
274	        case G.AaGClass{n, rs}:
275	          match s:
276	            case Nil{}:
277	              Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})))
278	            case Con{h, t}:
279	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == _ : Bool}
280	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), False{}, ef_class(n, rs, r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
281	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGClass{n, rs}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(G.AaGClass.has(n, rs, h), fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_class(n, rs, r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, _) : Bool}
282	              %Equal.sym(Bool, fe_any(r, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), t)), fe_cuts(r, t)) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
283	              %glob.thm(r, t) : {Bool.and(G.AaGClass.has(n, rs, h), G.AaGSeq.matches(r, t)) == Bool.or(False{}, Bool.and(G.AaGClass.has(n, rs, h), _)) : Bool}
284	              {==}
285	        case G.AaGStar{}:
286	          match s:
287	            case Nil{}:
288	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
289	              glob.thm(r, Nil{})
290	            case Con{h, t}:
291	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == _ : Bool}
292	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
293	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), gr_star(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
294	              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(_, Bool.and(U32.is_ne(h, 47), G.AaGSeq.fits_any(Con{G.AaGStar{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
295	              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), G.AaGSeq.matches(Con{G.AaGStar{}, r}, t))) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), Bool.and(U32.is_ne(h, 47), _)) : Bool}
296	              {==}
297	        case G.AaGStar2{}:
298	          match s:
299	            case Nil{}:
300	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Nil{}))) : {G.AaGSeq.matches(r, Nil{}) == _ : Bool}
301	              glob.thm(r, Nil{})
302	            case Con{h, t}:
303	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.append(G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), Bool.or(G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))), fa_app(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == _ : Bool}
304	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.empty_first(G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))), G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), ef_star2(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t}))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)))) : Bool}
305	              %Equal.sym(Bool, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.grow(h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))), G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t)), gr_star2(r, h, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.fits_any(r, G.AaGCuts.all(G.AaGSeq.len(r), Con{h, t})), _) : Bool}
306	              %glob.thm(r, Con{h, t}) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(_, G.AaGSeq.fits_any(Con{G.AaGStar2{}, r}, G.AaGCuts.all(1n+G.AaGSeq.len(r), t))) : Bool}
307	              %glob.thm(seq, t) : {Bool.or(G.AaGSeq.matches(r, Con{h, t}), G.AaGSeq.matches(Con{G.AaGStar2{}, r}, t)) == Bool.or(G.AaGSeq.matches(r, Con{h, t}), _) : Bool}
308	              {==}
309	
310	# The fast matcher equals the backtracking one
311	
312	# the propositional identities each token's step comes to
313	
314	def nfa.taut_nil(+a: Bool, +n: Bool, +c: Bool, +b: Bool) -> {Bool.and(a, n) == Bool.or(Bool.and(a, n), Bool.or(Bool.and(c, False{}), Bool.and(b, False{}))) : Bool}:
315	  match a:
316	    case True{}:
317	      match n:
318	        case True{}:
319	          match c:
320	            case True{}:
321	              match b:
322	                case True{}:
323	                  {==}
324	                case False{}:
325	                  {==}
326	            case False{}:
327	              match b:
328	                case True{}:
329	                  {==}
330	                case False{}:
331	                  {==}
332	        case False{}:
333	          match c:
334	            case True{}:
335	              match b:
336	                case True{}:
337	                  {==}
338	                case False{}:
339	                  {==}
340	            case False{}:
341	              match b:
342	                case True{}:
343	                  {==}
344	                case False{}:
345	                  {==}
346	    case False{}:
347	      match n:
348	        case True{}:
349	          match c:
350	            case True{}:
351	              match b:
352	                case True{}:
353	                  {==}
354	                case False{}:
355	                  {==}
356	            case False{}:
357	              match b:
358	                case True{}:
359	                  {==}
360	                case False{}:
361	                  {==}
362	        case False{}:
363	          match c:
364	            case True{}:
365	              match b:
366	                case True{}:
367	                  {==}
368	                case False{}:
369	                  {==}
370	            case False{}:
371	              match b:
372	                case True{}:
373	                  {==}
374	                case False{}:
375	                  {==}
376	
377	def nfa.taut_adv(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), False{}), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), e), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.and(e, q)), Bool.or(Bool.and(hb, Bool.and(e, q)), z))) : Bool}:
378	  match hb:
379	    case True{}:
380	      match cin:
381	        case True{}:
382	          match ain:
383	            case True{}:
384	              match e:
385	                case True{}:
386	                  match p:
387	                    case True{}:
388	                      match q:
389	                        case True{}:
390	                          match r:
391	                            case True{}:
392	                              match z:
393	                                case True{}:
394	                                  {==}
395	                                case False{}:
396	                                  {==}
397	                            case False{}:
398	                              match z:
399	                                case True{}:
400	                                  {==}
401	                                case False{}:
402	                                  {==}
403	                        case False{}:
404	                          match r:
405	                            case True{}:
406	                              match z:
407	                                case True{}:
408	                                  {==}
409	                                case False{}:
410	                                  {==}
411	                            case False{}:
412	                              match z:
413	                                case True{}:
414	                                  {==}
415	                                case False{}:
416	                                  {==}
417	                    case False{}:
418	                      match q:
419	                        case True{}:
420	                          match r:
421	                            case True{}:
422	                              match z:
423	                                case True{}:
424	                                  {==}
425	                                case False{}:
426	                                  {==}
427	                            case False{}:
428	                              match z:
429	                                case True{}:
430	                                  {==}
431	                                case False{}:
432	                                  {==}
433	                        case False{}:
434	                          match r:
435	                            case True{}:
436	                              match z:
437	                                case True{}:
438	                                  {==}
439	                                case False{}:
440	                                  {==}
441	                            case False{}:
442	                              match z:
443	                                case True{}:
444	                                  {==}
445	                                case False{}:
446	                                  {==}
447	                case False{}:
448	                  match p:
449	                    case True{}:
450	                      match q:
451	                        case True{}:
452	                          match r:
453	                            case True{}:
454	                              match z:
455	                                case True{}:
456	                                  {==}
457	                                case False{}:
458	                                  {==}
459	                            case False{}:
460	                              match z:
461	                                case True{}:
462	                                  {==}
463	                                case False{}:
464	                                  {==}
465	                        case False{}:
466	                          match r:
467	                            case True{}:
468	                              match z:
469	                                case True{}:
470	                                  {==}
471	                                case False{}:
472	                                  {==}
473	                            case False{}:
474	                              match z:
475	                                case True{}:
476	                                  {==}
477	                                case False{}:
478	                                  {==}
479	                    case False{}:
480	                      match q:
481	                        case True{}:
482	                          match r:
483	                            case True{}:
484	                              match z:
485	                                case True{}:
486	                                  {==}
487	                                case False{}:
488	                                  {==}
489	                            case False{}:
490	                              match z:
491	                                case True{}:
492	                                  {==}
493	                                case False{}:
494	                                  {==}
495	                        case False{}:
496	                          match r:
497	                            case True{}:
498	                              match z:
499	                                case True{}:
500	                                  {==}
501	                                case False{}:
502	                                  {==}
503	                            case False{}:
504	                              match z:
505	                                case True{}:
506	                                  {==}
507	                                case False{}:
508	                                  {==}
509	            case False{}:
510	              match e:
511	                case True{}:
512	                  match p:
513	                    case True{}:
514	                      match q:
515	                        case True{}:
516	                          match r:
517	                            case True{}:
518	                              match z:
519	                                case True{}:
520	                                  {==}
521	                                case False{}:
522	                                  {==}
523	                            case False{}:
524	                              match z:
525	                                case True{}:
526	                                  {==}
527	                                case False{}:
528	                                  {==}
529	                        case False{}:
530	                          match r:
531	                            case True{}:
532	                              match z:
533	                                case True{}:
534	                                  {==}
535	                                case False{}:
536	                                  {==}
537	                            case False{}:
538	                              match z:
539	                                case True{}:
540	                                  {==}
541	                                case False{}:
542	                                  {==}
543	                    case False{}:
544	                      match q:
545	                        case True{}:
546	                          match r:
547	                            case True{}:
548	                              match z:
549	                                case True{}:
550	                                  {==}
551	                                case False{}:
552	                                  {==}
553	                            case False{}:
554	                              match z:
555	                                case True{}:
556	                                  {==}
557	                                case False{}:
558	                                  {==}
559	                        case False{}:
560	                          match r:
561	                            case True{}:
562	                              match z:
563	                                case True{}:
564	                                  {==}
565	                                case False{}:
566	                                  {==}
567	                            case False{}:
568	                              match z:
569	                                case True{}:
570	                                  {==}
571	                                case False{}:
572	                                  {==}
573	                case False{}:
574	                  match p:
575	                    case True{}:
576	                      match q:
577	                        case True{}:
578	                          match r:
579	                            case True{}:
580	                              match z:
581	                                case True{}:
582	                                  {==}
583	                                case False{}:
584	                                  {==}
585	                            case False{}:
586	                              match z:
587	                                case True{}:
588	                                  {==}
589	                                case False{}:
590	                                  {==}
591	                        case False{}:
592	                          match r:
593	                            case True{}:
594	                              match z:
595	                                case True{}:
596	                                  {==}
597	                                case False{}:
598	                                  {==}
599	                            case False{}:
600	                              match z:
601	                                case True{}:
602	                                  {==}
603	                                case False{}:
604	                                  {==}
605	                    case False{}:
606	                      match q:
607	                        case True{}:
608	                          match r:
609	                            case True{}:
610	                              match z:
611	                                case True{}:
612	                                  {==}
613	                                case False{}:
614	                                  {==}
615	                            case False{}:
616	                              match z:
617	                                case True{}:
618	                                  {==}
619	                                case False{}:
620	                                  {==}
621	                        case False{}:
622	                          match r:
623	                            case True{}:
624	                              match z:
625	                                case True{}:
626	                                  {==}
627	                                case False{}:
628	                                  {==}
629	                            case False{}:
630	                              match z:
631	                                case True{}:
632	                                  {==}
633	                                case False{}:
634	                                  {==}
635	        case False{}:
636	          match ain:
637	            case True{}:
638	              match e:
639	                case True{}:
640	                  match p:
641	                    case True{}:
642	                      match q:
643	                        case True{}:
644	                          match r:
645	                            case True{}:
646	                              match z:
647	                                case True{}:
648	                                  {==}
649	                                case False{}:
650	                                  {==}
651	                            case False{}:
652	                              match z:
653	                                case True{}:
654	                                  {==}
655	                                case False{}:
656	                                  {==}
657	                        case False{}:
658	                          match r:
659	                            case True{}:
660	                              match z:
661	                                case True{}:
662	                                  {==}
663	                                case False{}:
664	                                  {==}
665	                            case False{}:
666	                              match z:
667	                                case True{}:
668	                                  {==}
669	                                case False{}:
670	                                  {==}
671	                    case False{}:
672	                      match q:
673	                        case True{}:
674	                          match r:
675	                            case True{}:
676	                              match z:
677	                                case True{}:
678	                                  {==}
679	                                case False{}:
680	                                  {==}
681	                            case False{}:
682	                              match z:
683	                                case True{}:
684	                                  {==}
685	                                case False{}:
686	                                  {==}
687	                        case False{}:
688	                          match r:
689	                            case True{}:
690	                              match z:
691	                                case True{}:
692	                                  {==}
693	                                case False{}:
694	                                  {==}
695	                            case False{}:
696	                              match z:
697	                                case True{}:
698	                                  {==}
699	                                case False{}:
700	                                  {==}
701	                case False{}:
702	                  match p:
703	                    case True{}:
704	                      match q:
705	                        case True{}:
706	                          match r:
707	                            case True{}:
708	                              match z:
709	                                case True{}:
710	                                  {==}
711	                                case False{}:
712	                                  {==}
713	                            case False{}:
714	                              match z:
715	                                case True{}:
716	                                  {==}
717	                                case False{}:
718	                                  {==}
719	                        case False{}:
720	                          match r:
721	                            case True{}:
722	                              match z:
723	                                case True{}:
724	                                  {==}
725	                                case False{}:
726	                                  {==}
727	                            case False{}:
728	                              match z:
729	                                case True{}:
730	                                  {==}
731	                                case False{}:
732	                                  {==}
733	                    case False{}:
734	                      match q:
735	                        case True{}:
736	                          match r:
737	                            case True{}:
738	                              match z:
739	                                case True{}:
740	                                  {==}
741	                                case False{}:
742	                                  {==}
743	                            case False{}:
744	                              match z:
745	                                case True{}:
746	                                  {==}
747	                                case False{}:
748	                                  {==}
749	                        case False{}:
750	                          match r:
751	                            case True{}:
752	                              match z:
753	                                case True{}:
754	                                  {==}
755	                                case False{}:
756	                                  {==}
757	                            case False{}:
758	                              match z:
759	                                case True{}:
760	                                  {==}
761	                                case False{}:
762	                                  {==}
763	            case False{}:
764	              match e:
765	                case True{}:
766	                  match p:
767	                    case True{}:
768	                      match q:
769	                        case True{}:
770	                          match r:
771	                            case True{}:
772	                              match z:
773	                                case True{}:
774	                                  {==}
775	                                case False{}:
776	                                  {==}
777	                            case False{}:
778	                              match z:
779	                                case True{}:
780	                                  {==}
781	                                case False{}:
782	                                  {==}
783	                        case False{}:
784	                          match r:
785	                            case True{}:
786	                              match z:
787	                                case True{}:
788	                                  {==}
789	                                case False{}:
790	                                  {==}
791	                            case False{}:
792	                              match z:
793	                                case True{}:
794	                                  {==}
795	                                case False{}:
796	                                  {==}
797	                    case False{}:
798	                      match q:
799	                        case True{}:
800	                          match r:
801	                            case True{}:
802	                              match z:
803	                                case True{}:
804	                                  {==}
805	                                case False{}:
806	                                  {==}
807	                            case False{}:
808	                              match z:
809	                                case True{}:
810	                                  {==}
811	                                case False{}:
812	                                  {==}
813	                        case False{}:
814	                          match r:
815	                            case True{}:
816	                              match z:
817	                                case True{}:
818	                                  {==}
819	                                case False{}:
820	                                  {==}
821	                            case False{}:
822	                              match z:
823	                                case True{}:
824	                                  {==}
825	                                case False{}:
826	                                  {==}
827	                case False{}:
828	                  match p:
829	                    case True{}:
830	                      match q:
831	                        case True{}:
832	                          match r:
833	                            case True{}:
834	                              match z:
835	                                case True{}:
836	                                  {==}
837	                                case False{}:
838	                                  {==}
839	                            case False{}:
840	                              match z:
841	                                case True{}:
842	                                  {==}
843	                                case False{}:
844	                                  {==}
845	                        case False{}:
846	                          match r:
847	                            case True{}:
848	                              match z:
849	                                case True{}:
850	                                  {==}
851	                                case False{}:
852	                                  {==}
853	                            case False{}:
854	                              match z:
855	                                case True{}:
856	                                  {==}
857	                                case False{}:
858	                                  {==}
859	                    case False{}:
860	                      match q:
861	                        case True{}:
862	                          match r:
863	                            case True{}:
864	                              match z:
865	                                case True{}:
866	                                  {==}
867	                                case False{}:
868	                                  {==}
869	                            case False{}:
870	                              match z:
871	                                case True{}:
872	                                  {==}
873	                                case False{}:
874	                                  {==}
875	                        case False{}:
876	                          match r:
877	                            case True{}:
878	                              match z:
879	                                case True{}:
880	                                  {==}
881	                                case False{}:
882	                                  {==}
883	                            case False{}:
884	                              match z:
885	                                case True{}:
886	                                  {==}
887	                                case False{}:
888	                                  {==}
889	    case False{}:
890	      match cin:
891	        case True{}:
892	          match ain:
893	            case True{}:
894	              match e:
895	                case True{}:
896	                  match p:
897	                    case True{}:
898	                      match q:
899	                        case True{}:
900	                          match r:
901	                            case True{}:
902	                              match z:
903	                                case True{}:
904	                                  {==}
905	                                case False{}:
906	                                  {==}
907	                            case False{}:
908	                              match z:
909	                                case True{}:
910	                                  {==}
911	                                case False{}:
912	                                  {==}
913	                        case False{}:
914	                          match r:
915	                            case True{}:
916	                              match z:
917	                                case True{}:
918	                                  {==}
919	                                case False{}:
920	                                  {==}
921	                            case False{}:
922	                              match z:
923	                                case True{}:
924	                                  {==}
925	                                case False{}:
926	                                  {==}
927	                    case False{}:
928	                      match q:
929	                        case True{}:
930	                          match r:
931	                            case True{}:
932	                              match z:
933	                                case True{}:
934	                                  {==}
935	                                case False{}:
936	                                  {==}
937	                            case False{}:
938	                              match z:
939	                                case True{}:
940	                                  {==}
941	                                case False{}:
942	                                  {==}
943	                        case False{}:
944	                          match r:
945	                            case True{}:
946	                              match z:
947	                                case True{}:
948	                                  {==}
949	                                case False{}:
950	                                  {==}
951	                            case False{}:
952	                              match z:
953	                                case True{}:
954	                                  {==}
955	                                case False{}:
956	                                  {==}
957	                case False{}:
958	                  match p:
959	                    case True{}:
960	                      match q:
961	                        case True{}:
962	                          match r:
963	                            case True{}:
964	                              match z:
965	                                case True{}:
966	                                  {==}
967	                                case False{}:
968	                                  {==}
969	                            case False{}:
970	                              match z:
971	                                case True{}:
972	                                  {==}
973	                                case False{}:
974	                                  {==}
975	                        case False{}:
976	                          match r:
977	                            case True{}:
978	                              match z:
979	                                case True{}:
980	                                  {==}
981	                                case False{}:
982	                                  {==}
983	                            case False{}:
984	                              match z:
985	                                case True{}:
986	                                  {==}
987	                                case False{}:
988	                                  {==}
989	                    case False{}:
990	                      match q:
991	                        case True{}:
992	                          match r:
993	                            case True{}:
994	                              match z:
995	                                case True{}:
996	                                  {==}
997	                                case False{}:
998	                                  {==}
999	                            case False{}:
1000	                              match z:
1001	                                case True{}:
1002	                                  {==}
1003	                                case False{}:
1004	                                  {==}
1005	                        case False{}:
1006	                          match r:
1007	                            case True{}:
1008	                              match z:
1009	                                case True{}:
1010	                                  {==}
1011	                                case False{}:
1012	                                  {==}
1013	                            case False{}:
1014	                              match z:
1015	                                case True{}:
1016	                                  {==}
1017	                                case False{}:
1018	                                  {==}
1019	            case False{}:
1020	              match e:
1021	                case True{}:
1022	                  match p:
1023	                    case True{}:
1024	                      match q:
1025	                        case True{}:
1026	                          match r:
1027	                            case True{}:
1028	                              match z:
1029	                                case True{}:
1030	                                  {==}
1031	                                case False{}:
1032	                                  {==}
1033	                            case False{}:
1034	                              match z:
1035	                                case True{}:
1036	                                  {==}
1037	                                case False{}:
1038	                                  {==}
1039	                        case False{}:
1040	                          match r:
1041	                            case True{}:
1042	                              match z:
1043	                                case True{}:
1044	                                  {==}
1045	                                case False{}:
1046	                                  {==}
1047	                            case False{}:
1048	                              match z:
1049	                                case True{}:
1050	                                  {==}
1051	                                case False{}:
1052	                                  {==}
1053	                    case False{}:
1054	                      match q:
1055	                        case True{}:
1056	                          match r:
1057	                            case True{}:
1058	                              match z:
1059	                                case True{}:
1060	                                  {==}
1061	                                case False{}:
1062	                                  {==}
1063	                            case False{}:
1064	                              match z:
1065	                                case True{}:
1066	                                  {==}
1067	                                case False{}:
1068	                                  {==}
1069	                        case False{}:
1070	                          match r:
1071	                            case True{}:
1072	                              match z:
1073	                                case True{}:
1074	                                  {==}
1075	                                case False{}:
1076	                                  {==}
1077	                            case False{}:
1078	                              match z:
1079	                                case True{}:
1080	                                  {==}
1081	                                case False{}:
1082	                                  {==}
1083	                case False{}:
1084	                  match p:
1085	                    case True{}:
1086	                      match q:
1087	                        case True{}:
1088	                          match r:
1089	                            case True{}:
1090	                              match z:
1091	                                case True{}:
1092	                                  {==}
1093	                                case False{}:
1094	                                  {==}
1095	                            case False{}:
1096	                              match z:
1097	                                case True{}:
1098	                                  {==}
1099	                                case False{}:
1100	                                  {==}
1101	                        case False{}:
1102	                          match r:
1103	                            case True{}:
1104	                              match z:
1105	                                case True{}:
1106	                                  {==}
1107	                                case False{}:
1108	                                  {==}
1109	                            case False{}:
1110	                              match z:
1111	                                case True{}:
1112	                                  {==}
1113	                                case False{}:
1114	                                  {==}
1115	                    case False{}:
1116	                      match q:
1117	                        case True{}:
1118	                          match r:
1119	                            case True{}:
1120	                              match z:
1121	                                case True{}:
1122	                                  {==}
1123	                                case False{}:
1124	                                  {==}
1125	                            case False{}:
1126	                              match z:
1127	                                case True{}:
1128	                                  {==}
1129	                                case False{}:
1130	                                  {==}
1131	                        case False{}:
1132	                          match r:
1133	                            case True{}:
1134	                              match z:
1135	                                case True{}:
1136	                                  {==}
1137	                                case False{}:
1138	                                  {==}
1139	                            case False{}:
1140	                              match z:
1141	                                case True{}:
1142	                                  {==}
1143	                                case False{}:
1144	                                  {==}
1145	        case False{}:
1146	          match ain:
1147	            case True{}:
1148	              match e:
1149	                case True{}:
1150	                  match p:
1151	                    case True{}:
1152	                      match q:
1153	                        case True{}:
1154	                          match r:
1155	                            case True{}:
1156	                              match z:
1157	                                case True{}:
1158	                                  {==}
1159	                                case False{}:
1160	                                  {==}
1161	                            case False{}:
1162	                              match z:
1163	                                case True{}:
1164	                                  {==}
1165	                                case False{}:
1166	                                  {==}
1167	                        case False{}:
1168	                          match r:
1169	                            case True{}:
1170	                              match z:
1171	                                case True{}:
1172	                                  {==}
1173	                                case False{}:
1174	                                  {==}
1175	                            case False{}:
1176	                              match z:
1177	                                case True{}:
1178	                                  {==}
1179	                                case False{}:
1180	                                  {==}
1181	                    case False{}:
1182	                      match q:
1183	                        case True{}:
1184	                          match r:
1185	                            case True{}:
1186	                              match z:
1187	                                case True{}:
1188	                                  {==}
1189	                                case False{}:
1190	                                  {==}
1191	                            case False{}:
1192	                              match z:
1193	                                case True{}:
1194	                                  {==}
1195	                                case False{}:
1196	                                  {==}
1197	                        case False{}:
1198	                          match r:
1199	                            case True{}:
1200	                              match z:
1201	                                case True{}:
1202	                                  {==}
1203	                                case False{}:
1204	                                  {==}
1205	                            case False{}:
1206	                              match z:
1207	                                case True{}:
1208	                                  {==}
1209	                                case False{}:
1210	                                  {==}
1211	                case False{}:
1212	                  match p:
1213	                    case True{}:
1214	                      match q:
1215	                        case True{}:
1216	                          match r:
1217	                            case True{}:
1218	                              match z:
1219	                                case True{}:
1220	                                  {==}
1221	                                case False{}:
1222	                                  {==}
1223	                            case False{}:
1224	                              match z:
1225	                                case True{}:
1226	                                  {==}
1227	                                case False{}:
1228	                                  {==}
1229	                        case False{}:
1230	                          match r:
1231	                            case True{}:
1232	                              match z:
1233	                                case True{}:
1234	                                  {==}
1235	                                case False{}:
1236	                                  {==}
1237	                            case False{}:
1238	                              match z:
1239	                                case True{}:
1240	                                  {==}
1241	                                case False{}:
1242	                                  {==}
1243	                    case False{}:
1244	                      match q:
1245	                        case True{}:
1246	                          match r:
1247	                            case True{}:
1248	                              match z:
1249	                                case True{}:
1250	                                  {==}
1251	                                case False{}:
1252	                                  {==}
1253	                            case False{}:
1254	                              match z:
1255	                                case True{}:
1256	                                  {==}
1257	                                case False{}:
1258	                                  {==}
1259	                        case False{}:
1260	                          match r:
1261	                            case True{}:
1262	                              match z:
1263	                                case True{}:
1264	                                  {==}
1265	                                case False{}:
1266	                                  {==}
1267	                            case False{}:
1268	                              match z:
1269	                                case True{}:
1270	                                  {==}
1271	                                case False{}:
1272	                                  {==}
1273	            case False{}:
1274	              match e:
1275	                case True{}:
1276	                  match p:
1277	                    case True{}:
1278	                      match q:
1279	                        case True{}:
1280	                          match r:
1281	                            case True{}:
1282	                              match z:
1283	                                case True{}:
1284	                                  {==}
1285	                                case False{}:
1286	                                  {==}
1287	                            case False{}:
1288	                              match z:
1289	                                case True{}:
1290	                                  {==}
1291	                                case False{}:
1292	                                  {==}
1293	                        case False{}:
1294	                          match r:
1295	                            case True{}:
1296	                              match z:
1297	                                case True{}:
1298	                                  {==}
1299	                                case False{}:
1300	                                  {==}
1301	                            case False{}:
1302	                              match z:
1303	                                case True{}:
1304	                                  {==}
1305	                                case False{}:
1306	                                  {==}
1307	                    case False{}:
1308	                      match q:
1309	                        case True{}:
1310	                          match r:
1311	                            case True{}:
1312	                              match z:
1313	                                case True{}:
1314	                                  {==}
1315	                                case False{}:
1316	                                  {==}
1317	                            case False{}:
1318	                              match z:
1319	                                case True{}:
1320	                                  {==}
1321	                                case False{}:
1322	                                  {==}
1323	                        case False{}:
1324	                          match r:
1325	                            case True{}:
1326	                              match z:
1327	                                case True{}:
1328	                                  {==}
1329	                                case False{}:
1330	                                  {==}
1331	                            case False{}:
1332	                              match z:
1333	                                case True{}:
1334	                                  {==}
1335	                                case False{}:
1336	                                  {==}
1337	                case False{}:
1338	                  match p:
1339	                    case True{}:
1340	                      match q:
1341	                        case True{}:
1342	                          match r:
1343	                            case True{}:
1344	                              match z:
1345	                                case True{}:
1346	                                  {==}
1347	                                case False{}:
1348	                                  {==}
1349	                            case False{}:
1350	                              match z:
1351	                                case True{}:
1352	                                  {==}
1353	                                case False{}:
1354	                                  {==}
1355	                        case False{}:
1356	                          match r:
1357	                            case True{}:
1358	                              match z:
1359	                                case True{}:
1360	                                  {==}
1361	                                case False{}:
1362	                                  {==}
1363	                            case False{}:
1364	                              match z:
1365	                                case True{}:
1366	                                  {==}
1367	                                case False{}:
1368	                                  {==}
1369	                    case False{}:
1370	                      match q:
1371	                        case True{}:
1372	                          match r:
1373	                            case True{}:
1374	                              match z:
1375	                                case True{}:
1376	                                  {==}
1377	                                case False{}:
1378	                                  {==}
1379	                            case False{}:
1380	                              match z:
1381	                                case True{}:
1382	                                  {==}
1383	                                case False{}:
1384	                                  {==}
1385	                        case False{}:
1386	                          match r:
1387	                            case True{}:
1388	                              match z:
1389	                                case True{}:
1390	                                  {==}
1391	                                case False{}:
1392	                                  {==}
1393	                            case False{}:
1394	                              match z:
1395	                                case True{}:
1396	                                  {==}
1397	                                case False{}:
1398	                                  {==}
1399	
1400	def nfa.taut_star(+hb: Bool, +cin: Bool, +ain: Bool, +e: Bool, +p: Bool, +q: Bool, +r: Bool, +z: Bool) -> {Bool.or(Bool.and(Bool.or(Bool.and(Bool.or(hb, cin), e), ain), p), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), False{}), q), Bool.or(Bool.and(Bool.and(Bool.or(hb, cin), True{}), r), z))) == Bool.or(Bool.and(ain, p), Bool.or(Bool.and(cin, Bool.or(r, Bool.and(e, p))), Bool.or(Bool.and(hb, Bool.or(r, Bool.and(e, p))), z))) : Bool}:
1401	  match hb:
1402	    case True{}:
1403	      match cin:
1404	        case True{}:
1405	          match ain:
1406	            case True{}:
1407	              match e:
1408	                case True{}:
1409	                  match p:
1410	                    case True{}:
1411	                      match q:
1412	                        case True{}:
1413	                          match r:
1414	                            case True{}:
1415	                              match z:
1416	                                case True{}:
1417	                                  {==}
1418	                                case False{}:
1419	                                  {==}
1420	                            case False{}:
1421	                              match z:
1422	                                case True{}:
1423	                                  {==}
1424	                                case False{}:
1425	                                  {==}
1426	                        case False{}:
1427	                          match r:
1428	                            case True{}:
1429	                              match z:
1430	                                case True{}:
1431	                                  {==}
1432	                                case False{}:
1433	                                  {==}
1434	                            case False{}:
1435	                              match z:
1436	                                case True{}:
1437	                                  {==}
1438	                                case False{}:
1439	                                  {==}
1440	                    case False{}:
1441	                      match q:
1442	                        case True{}:
1443	                          match r:
1444	                            case True{}:
1445	                              match z:
1446	                                case True{}:
1447	                                  {==}
1448	                                case False{}:
1449	                                  {==}
1450	                            case False{}:
1451	                              match z:
1452	                                case True{}:
1453	                                  {==}
1454	                                case False{}:
1455	                                  {==}
1456	                        case False{}:
1457	                          match r:
1458	                            case True{}:
1459	                              match z:
1460	                                case True{}:
1461	                                  {==}
1462	                                case False{}:
1463	                                  {==}
1464	                            case False{}:
1465	                              match z:
1466	                                case True{}:
1467	                                  {==}
1468	                                case False{}:
1469	                                  {==}
1470	                case False{}:
1471	                  match p:
1472	                    case True{}:
1473	                      match q:
1474	                        case True{}:
1475	                          match r:
1476	                            case True{}:
1477	                              match z:
1478	                                case True{}:
1479	                                  {==}
1480	                                case False{}:
1481	                                  {==}
1482	                            case False{}:
1483	                              match z:
1484	                                case True{}:
1485	                                  {==}
1486	                                case False{}:
1487	                                  {==}
1488	                        case False{}:
1489	                          match r:
1490	                            case True{}:
1491	                              match z:
1492	                                case True{}:
1493	                                  {==}
1494	                                case False{}:
1495	                                  {==}
1496	                            case False{}:
1497	                              match z:
1498	                                case True{}:
1499	                                  {==}
1500	                                case False{}:
1501	                                  {==}
1502	                    case False{}:
1503	                      match q:
1504	                        case True{}:
1505	                          match r:
1506	                            case True{}:
1507	                              match z:
1508	                                case True{}:
1509	                                  {==}
1510	                                case False{}:
1511	                                  {==}
1512	                            case False{}:
1513	                              match z:
1514	                                case True{}:
1515	                                  {==}
1516	                                case False{}:
1517	                                  {==}
1518	                        case False{}:
1519	                          match r:
1520	                            case True{}:
1521	                              match z:
1522	                                case True{}:
1523	                                  {==}
1524	                                case False{}:
1525	                                  {==}
1526	                            case False{}:
1527	                              match z:
1528	                                case True{}:
1529	                                  {==}
1530	                                case False{}:
1531	                                  {==}
1532	            case False{}:
1533	              match e:
1534	                case True{}:
1535	                  match p:
1536	                    case True{}:
1537	                      match q:
1538	                        case True{}:
1539	                          match r:
1540	                            case True{}:
1541	                              match z:
1542	                                case True{}:
1543	                                  {==}
1544	                                case False{}:
1545	                                  {==}
1546	                            case False{}:
1547	                              match z:
1548	                                case True{}:
1549	                                  {==}
1550	                                case False{}:
1551	                                  {==}
1552	                        case False{}:
1553	                          match r:
1554	                            case True{}:
1555	                              match z:
1556	                                case True{}:
1557	                                  {==}
1558	                                case False{}:
1559	                                  {==}
1560	                            case False{}:
1561	                              match z:
1562	                                case True{}:
1563	                                  {==}
1564	                                case False{}:
1565	                                  {==}
1566	                    case False{}:
1567	                      match q:
1568	                        case True{}:
1569	                          match r:
1570	                            case True{}:
1571	                              match z:
1572	                                case True{}:
1573	                                  {==}
1574	                                case False{}:
1575	                                  {==}
1576	                            case False{}:
1577	                              match z:
1578	                                case True{}:
1579	                                  {==}
1580	                                case False{}:
1581	                                  {==}
1582	                        case False{}:
1583	                          match r:
1584	                            case True{}:
1585	                              match z:
1586	                                case True{}:
1587	                                  {==}
1588	                                case False{}:
1589	                                  {==}
1590	                            case False{}:
1591	                              match z:
1592	                                case True{}:
1593	                                  {==}
1594	                                case False{}:
1595	                                  {==}
1596	                case False{}:
1597	                  match p:
1598	                    case True{}:
1599	                      match q:
1600	                        case True{}:
1601	                          match r:
1602	                            case True{}:
1603	                              match z:
1604	                                case True{}:
1605	                                  {==}
1606	                                case False{}:
1607	                                  {==}
1608	                            case False{}:
1609	                              match z:
1610	                                case True{}:
1611	                                  {==}
1612	                                case False{}:
1613	                                  {==}
1614	                        case False{}:
1615	                          match r:
1616	                            case True{}:
1617	                              match z:
1618	                                case True{}:
1619	                                  {==}
1620	                                case False{}:
1621	                                  {==}
1622	                            case False{}:
1623	                              match z:
1624	                                case True{}:
1625	                                  {==}
1626	                                case False{}:
1627	                                  {==}
1628	                    case False{}:
1629	                      match q:
1630	                        case True{}:
1631	                          match r:
1632	                            case True{}:
1633	                              match z:
1634	                                case True{}:
1635	                                  {==}
1636	                                case False{}:
1637	                                  {==}
1638	                            case False{}:
1639	                              match z:
1640	                                case True{}:
1641	                                  {==}
1642	                                case False{}:
1643	                                  {==}
1644	                        case False{}:
1645	                          match r:
1646	                            case True{}:
1647	                              match z:
1648	                                case True{}:
1649	                                  {==}
1650	                                case False{}:
1651	                                  {==}
1652	                            case False{}:
1653	                              match z:
1654	                                case True{}:
1655	                                  {==}
1656	                                case False{}:
1657	                                  {==}
1658	        case False{}:
1659	          match ain:
1660	            case True{}:
1661	              match e:
1662	                case True{}:
1663	                  match p:
1664	                    case True{}:
1665	                      match q:
1666	                        case True{}:
1667	                          match r:
1668	                            case True{}:
1669	                              match z:
1670	                                case True{}:
1671	                                  {==}
1672	                                case False{}:
1673	                                  {==}
1674	                            case False{}:
1675	                              match z:
1676	                                case True{}:
1677	                                  {==}
1678	                                case False{}:
1679	                                  {==}
1680	                        case False{}:
1681	                          match r:
1682	                            case True{}:
1683	                              match z:
1684	                                case True{}:
1685	                                  {==}
1686	                                case False{}:
1687	                                  {==}
1688	                            case False{}:
1689	                              match z:
1690	                                case True{}:
1691	                                  {==}
1692	                                case False{}:
1693	                                  {==}
1694	                    case False{}:
1695	                      match q:
1696	                        case True{}:
1697	                          match r:
1698	                            case True{}:
1699	                              match z:
1700	                                case True{}:
1701	                                  {==}
1702	                                case False{}:
1703	                                  {==}
1704	                            case False{}:
1705	                              match z:
1706	                                case True{}:
1707	                                  {==}
1708	                                case False{}:
1709	                                  {==}
1710	                        case False{}:
1711	                          match r:
1712	                            case True{}:
1713	                              match z:
1714	                                case True{}:
1715	                                  {==}
1716	                                case False{}:
1717	                                  {==}
1718	                            case False{}:
1719	                              match z:
1720	                                case True{}:
1721	                                  {==}
1722	                                case False{}:
1723	                                  {==}
1724	                case False{}:
1725	                  match p:
1726	                    case True{}:
1727	                      match q:
1728	                        case True{}:
1729	                          match r:
1730	                            case True{}:
1731	                              match z:
1732	                                case True{}:
1733	                                  {==}
1734	                                case False{}:
1735	                                  {==}
1736	                            case False{}:
1737	                              match z:
1738	                                case True{}:
1739	                                  {==}
1740	                                case False{}:
1741	                                  {==}
1742	                        case False{}:
1743	                          match r:
1744	                            case True{}:
1745	                              match z:
1746	                                case True{}:
1747	                                  {==}
1748	                                case False{}:
1749	                                  {==}
1750	                            case False{}:
1751	                              match z:
1752	                                case True{}:
1753	                                  {==}
1754	                                case False{}:
1755	                                  {==}
1756	                    case False{}:
1757	                      match q:
1758	                        case True{}:
1759	                          match r:
1760	                            case True{}:
1761	                              match z:
1762	                                case True{}:
1763	                                  {==}
1764	                                case False{}:
1765	                                  {==}
1766	                            case False{}:
1767	                              match z:
1768	                                case True{}:
1769	                                  {==}
1770	                                case False{}:
1771	                                  {==}
1772	                        case False{}:
1773	                          match r:
1774	                            case True{}:
1775	                              match z:
1776	                                case True{}:
1777	                                  {==}
1778	                                case False{}:
1779	                                  {==}
1780	                            case False{}:
1781	                              match z:
1782	                                case True{}:
1783	                                  {==}
1784	                                case False{}:
1785	                                  {==}
1786	            case False{}:
1787	              match e:
1788	                case True{}:
1789	                  match p:
1790	                    case True{}:
1791	                      match q:
1792	                        case True{}:
1793	                          match r:
1794	                            case True{}:
1795	                              match z:
1796	                                case True{}:
1797	                                  {==}
1798	                                case False{}:
1799	                                  {==}
1800	                            case False{}:
1801	                              match z:
1802	                                case True{}:
1803	                                  {==}
1804	                                case False{}:
1805	                                  {==}
1806	                        case False{}:
1807	                          match r:
1808	                            case True{}:
1809	                              match z:
1810	                                case True{}:
1811	                                  {==}
1812	                                case False{}:
1813	                                  {==}
1814	                            case False{}:
1815	                              match z:
1816	                                case True{}:
1817	                                  {==}
1818	                                case False{}:
1819	                                  {==}
1820	                    case False{}:
1821	                      match q:
1822	                        case True{}:
1823	                          match r:
1824	                            case True{}:
1825	                              match z:
1826	                                case True{}:
1827	                                  {==}
1828	                                case False{}:
1829	                                  {==}
1830	                            case False{}:
1831	                              match z:
1832	                                case True{}:
1833	                                  {==}
1834	                                case False{}:
1835	                                  {==}
1836	                        case False{}:
1837	                          match r:
1838	                            case True{}:
1839	                              match z:
1840	                                case True{}:
1841	                                  {==}
1842	                                case False{}:
1843	                                  {==}
1844	                            case False{}:
1845	                              match z:
1846	                                case True{}:
1847	                                  {==}
1848	                                case False{}:
1849	                                  {==}
1850	                case False{}:
1851	                  match p:
1852	                    case True{}:
1853	                      match q:
1854	                        case True{}:
1855	                          match r:
1856	                            case True{}:
1857	                              match z:
1858	                                case True{}:
1859	                                  {==}
1860	                                case False{}:
1861	                                  {==}
1862	                            case False{}:
1863	                              match z:
1864	                                case True{}:
1865	                                  {==}
1866	                                case False{}:
1867	                                  {==}
1868	                        case False{}:
1869	                          match r:
1870	                            case True{}:
1871	                              match z:
1872	                                case True{}:
1873	                                  {==}
1874	                                case False{}:
1875	                                  {==}
1876	                            case False{}:
1877	                              match z:
1878	                                case True{}:
1879	                                  {==}
1880	                                case False{}:
1881	                                  {==}
1882	                    case False{}:
1883	                      match q:
1884	                        case True{}:
1885	                          match r:
1886	                            case True{}:
1887	                              match z:
1888	                                case True{}:
1889	                                  {==}
1890	                                case False{}:
1891	                                  {==}
1892	                            case False{}:
1893	                              match z:
1894	                                case True{}:
1895	                                  {==}
1896	                                case False{}:
1897	                                  {==}
1898	                        case False{}:
1899	                          match r:
1900	                            case True{}:
1901	                              match z:
1902	                                case True{}:
1903	                                  {==}
1904	                                case False{}:
1905	                                  {==}
1906	                            case False{}:
1907	                              match z:
1908	                                case True{}:
1909	                                  {==}
1910	                                case False{}:
1911	                                  {==}
1912	    case False{}:
1913	      match cin:
1914	        case True{}:
1915	          match ain:
1916	            case True{}:
1917	              match e:
1918	                case True{}:
1919	                  match p:
1920	                    case True{}:
1921	                      match q:
1922	                        case True{}:
1923	                          match r:
1924	                            case True{}:
1925	                              match z:
1926	                                case True{}:
1927	                                  {==}
1928	                                case False{}:
1929	                                  {==}
1930	                            case False{}:
1931	                              match z:
1932	                                case True{}:
1933	                                  {==}
1934	                                case False{}:
1935	                                  {==}
1936	                        case False{}:
1937	                          match r:
1938	                            case True{}:
1939	                              match z:
1940	                                case True{}:
1941	                                  {==}
1942	                                case False{}:
1943	                                  {==}
1944	                            case False{}:
1945	                              match z:
1946	                                case True{}:
1947	                                  {==}
1948	                                case False{}:
1949	                                  {==}
1950	                    case False{}:
1951	                      match q:
1952	                        case True{}:
1953	                          match r:
1954	                            case True{}:
1955	                              match z:
1956	                                case True{}:
1957	                                  {==}
1958	                                case False{}:
1959	                                  {==}
1960	                            case False{}:
1961	                              match z:
1962	                                case True{}:
1963	                                  {==}
1964	                                case False{}:
1965	                                  {==}
1966	                        case False{}:
1967	                          match r:
1968	                            case True{}:
1969	                              match z:
1970	                                case True{}:
1971	                                  {==}
1972	                                case False{}:
1973	                                  {==}
1974	                            case False{}:
1975	                              match z:
1976	                                case True{}:
1977	                                  {==}
1978	                                case False{}:
1979	                                  {==}
1980	                case False{}:
1981	                  match p:
1982	                    case True{}:
1983	                      match q:
1984	                        case True{}:
1985	                          match r:
1986	                            case True{}:
1987	                              match z:
1988	                                case True{}:
1989	                                  {==}
1990	                                case False{}:
1991	                                  {==}
1992	                            case False{}:
1993	                              match z:
1994	                                case True{}:
1995	                                  {==}
1996	                                case False{}:
1997	                                  {==}
1998	                        case False{}:
1999	                          match r:
2000	                            case True{}:
Lines 1-2000 of 3947. More: https://jend.leeeet.dev/read.txt?path=bend-osdev-apparmor@0.1.0.0/PROOF.bend&start_line=2001