-lemma sem_match_tuple_step:
- accRealize ? match_tuple_step (inr … (inl … (inr … 0)))
- R_match_tuple_step_true R_match_tuple_step_false.
-@(acc_sem_if_app … (sem_test_char ? (λc:STape.¬ is_grid (\fst c))) …
- (sem_seq … sem_compare
- (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c)))
- (sem_nop …)
- (sem_seq … sem_mark_next_tuple
- (sem_if … (sem_test_char ? (λc:STape.is_grid (\fst c)))
- (sem_mark ?) (sem_seq … (sem_move_l …) (sem_init_current …))))))
- (sem_nop ?) …)
-[(* is_grid: termination case *)
- 2:#t1 #t2 #t3 whd in ⊢ (%→?); #H #H1 whd #ls #c #rs #Ht1
- cases (H c ?) [2: >Ht1 %] #Hgrid #Heq %
- [@injective_notb @Hgrid | <Heq @H1]
-|#tapea #tapeout #tapeb whd in ⊢ (%→?); #Htapea
- * #tapec * #Hcompare #Hor
- #ls #c #l1 #l2 #c1 #l3 #l4 #rs #n #Hc #Hl1bars #Hl1marks #Hc1 #Hl3 #eqn
- #eqlen #Htable #Htapea1 cases (Htapea 〈c,true〉 ?) >Htapea1 [2:%]
- #notgridc -Htapea -Htapea1 -tapea #Htapeb
- cases (Hcompare … Htapeb) -Hcompare -Htapeb * #_ #_ #Hcompare
- cases (Hcompare c c1 l1 l3 (l2@[〈bar,false〉]) (l4@〈grid,false〉::rs) eqlen Hl1bars Hl3 Hl1marks … (refl …) Hc ?)
- -Hcompare
- [* #Htemp destruct (Htemp) #Htapec %1 % [%]
- >Htapec in Hor; -Htapec *
- [2: * #t3 * whd in ⊢ (%→?); #H @False_ind
- cases (H … (refl …)) whd in ⊢ ((??%?)→?); #H destruct (H)
- |* #taped * whd in ⊢ (%→?); #Htaped cases (Htaped ? (refl …)) -Htaped *
- #Htaped whd in ⊢ (%→?); #Htapeout >Htapeout >Htaped >associative_append
- %
- ]
- |* #la * #c' * #d' * #lb * #lc * * * #H1 #H2 #H3 #Htapec
- cut (〈c,false〉::l1 ≠ 〈c1,false〉::l3)
- [>H2 >H3 elim la
- [@(not_to_not …H1) normalize #H destruct %
- |#x #tl @not_to_not normalize #H destruct //
- ]
- ] #Hnoteq %2
- cut (is_bit d' = true)
- [cases la in H3;
- [normalize in ⊢ (%→?); #H destruct //
- |#x #tl #H @(Hl3 〈d',false〉)
- normalize in H; destruct @memb_append_l2 @memb_hd
- ]
- ] #Hd'
- >Htapec in Hor; -Htapec *
- [* #taped * whd in ⊢ (%→?); #H @False_ind
- cases (H … (refl …)) >(bit_not_grid ? Hd') #Htemp destruct (Htemp)
- |* #taped * whd in ⊢ (%→?); #H cases (H … (refl …)) -H #_
- #Htaped * #tapee * whd in ⊢ (%→?); #Htapee
- <(associative_append ? lc (〈comma,false〉::l4)) in Htaped; #Htaped
- cases (Htapee … Htaped ???) -Htaped -Htapee
- [* #rs3 * * (* we proceed by cases on rs4 *)
- [(* rs4 is empty *)
- * #d * #b * * * #Heq1 #Hnobars
- whd in ⊢ ((???%)→?); #Htemp destruct (Htemp)
- #Htapee *
- [* #tapef * whd in ⊢ (%→?); >Htapee -Htapee #Htapef
- cases (Htapef … (refl …)) -Htapef #_ #Htapef >Htapef -Htapef
- whd in ⊢ (%→?); #H lapply (H … ???? (refl …)) #Htapeout
- %2 %
- [% [@Hnoteq |@daemon]
- |>Htapeout %
- ]
- |* #tapef * whd in ⊢ (%→?); >Htapee -Htapee #Htapef
- cases (Htapef … (refl …)) whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)
- ]
- |(* rs4 not empty *)
- * #d2 #b2 #rs3' * #d * #b * * * #Heq1 #Hnobars
- cut (is_grid d2 = false) [@daemon (* no grids in table *)] #Hd2
- whd in ⊢ ((???%)→?); #Htemp destruct (Htemp) #Htapee >Htapee -Htapee *
- [* #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) >Hd2 #Htemp destruct (Htemp)
- |* #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) #_ -Htapef #Htapef
- * #tapeg >Htapef -Htapef * whd in ⊢ (%→?);
- #H lapply (H … (refl …)) whd in ⊢ (???%→?); -H #Htapeg
- >Htapeg -Htapeg whd in ⊢ (%→?); #Htapeout
- %1 cases (some_option_hd ? (reverse ? (reverse ? la)) 〈c',true〉)
- * #c00 #b00 #Hoption
- lapply
- (Htapeout (reverse ? rs3 @〈d',false〉::reverse ? la@reverse ? (l2@[〈bar,false〉])@(〈grid,false〉::reverse ? lb))
- c' (reverse ? la) false ls bar (〈d2,true〉::rs3'@〈grid,false〉::rs) c00 b00 ?????) -Htapeout
- [whd in ⊢ (??(??%??)?); @eq_f3 [2:%|3: %]
- >associative_append
- generalize in match (〈c',true〉::reverse ? la@〈grid,false〉::ls); #l
- whd in ⊢ (???(???%)); >associative_append >associative_append %
- |>reverse_cons @Hoption
- |cases la in H2;
- [normalize in ⊢ (%→?); #Htemp destruct (Htemp)
- @injective_notb @notgridc
- |#x #tl normalize in ⊢ (%→?); #Htemp destruct (Htemp)
- @bit_not_grid @(Hl1bars 〈c',false〉) @memb_append_l2 @memb_hd
- ]
- |cut (only_bits (la@(〈c',false〉::lb)))
- [<H2 whd #c0 #Hmemb cases (orb_true_l … Hmemb)
- [#eqc0 >(\P eqc0) @Hc |@Hl1bars]
- |#Hl1' #x #Hx @bit_not_grid @Hl1'
- @memb_append_l1 @daemon
- ]
- |@daemon
- |@daemon
- ]
- ]
- ]
- |* #Hnobars #Htapee >Htapee -Htapee *
- [whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) -Htapef #_ #Htapef >Htapef -Htapef
- whd in ⊢ (%→?); #Htapeout %2
- >(Htapeout … (refl …)) %
- [ %
- [ @Hnoteq
- | whd #x #Hx @Hnobars @memb_append_l2 @memb_cons //
- ]
- | %
- ]
- |whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) -Htapef
- whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)
- ]
- |@daemon (* no marks in table *)
- |(* no grids in table *)
- #x #Hx cases (memb_append … Hx)
- [-Hx #Hx @bit_not_grid @Hl3 cases la in H3; normalize
- [#H3 destruct (H3) @Hx | #y #tl #H3 destruct (H3)
- @memb_append_l2 @memb_cons @Hx ]
- |-Hx #Hx @(no_grids_in_table … Htable)
- @memb_append_l2 @memb_cons @memb_cons @memb_append_l2 @Hx
- ]
- |whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') %
- ]
- ]
- |(* no marks in l3 *)
- @daemon
- |(* no marks in l2@[〈bar,false〉] *) @daemon
- |>associative_append %
- ]
- ]