definition compare ≝ λi,j,sig,n.
whileTM … (compare_step i j sig n) comp1.
+(* (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
+ (∃rs0'.rs0 = rs@rs0' ∧
+ outt = change_vec ??
+ (change_vec ?? int
+ (mk_tape sig (reverse sig rs@x::ls) (None sig) []) i)
+ (mk_tape sig (reverse sig rs@x::ls0) (option_hd sig rs0')
+ (tail sig rs0')) j) ∨
+ (∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
+ outt = change_vec ??
+ (change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
+ (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).*)
definition R_compare ≝
λi,j,sig,n.λint,outt: Vector (tape sig) (S n).
((current ? (nth i ? int (niltape ?)) ≠ current ? (nth j ? int (niltape ?)) ∨
(* nth i ? int (niltape ?) = midtape sig ls x (xs@ci::rs) → *)
nth i ? int (niltape ?) = midtape sig ls x rs →
nth j ? int (niltape ?) = midtape sig ls0 x rs0 →
- (∃rs'.rs = rs0@rs' ∧ current ? (nth j ? outt (niltape ?)) = None ?) ∨
+ (∃rs'.rs = rs0@rs' ∧
+ outt = change_vec ??
+ (change_vec ?? int
+ (mk_tape sig (reverse sig rs0@x::ls) (option_hd sig rs') (tail ? rs')) i)
+ (mk_tape sig (reverse sig rs0@x::ls0) (None ?) [ ]) j) ∨
(∃rs0'.rs0 = rs@rs0' ∧
outt = change_vec ??
(change_vec ?? int
(∃xs,ci,cj,rs',rs0'.ci ≠ cj ∧ rs = xs@ci::rs' ∧ rs0 = xs@cj::rs0' ∧
outt = change_vec ??
(change_vec ?? int (midtape sig (reverse ? xs@x::ls) ci rs') i)
- (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).
+ (midtape sig (reverse ? xs@x::ls0) cj rs0') j)).
lemma wsem_compare : ∀i,j,sig,n.i ≠ j → i < S n → j < S n →
compare i j sig n ⊫ R_compare i j sig n.
[ -IH2 #Hnthj % % %{(r1::rs1)} % [%]
>Hnthj in Hd; #Hd >Hd in IH1; #IH1 >IH1
[| %2 >nth_change_vec // ]
- >nth_change_vec //
+ >Hnthi >Hnthj %
| #r2 #rs2 #Hnthj lapply IH2; >Hd in IH1; >Hnthi >Hnthj
>nth_change_vec //
>nth_change_vec_neq [| @sym_not_eq // ] >nth_change_vec //
cases (true_or_false (r1 == r2)) #Hr1r2
[ >(\P Hr1r2) #_ #IH2 cases (IH2 … (refl ??) (refl ??)) [ *
[ * #rs' * #Hrs1 #Hcurout_j % % %{rs'}
- >Hrs1 >Hcurout_j normalize % //
+ >Hrs1 %
+ [ %
+ | >Hcurout_j >change_vec_commute // >change_vec_change_vec
+ >change_vec_commute // @sym_not_eq // ]
| * #rs0' * #Hrs2 #Hcurout_i % %2 %{rs0'}
>Hrs2 >Hcurout_i % //
>change_vec_commute // >change_vec_change_vec