definition STape ≝ FinProd … FSUnialpha FinBool.
definition only_bits ≝ λl.
- ∀c.memb STape c l = true → is_bit (\fst c) = true.
+ ∀c.memb STape c l
+ = true → is_bit (\fst c) = true.
definition only_bits_or_nulls ≝ λl.
∀c.memb STape c l = true → bit_or_null (\fst c) = true.
match_in_table n qin cin qout cout mv
(mk_tuple qin0 cin0 qout0 cout0 mv0@tb).
-axiom append_l1_injective :
- ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
-axiom append_l2_injective :
- ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
-axiom append_l1_injective_r :
- ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
-axiom append_l2_injective_r :
- ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
-axiom cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
-axiom cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
axiom tuple_len : ∀n,t.tuple_TM n t → |t| = 2*n+6.
axiom append_eq_tech1 :
∀A,l1,l2,l3,l4.l1@l2 = l3@l4 → |l1| < |l3| → ∃la:list A.l1@la = l3.
[ #la * #lb * #HT1c #HT0 %{lb} >HT1c @(eq_f2 ??? (append ?) (c::la)) //
>HT0 in Ht'; >HT1c >associative_append in ⊢ (???%→?); #Ht'
<(append_l1_injective_r … Ht') // <(cons_injective_l ????? Ht) %
- |@daemon ]
+ |@(noteq_to_eqnot ? true) @(not_to_not … not_eq_true_false) #Hbar @sym_eq
+ cases (memb_append … Hbar) -Hbar #Hbar
+ [@(Hqin2 … Hbar)
+ |cases (orb_true_l … Hbar) -Hbar
+ [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcin
+ |whd in ⊢ ((??%?)→?); #Hbar cases (memb_append … Hbar) -Hbar #Hbar
+ [@(Hqout2 … Hbar)
+ |cases (orb_true_l … Hbar) -Hbar
+ [#Hbar lapply (\P Hbar) -Hbar #Hbar destruct (Hbar) @Hcout
+ |#Hbar cases (orb_true_l … Hbar) -Hbar
+ [whd in ⊢ ((??%?)→?); #Hbar @Hbar
+ |#Hbar lapply (memb_single … Hbar) -Hbar #Hbar destruct (Hbar) @Hmv
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
qed.
lemma generic_match_to_match_in_table :
∨
(no_bars rs1 ∧ t2 = midtape ? (reverse ? rs1@c::ls) 〈grid,false〉 rs2).
+axiom daemon :∀P:Prop.P.
+
axiom tech_split :
∀A:DeqSet.∀f,l.
(∀x.memb A x l = true → f x = false) ∨