Commit cea760d5 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Remove error message in dk_obj_examples.dk

It should not have been tracked in the first place.
parent 4027595e
......@@ -101,11 +101,6 @@ def trueT : A : type -> BoolT A
(boolT A)
self l_then dk_logic.I).
ERROR line:99 column:14 Error while typing 'self:(dk_obj_examples.BoolT A[0]) => dk_obj.mem_select (dk_obj_examples.boolT A[1]) self[0] dk_obj_examples.l_then dk_logic.I' in context:
A: dk_obj_examples.type.
Expected: ?:(dk_obj.PreObj (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) A[0] (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[0] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[0] dk_type.nil))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil)))) -> dk_obj.PreObj (dk_type.assoc (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] dk_type.nil))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_string.eq_rect (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (l:dk_string.String => dk_domain.position (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons l[0] (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil)))) dk_logic.I (dk_domain.Position_head (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil))))) (dk_type.domain (dk_type.assoc (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] dk_type.nil))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_string.eq_rect (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (l:dk_string.String => dk_domain.position (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons l[0] (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil)))) dk_logic.I (dk_domain.Position_head (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil))))))
Inferred: self:(dk_obj.PreObj (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) A[0] (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[0] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[0] dk_type.nil))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)) (dk_domain.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil)))) -> dk_obj.PreObj (dk_type.assoc (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] dk_type.nil)) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_string.eq_rect (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (l:dk_string.String => dk_domain.position (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons l[0] (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil))) dk_logic.I (dk_domain.Position_head (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil)))) (dk_type.domain (dk_type.assoc (dk_type.cons (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] (dk_type.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) A[1] dk_type.nil)) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_string.eq_rect (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (l:dk_string.String => dk_domain.position (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons l[0] (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil))) dk_logic.I (dk_domain.Position_head (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) (dk_domain.cons (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) (dk_string.cons (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))))) (dk_machine_int.S1 (dk_nat.S (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O)))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S (dk_nat.S dk_nat.O))) (dk_machine_int.S0 (dk_nat.S (dk_nat.S dk_nat.O)) (dk_machine_int.S1 (dk_nat.S dk_nat.O) (dk_machine_int.S1 dk_nat.O dk_machine_int.O))))))) dk_string.nil)))) dk_domain.nil))))).
def falseT : A : type -> BoolT A
:= A : type =>
dk_obj.mem_update
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment