+letin value ≝ (
+ let rec value (p: ℚ) (l : list bar) on l ≝
+ match l with
+ [ nil ⇒ 〈O,OQ〉
+ | cons x tl ⇒
+ match q_cmp p (Qpos (\fst x)) with
+ [ q_lt _ ⇒ 〈O, \snd x〉
+ | _ ⇒
+ let rc ≝ value (p - Qpos (\fst x)) tl in
+ 〈S (\fst rc),\snd rc〉]]
+ in value :
+ ∀acc,l.∃p:nat × ℚ. OQ ≤ acc →
+ And3
+ (sum_bases l (\fst p) ≤ acc)
+ (acc < sum_bases l (S (\fst p)))
+ (\snd p = \snd (nth l ▭ (\fst p))));
+[5: clearbody value;
+ cases (q_cmp i (start f));
+ [2: exists [apply 〈O,OQ〉] simplify; reflexivity;
+ |*: cases (value (i - start f) (bars f)) (p Hp);
+ cases Hp; clear Hp value;
+ exists[1,3:apply p]; simplify; split; assumption;]
+|1,3: intros; split;
+ [1,4: clear H2; cases (value (q-Qpos (\fst b)) l1); cases H2; clear H2;
+ simplify; apply q_le_minus; assumption;
+ |2,5: cases (value (q-Qpos (\fst b)) l1); cases H3; clear H3 H2 value;
+ change with (q < sum_bases l1 (S (\fst w)) + Qpos (\fst b));
+ apply q_lt_plus; assumption;
+ |*: cases (value (q-Qpos (\fst b)) l1); simplify; cases H3; clear H3 value H2;
+ assumption;]
+|2: clear value H2; simplify; split;
+ [1:
+
+
+definition same_shape ≝
+ λl1,l2:q_f.
+ ∀input.∃col.
+
+ And3
+ (sum_bases (bars l2) j ≤ offset - start l2)
+ (offset - start l2 ≤ sum_bases (bars l2) (S j))
+ (\snd (nth (bars l2)) q0 j) = \snd (nth (bars l1) q0 i).
+
+…┐─┌┐…
+\ldots\boxdl\boxh\boxdr\boxdl\ldots
+
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
+definition rebase_spec ≝
+ ∀l1,l2:q_f.∃p:q_f × q_f.
+ And4
+ (len (bars (\fst p)) = len (bars (\snd p)))
+ (start (\fst p) = start (\snd p))
+ (∀i.\fst (nth (bars (\fst p)) q0 i) = \fst (nth (bars (\snd p)) q0 i))
+ (∀i,offset.
+ sum_bases (bars l1) i ≤ offset - start l1 →
+ offset - start l1 ≤ sum_bases (bars l1) (S i) →
+ ∃j.
+ And3
+ (sum_bases (bars (\fst p)) j ≤ offset - start (\fst p))
+ (offset - start (\fst p) ≤ sum_bases (bars (\fst p)) (S j))
+ (\snd (nth (bars (\fst p)) q0 j) = \snd (nth (bars l1) q0 i)) ∧
+ And3
+ (sum_bases (bars (\snd p)) j ≤ offset - start (\snd p))
+ (offset - start (\snd p) ≤ sum_bases (bars (\snd p)) (S j))
+ (\snd (nth (bars (\snd p)) q0 j) = \snd (nth (bars l2) q0 i))).
+
+definition rebase_spec_simpl ≝
+ λl1,l2:list (ℚ × ℚ).λp:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).
+ len ( (\fst p)) = len ( (\snd p)) ∧
+ (∀i.
+ \fst (nth ( (\fst p)) q0 i) =
+ \fst (nth ( (\snd p)) q0 i)) ∧
+ ∀i,offset.
+ sum_bases ( l1) i ≤ offset ∧
+ offset ≤ sum_bases ( l1) (S i)
+ →
+ ∃j.
+ sum_bases ( (\fst p)) j ≤ offset ∧
+ offset ≤ sum_bases ((\fst p)) (S j) ∧
+ \snd (nth ( (\fst p)) q0 j) =
+ \snd (nth ( l1) q0 i).
+
+definition eject ≝
+ λP.λp:∃x:(list bar) × (list bar).P x.match p with [ex_introT p _ ⇒ p].
+coercion eject.
+definition inject ≝ λP.λp:(list bar) × (list bar).λh:P p. ex_introT ? P p h.
+coercion inject with 0 1 nocomposites.
+
+definition rebase: rebase_spec.
+intros 2 (f1 f2); cases f1 (s1 l1); cases f2 (s2 l2); clear f1 f2;
+letin spec ≝ (
+ λl1,l2:list (ℚ × ℚ).λm:nat.λz:(list (ℚ × ℚ)) × (list (ℚ × ℚ)).
+ len l1 + len l2 < m → rebase_spec_simpl l1 l2 z);