Index: /src/ASM/AssemblyProof.ma
===================================================================
--- /src/ASM/AssemblyProof.ma	(revision 1948)
+++ /src/ASM/AssemblyProof.ma	(revision 1952)
@@ -2205,332 +2205,2 @@
   //
 qed.
-
-theorem main_thm:
-  ∀M.
-  ∀M'.
-  ∀cm.
-  ∀ps.
-  ∀sigma.
-  ∀policy.
-    next_internal_pseudo_address_map M cm ps = Some … M' →
-      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
-        status_of_pseudo_status M' … 
-          (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
-  #M #M' * #preamble #instr_list #ps #sigma #policy
-  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
-  @(pose … (program_counter ?? ps)) #ppc #EQppc
-  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
-  @pair_elim #labels #costs #H0 normalize nodelta
-  @pair_elim #assembled #costs' #EQ1 normalize nodelta
-  @pair_elim #pi #newppc #EQ2 normalize nodelta
-  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
-  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
-  whd in match execute_1_pseudo_instruction; normalize nodelta
-  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
-  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
-  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
-  [>EQ2 %]
-  inversion pi
-  [2,3: (* Comment, Cost *)
-    #ARG #EQ
-    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
-    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
-    whd in match (execute_1_pseudo_instruction0 ?????);
-    %{0} @split_eq_status
-   CSC: STOP HERE, was // but requires -H0 -H3 because of \fst and \pi1
-   ⇒ CHANGE TO AVOID \fst and \pi1! (*
-   try (<H3 -H0 -H3 //)
-   [ <add_zero in H3; #H3 >H3 -H0 -H3 //
-   | -H0 -H3 /demod/*)
-  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
-   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
-       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
-         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
-         @pair_elim' * #instr #newppc' #ticks #EQ4       
-         * * #H2a #H2b whd in ⊢ (% → ?) #H2
-         >H2b >(eq_instruction_to_eq … H2a)
-         #EQ %[@1]
-         <MAP >(eq_bv_eq … H2) >EQ
-         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
-         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
-         whd in ⊢ (??%?)
-         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
-         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
-  |6: (* Mov *) #arg1 #arg2
-       #H1 #H2 #EQ %[@1]
-       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-       change in ⊢ (? → ??%?) with (execute_1_0 ??)
-       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-       >H2b >(eq_instruction_to_eq … H2a)
-       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
-       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
-       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
-       normalize nodelta;
-       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
-       #result #flags
-       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
-  |5: (* Call *) #label #MAP
-      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
-      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
-       [ (* short *) #abs @⊥ destruct (abs)
-       |3: (* long *) #H1 #H2 #EQ %[@1]
-           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-           change in ⊢ (? → ??%?) with (execute_1_0 ??)
-           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           whd in ⊢ (???% → ??%?);
-           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
-           >(eq_bv_eq … H2c)
-           change with
-            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
-                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
-           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
-           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
-           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
-           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
-           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
-           @split_eq_status;
-            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
-              >code_memory_write_at_stack_pointer %
-            | >set_program_counter_set_low_internal_ram
-              >set_clock_set_low_internal_ram
-              @low_internal_ram_write_at_stack_pointer
-               [ >EQ0 @pol | % | %
-               | @(pair_destruct_2 … EQ1)
-               | @(pair_destruct_2 … EQ2)
-               | >(pair_destruct_1 ????? EQpc)
-                 >(pair_destruct_2 ????? EQpc)
-                 @split_elim #x #y #H <H -x y H;
-                 >(pair_destruct_1 ????? EQppc)
-                 >(pair_destruct_2 ????? EQppc)
-                 @split_elim #x #y #H <H -x y H;
-                 >EQ0 % ]
-            | >set_low_internal_ram_set_high_internal_ram
-              >set_program_counter_set_high_internal_ram
-              >set_clock_set_high_internal_ram
-              @high_internal_ram_write_at_stack_pointer
-               [ >EQ0 @pol | % | %
-               | @(pair_destruct_2 … EQ1)
-               | @(pair_destruct_2 … EQ2)
-               | >(pair_destruct_1 ????? EQpc)
-                 >(pair_destruct_2 ????? EQpc)
-                 @split_elim #x #y #H <H -x y H;
-                 >(pair_destruct_1 ????? EQppc)
-                 >(pair_destruct_2 ????? EQppc)
-                 @split_elim #x #y #H <H -x y H;
-                 >EQ0 % ]            
-            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
-              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
-              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
-              >external_ram_write_at_stack_pointer %
-            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
-              >EQ0 % 
-            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
-              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
-              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
-              >special_function_registers_8051_write_at_stack_pointer %
-            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
-              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
-              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
-              >special_function_registers_8052_write_at_stack_pointer %
-            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
-              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
-              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
-              >p1_latch_write_at_stack_pointer %
-            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
-              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
-              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
-              >p3_latch_write_at_stack_pointer %
-            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
-              >clock_write_at_stack_pointer whd in ⊢ (???%)
-              >clock_write_at_stack_pointer whd in ⊢ (???%)
-              >clock_write_at_stack_pointer %]
-       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
-         @pair_elim' #fst_5_addr #rest_addr #EQ1
-         @pair_elim' #fst_5_pc #rest_pc #EQ2
-         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
-         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
-         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
-         change in ⊢ (? →??%?) with (execute_1_0 ??)
-         @pair_elim' * #instr #newppc' #ticks #EQn
-          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
-          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
-          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
-          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
-          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
-          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
-          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
-          >get_8051_sfr_set_8051_sfr
-          
-          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
-           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
-           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
-           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
-           generalize in match (refl … (split bool 4 4 pc_bu))
-           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
-           generalize in match (refl … (split bool 3 8 rest_addr))
-           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
-           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
-           generalize in match
-            (refl …
-             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
-             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
-           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
-           @split_eq_status try %
-            [ change with (? = sigma ? (address_of_word_labels ps label))
-              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
-            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
-              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
-  |4: (* Jmp *) #label #MAP
-      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
-      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
-       [3: (* long *) #H1 #H2 #EQ %[@1]
-           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-           change in ⊢ (? → ??%?) with (execute_1_0 ??)
-           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
-           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
-       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
-           generalize in match
-            (refl ?
-             (sub_16_with_carry
-              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
-              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
-              false))
-           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
-           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
-           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
-           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
-           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-           change in ⊢ (? → ??%?) with (execute_1_0 ??)
-           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           whd in ⊢ (???% → ?);
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
-           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
-           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
-           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
-           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
-           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
-       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
-         generalize in match
-          (refl …
-            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
-         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
-         generalize in match
-          (refl …
-            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
-         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
-         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
-         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
-         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
-         change in ⊢ (? →??%?) with (execute_1_0 ??)
-           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-           >H2b >(eq_instruction_to_eq … H2a)
-           generalize in match EQ; -EQ;
-           whd in ⊢ (???% → ?);
-           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
-           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
-           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
-           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
-           generalize in match (refl … (split bool 4 4 pc_bu))
-           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
-           generalize in match (refl … (split bool 3 8 rest_addr))
-           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
-           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
-           generalize in match
-            (refl …
-             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
-             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
-           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7    
-           @split_eq_status try %
-            [ change with (? = sigma ?? (address_of_word_labels ps label))
-              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
-            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
-              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
-  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
-    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
-       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-       change in ⊢ (? → ??%?) with (execute_1_0 ??)
-       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-       >H2b >(eq_instruction_to_eq … H2a)
-       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
-       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
-       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
-       normalize nodelta; #MAP;
-       [1: change in ⊢ (? → %) with
-        ((let 〈result,flags〉 ≝
-          add_8_with_carry
-           (get_arg_8 ? ps false ACC_A)
-           (get_arg_8 ?
-             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
-             false (DIRECT ARG2))
-           ? in ?) = ?)
-        [2,3: %]
-        change in ⊢ (???% → ?) with
-         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
-        >get_arg_8_set_clock
-       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
-         [2,4: #abs @⊥ normalize in abs; destruct (abs)
-         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
-       [ change in ⊢ (? → %) with
-        ((let 〈result,flags〉 ≝
-          add_8_with_carry
-           (get_arg_8 ? ps false ACC_A)
-           (get_arg_8 ?
-             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
-             false (DIRECT ARG2))
-           ? in ?) = ?)
-          >get_arg_8_set_low_internal_ram
-       
-        cases (add_8_with_carry ???)
-         
-        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
-       #result #flags
-       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
-    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
-       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
-       change in ⊢ (? → ??%?) with (execute_1_0 ??)
-       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
-       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
-       >H2b >(eq_instruction_to_eq … H2a)
-       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
-       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
-       [1,2,3,4: cases (half_add ???) #carry #result
-       | cases (half_add ???) #carry #bl normalize nodelta;
-         cases (full_add ????) #carry' #bu normalize nodelta ]
-        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
-        [5: %
-        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
-      (set_program_counter pseudo_assembly_program ps newppc)
-      (\fst  (ticks_of0 〈preamble,instr_list〉
-                   (program_counter pseudo_assembly_program ps)
-                   (Instruction (INC Identifier (DIRECT ARG))))
-       +clock pseudo_assembly_program
-        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
-        [2,3: // ]
-            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
-            whd in ⊢ (??%%)
-            cases (split bool 4 4 ARG)
-            #nu' #nl'
-            normalize nodelta
-            cases (split bool 1 3 nu')
-            #bit_1' #ignore'
-            normalize nodelta
-            cases (get_index_v bool 4 nu' ? ?)
-            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
-            |
-            ]
-cases daemon (* EASY CASES TO BE COMPLETED *)
-qed.
Index: /src/ASM/AssemblyProofSplit.ma
===================================================================
--- /src/ASM/AssemblyProofSplit.ma	(revision 1952)
+++ /src/ASM/AssemblyProofSplit.ma	(revision 1952)
@@ -0,0 +1,333 @@
+include "ASM/AssemblyProof.ma".
+include alias "arithmetics/nat.ma".
+include alias "basics/logic.ma".
+
+theorem main_thm:
+  ∀M.
+  ∀M'.
+  ∀cm.
+  ∀ps.
+  ∀sigma.
+  ∀policy.
+    next_internal_pseudo_address_map M cm ps = Some … M' →
+      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
+        status_of_pseudo_status M' … 
+          (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
+  #M #M' * #preamble #instr_list #ps #sigma #policy
+  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
+  @(pose … (program_counter ?? ps)) #ppc #EQppc
+  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
+  @pair_elim #labels #costs #H0 normalize nodelta
+  @pair_elim #assembled #costs' #EQ1 normalize nodelta
+  @pair_elim #pi #newppc #EQ2 normalize nodelta
+  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
+  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
+  whd in match execute_1_pseudo_instruction; normalize nodelta
+  whd in match ticks_of; normalize nodelta <EQppc #H2 >EQ2 normalize nodelta
+  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
+  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
+  [>EQ2 %]
+  inversion pi
+  [2,3: (* Comment, Cost *)
+    #ARG #EQ
+    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
+    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
+    whd in match (execute_1_pseudo_instruction0 ?????);
+    %{0} @split_eq_statusCSC: this works :-) (lapply H3 -H3 letin sixteen ≝ 16 #H3 // /demod/)
+   CSC: STOP HERE, was // but requires -H3 because of 16!
+   ⇒ CHANGE TO AVOID \fst and \pi1! (*
+   try (<H3 -H0 -H3 //)
+   [ <add_zero in H3; #H3 >H3 -H0 -H3 //
+   | -H0 -H3 /demod/*)
+  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?)
+   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
+       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
+         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
+         @pair_elim' * #instr #newppc' #ticks #EQ4       
+         * * #H2a #H2b whd in ⊢ (% → ?) #H2
+         >H2b >(eq_instruction_to_eq … H2a)
+         #EQ %[@1]
+         <MAP >(eq_bv_eq … H2) >EQ
+         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
+         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
+         whd in ⊢ (??%?)
+         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
+         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
+  |6: (* Mov *) #arg1 #arg2
+       #H1 #H2 #EQ %[@1]
+       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+       change in ⊢ (? → ??%?) with (execute_1_0 ??)
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+       >H2b >(eq_instruction_to_eq … H2a)
+       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
+       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
+       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
+       normalize nodelta;
+       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
+       #result #flags
+       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
+  |5: (* Call *) #label #MAP
+      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
+      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
+       [ (* short *) #abs @⊥ destruct (abs)
+       |3: (* long *) #H1 #H2 #EQ %[@1]
+           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+           change in ⊢ (? → ??%?) with (execute_1_0 ??)
+           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+           >H2b >(eq_instruction_to_eq … H2a)
+           generalize in match EQ; -EQ;
+           whd in ⊢ (???% → ??%?);
+           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
+           >(eq_bv_eq … H2c)
+           change with
+            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
+                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
+           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
+           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
+           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
+           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
+           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
+           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
+           @split_eq_status;
+            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
+              >code_memory_write_at_stack_pointer %
+            | >set_program_counter_set_low_internal_ram
+              >set_clock_set_low_internal_ram
+              @low_internal_ram_write_at_stack_pointer
+               [ >EQ0 @pol | % | %
+               | @(pair_destruct_2 … EQ1)
+               | @(pair_destruct_2 … EQ2)
+               | >(pair_destruct_1 ????? EQpc)
+                 >(pair_destruct_2 ????? EQpc)
+                 @split_elim #x #y #H <H -x y H;
+                 >(pair_destruct_1 ????? EQppc)
+                 >(pair_destruct_2 ????? EQppc)
+                 @split_elim #x #y #H <H -x y H;
+                 >EQ0 % ]
+            | >set_low_internal_ram_set_high_internal_ram
+              >set_program_counter_set_high_internal_ram
+              >set_clock_set_high_internal_ram
+              @high_internal_ram_write_at_stack_pointer
+               [ >EQ0 @pol | % | %
+               | @(pair_destruct_2 … EQ1)
+               | @(pair_destruct_2 … EQ2)
+               | >(pair_destruct_1 ????? EQpc)
+                 >(pair_destruct_2 ????? EQpc)
+                 @split_elim #x #y #H <H -x y H;
+                 >(pair_destruct_1 ????? EQppc)
+                 >(pair_destruct_2 ????? EQppc)
+                 @split_elim #x #y #H <H -x y H;
+                 >EQ0 % ]            
+            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
+              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
+              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
+              >external_ram_write_at_stack_pointer %
+            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
+              >EQ0 % 
+            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
+              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8051_write_at_stack_pointer %
+            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
+              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
+              >special_function_registers_8052_write_at_stack_pointer %
+            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
+              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p1_latch_write_at_stack_pointer %
+            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
+              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
+              >p3_latch_write_at_stack_pointer %
+            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
+              >clock_write_at_stack_pointer whd in ⊢ (???%)
+              >clock_write_at_stack_pointer whd in ⊢ (???%)
+              >clock_write_at_stack_pointer %]
+       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+         @pair_elim' #fst_5_addr #rest_addr #EQ1
+         @pair_elim' #fst_5_pc #rest_pc #EQ2
+         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
+         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
+         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
+         change in ⊢ (? →??%?) with (execute_1_0 ??)
+         @pair_elim' * #instr #newppc' #ticks #EQn
+          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
+          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
+          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
+          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
+          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
+          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
+          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
+          >get_8051_sfr_set_8051_sfr
+          
+          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
+           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
+           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
+           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
+           generalize in match (refl … (split bool 4 4 pc_bu))
+           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
+           generalize in match (refl … (split bool 3 8 rest_addr))
+           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
+           generalize in match
+            (refl …
+             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
+             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
+           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
+           @split_eq_status try %
+            [ change with (? = sigma ? (address_of_word_labels ps label))
+              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
+              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
+  |4: (* Jmp *) #label #MAP
+      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
+      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
+       [3: (* long *) #H1 #H2 #EQ %[@1]
+           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+           change in ⊢ (? → ??%?) with (execute_1_0 ??)
+           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+           >H2b >(eq_instruction_to_eq … H2a)
+           generalize in match EQ; -EQ;
+           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
+           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
+       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+           generalize in match
+            (refl ?
+             (sub_16_with_carry
+              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
+              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
+              false))
+           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
+           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
+           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
+           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
+           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+           change in ⊢ (? → ??%?) with (execute_1_0 ??)
+           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+           >H2b >(eq_instruction_to_eq … H2a)
+           generalize in match EQ; -EQ;
+           whd in ⊢ (???% → ?);
+           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
+           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
+           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
+           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
+           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
+         generalize in match
+          (refl …
+            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
+         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
+         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
+         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
+         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
+         change in ⊢ (? →??%?) with (execute_1_0 ??)
+           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+           >H2b >(eq_instruction_to_eq … H2a)
+           generalize in match EQ; -EQ;
+           whd in ⊢ (???% → ?);
+           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
+           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
+           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
+           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
+           generalize in match (refl … (split bool 4 4 pc_bu))
+           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
+           generalize in match (refl … (split bool 3 8 rest_addr))
+           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
+           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
+           generalize in match
+            (refl …
+             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
+             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
+           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7    
+           @split_eq_status try %
+            [ change with (? = sigma ?? (address_of_word_labels ps label))
+              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
+            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 
+              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
+  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
+    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
+       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+       change in ⊢ (? → ??%?) with (execute_1_0 ??)
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+       >H2b >(eq_instruction_to_eq … H2a)
+       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
+       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
+       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
+       normalize nodelta; #MAP;
+       [1: change in ⊢ (? → %) with
+        ((let 〈result,flags〉 ≝
+          add_8_with_carry
+           (get_arg_8 ? ps false ACC_A)
+           (get_arg_8 ?
+             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
+             false (DIRECT ARG2))
+           ? in ?) = ?)
+        [2,3: %]
+        change in ⊢ (???% → ?) with
+         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
+        >get_arg_8_set_clock
+       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
+         [2,4: #abs @⊥ normalize in abs; destruct (abs)
+         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
+       [ change in ⊢ (? → %) with
+        ((let 〈result,flags〉 ≝
+          add_8_with_carry
+           (get_arg_8 ? ps false ACC_A)
+           (get_arg_8 ?
+             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
+             false (DIRECT ARG2))
+           ? in ?) = ?)
+          >get_arg_8_set_low_internal_ram
+       
+        cases (add_8_with_carry ???)
+         
+        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
+       #result #flags
+       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
+    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
+       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
+       change in ⊢ (? → ??%?) with (execute_1_0 ??)
+       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
+       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
+       >H2b >(eq_instruction_to_eq … H2a)
+       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
+       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
+       [1,2,3,4: cases (half_add ???) #carry #result
+       | cases (half_add ???) #carry #bl normalize nodelta;
+         cases (full_add ????) #carry' #bu normalize nodelta ]
+        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
+        [5: %
+        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
+      (set_program_counter pseudo_assembly_program ps newppc)
+      (\fst  (ticks_of0 〈preamble,instr_list〉
+                   (program_counter pseudo_assembly_program ps)
+                   (Instruction (INC Identifier (DIRECT ARG))))
+       +clock pseudo_assembly_program
+        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
+        [2,3: // ]
+            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
+            whd in ⊢ (??%%)
+            cases (split bool 4 4 ARG)
+            #nu' #nl'
+            normalize nodelta
+            cases (split bool 1 3 nu')
+            #bit_1' #ignore'
+            normalize nodelta
+            cases (get_index_v bool 4 nu' ? ?)
+            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
+            |
+            ]
+cases daemon (* EASY CASES TO BE COMPLETED *)
+qed.