- ] #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 …)) >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
- lapply (Htapee … Htaped ???) -Htaped -Htapee
- [whd in ⊢ (??%?); >(bit_not_grid … Hd') >(bit_not_bar … Hd') %
- |#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_cons @memb_append_l2 @Hx
- ]
- |@daemon (* TODO *)
- |*
- [* #rs3 * * (* we proceed by cases on rs4 *)
- [* #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
- %1 %
- [ //| @daemon]
- | >Htapeout %
- ]
- |* #tapef * whd in ⊢ (%→?); >Htapee -Htapee #Htapef
- cases (Htapef … (refl …)) whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)
- ]
- |* #d2 #b2 #rs3' * #d * #b * * * #Heq1 #Hnobars
- cut (is_grid d2 = false) [@daemon (* ??? *)] #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
- %
- |@daemon
- |@daemon
- |@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 …)) %
- [ %
- [ @daemon
- | @daemon
- ]
- | %
- ]
- |whd in ⊢ (%→?); * #tapef * whd in ⊢ (%→?); #Htapef
- cases (Htapef … (refl …)) -Htapef
- whd in ⊢ ((??%?)→?); #Htemp destruct (Htemp)
- ]
- |
-
-
-
-
-
-
- ????? (refl …) Hc ?) -Hcompare
- #Hcompare
- is_bit c = true → only_bits l1 → no_grids l2 → is_bit c1 = true →
- only_bits l3 → n = |l2| → |l2| = |l3| →
- table_TM (S n) (〈c1,true〉::l3@〈comma,false〉::l4) →#x
-
- #intape
-cases
- (acc_sem_if … (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 ?) intape)
-#k * #outc * * #Hloop #H1 #H2
-@(ex_intro ?? k) @(ex_intro ?? outc) %
-[ % [@Hloop ] ] -Hloop
-
\ No newline at end of file
+ ]
+ ]
+ ]
+qed.
+
+lemma generic_match_to_match_in_table :
+ ∀n,T.table_TM n T →
+ ∀qin,cin,qout,cout,mv.|qin| = n → |qout| = n →
+ only_bits qin → only_bits qout →
+ bit_or_null (\fst cin) = true → bit_or_null (\fst cout) = true →
+ bit_or_null (\fst mv) = true →
+ ∀t1,t2.
+ T = (t1@〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv])@t2 →
+ match_in_table n qin cin qout cout mv T.
+#n #T #Htable #qin #cin #qout #cout #mv #Hlenqin #Hlenqout
+#Hqinbits #Hqoutbits #Hcin #Hcout #Hmv
+elim Htable
+[ * [ #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse)
+ | #c0 #t1 #t2 normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+| #tuple #T0 #H1 #Htable0#IH #t1 #t2 #HT cases H1 #qin0 * #cin0 * #qout0 * #cout0 * #mv0
+ * * * * * * * * * *
+ #Hqin0marks #Hqout0marks #Hqin0bits #Hqout0bits #Hcin0 #Hcout0 #Hmv0 #Hcout0mv0
+ #Hlenqin0 #Hlenqout0 #Htuple
+ lapply (generic_match_to_match_in_table_tech n ? T0 t1
+ (qin@cin::〈comma,false〉::qout@[cout;〈comma,false〉;mv]@t2) H1) #Htmp
+ >Htuple in H1; #H1
+ lapply (ttm_cons … T0 H1 Htable0) <Htuple in ⊢ (%→?); >HT
+ >associative_append normalize >associative_append normalize
+ >associative_append #Htable cases (Htmp Htable ?)
+ [ #Ht1 >Htuple in HT; >Ht1 normalize in ⊢ (??%%→?);
+ >associative_append >associative_append #HT
+ cut (qin0 = qin ∧ (〈cin0,false〉 = cin ∧ (qout0 = qout ∧
+ (〈cout0,false〉 = cout ∧ (〈mv0,false〉 = mv ∧ T0 = t2)))))
+ [ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (append_l1_injective … HT) [ >Hlenqin @Hlenqin0 ]
+ #Hqin % [ @Hqin ] -Hqin
+ lapply (append_l2_injective … HT) [ >Hlenqin @Hlenqin0 ] -HT #HT
+ lapply (cons_injective_l ????? HT) #Hcin % [ @Hcin ] -Hcin
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT
+ >associative_append >associative_append #HT
+ lapply (append_l1_injective … HT) [ >Hlenqout @Hlenqout0 ]
+ #Hqout % [ @Hqout ] -Hqout
+ lapply (append_l2_injective … HT) [ >Hlenqout @Hlenqout0 ] -HT normalize #HT
+ lapply (cons_injective_l ????? HT) #Hcout % [ @Hcout ] -Hcout
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_r ????? HT) -HT #HT
+ lapply (cons_injective_l ????? HT) #Hmv % [ @Hmv ] -Hmv
+ @(cons_injective_r ????? HT) ]
+ -HT * #Hqin * #Hcin * #Hqout * #Hcout * #Hmv #HT0
+ >(?:〈bar,false〉::qin0@(〈cin0,false〉::〈comma,false〉::qout0@
+ [〈cout0,false〉;〈comma,false〉;〈mv0,false〉])@T0 = tuple@T0)
+ [ >Htuple >Hqin >Hqout >Hcin >Hcout >Hmv % //
+ | >Htuple normalize >associative_append normalize >associative_append
+ normalize >associative_append % ]
+ | * #T3 #HT3 >HT3 in HT; >associative_append; >associative_append #HT
+ lapply (append_l2_injective … HT) // -HT #HT %2 //
+ @(IH T3 t2) >HT >associative_append %
+ |>HT >associative_append normalize >associative_append normalize
+ >associative_append % ]
+]
+qed.