-
Notifications
You must be signed in to change notification settings - Fork 1
/
rhanoi4.v
1135 lines (1123 loc) · 51.8 KB
/
rhanoi4.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
From mathcomp Require Import all_ssreflect finmap.
From hanoi Require Import extra gdist ghanoi ghanoi4 triangular phi rhanoi3 psi.
Set Implicit Arguments.
Unset Strict Implicit.
(******************************************************************************)
(* *)
(* This file proves the formula that gives the distance between two perfect *)
(* configurations. It follows the proof given by Thierry Bousch in *)
(* La quatrième tour de Hanoı̈ *)
(* *)
(******************************************************************************)
Section Hanoi4.
Local Notation "c1 `-->_r c2" := (rmove c1 c2)
(format "c1 `-->_r c2", at level 60).
Local Notation "c1 `-->*_r c2" := (connect rmove c1 c2)
(format "c1 `-->*_r c2", at level 60).
Lemma gdist_leq (n : nat) (p1 p2 : peg 4) :
`d[`c[p1, n], `c[p2, n]]_rmove <= ϕ(n).
Proof.
have [/eqP->|p1Dp2] := boolP (p1 == p2); first by rewrite gdist0.
elim/ltn_ind: n p1 p2 p1Dp2 => [] [|[|n]] IH p1 p2 p1Dp2.
- rewrite (_ : `c[p1] = `c[p2]) ?gdist0 //.
by apply/ffunP => [] [].
- rewrite -[phi 1]/(size [:: `c[p2, 1]]).
apply: gdist_path_le => //=.
rewrite andbT; apply/moveP; exists ldisk; split => //=.
- by rewrite !ffunE.
- by move=> [[|]].
- by apply/on_topP => [] [].
by apply/on_topP => [] [].
pose p3 := `p[p1, p2].
set k := gmin n.+2.
set k1 := k.-1.+1.
have kP : 0 < k by apply: gmin_gt0.
have k1Lm2 : k1 < n.+2 by rewrite [k1]prednK //; apply: gmin_lt.
have k1Lm2S : k1 <= n.+2 by apply: ltnW.
rewrite -[in X in X <= _](subnK k1Lm2S); set k2 := _ - _.
rewrite -perfect_liftrn; set c1 := cliftrn _ _ _.
rewrite -perfect_liftrn; set c4 := cliftrn _ _ _.
pose c2 : _ _ (k2 + k1) := cliftrn k2 p1 `c[p3].
pose c3 : _ _ (k2 + k1) := cliftrn k2 p2 `c[p3].
apply: leq_trans (_ : _ <= gdist rmove c1 c2 + _) _.
by apply: gdist_triangular.
rewrite phi_gmin /g -/k -/k1 -addnn -addnA.
apply: leq_add.
apply: leq_trans.
apply: gdist_merger; first by apply: rirr.
by apply: connect_move.
rewrite -(prednK kP).
apply: IH => //.
by rewrite eq_sym opegDl.
apply: leq_trans (_ : _ <= gdist rmove c2 c3 + _) _.
by apply: gdist_triangular.
rewrite addnC.
apply: leq_add.
apply: leq_trans.
apply: gdist_merger; first apply: rirr.
by apply: connect_move.
rewrite -(prednK kP).
apply: IH => //.
by rewrite opegDr.
rewrite /c2 /c3; move: p1Dp2.
have [p2' -> p2'E] := unlift_some (opegDr p1 p2).
rewrite -/p3.
have [p1' -> p1'E] := unlift_some (opegDl p1 p2).
move => p1Dp2.
have p1'Dp2' : p1' != p2' by apply: contra p1Dp2 => /eqP->.
rewrite -[X in _ <= X]muln1 {11}(_ : 1 = (p1' != p2')); last first.
by rewrite (negPf p1'Dp2').
rewrite -gdist_rhanoi3p -/p3 -!crliftn_perfect -!plift_perfect.
rewrite -(prednK kP).
apply: gdist_liftln => [|i j|]; first by apply: rirr.
by (apply/idP/idP; apply: contra => /eqP) => [/lift_inj->|->].
by apply: move_connect.
Qed.
Notation " `cut[ a , b ] " := (ccut a b).
Notation " `tuc[ a , b ] " := (ctuc a b).
Notation " `dup[ a , b ] " := (rm_rep a b).
(* This is theorem 2.9 *)
Lemma gdist_le_psi n (u v : configuration 4 n) (p0 p2 p3 : peg 4) :
[/\ p3 != p2, p3 != p0 & p2 != p0] ->
(codom v) \subset [:: p2 ; p3] ->
psi (s2f [set i | u i == p0]) <= `d[u, v]_rmove.
Proof.
move=> pH.
elim/ltn_ind : n u v p0 p2 p3 pH =>
// [] [|n] IH u v p0 p2 p3 [p3Dp2 p3Dp0 p2Dp0] cH.
set E := [set i | _].
suff ->: E = set0 by rewrite s2f_set0 psi_set0.
by apply/setP=> [] [].
set E := [set i | _].
pose N : disk n.+1 := ldisk.
have [NiE|NniE] := boolP (N \in E); last first.
have->: E = E :\ N.
apply/setP=> i; move: NniE; rewrite !inE.
by case: (_ =P N) => // <- /negPf->.
rewrite s2f_liftr.
apply: leq_trans (gdist_cunlift (connect_move _ _)).
by apply: IH (codom_liftr cH).
have uN0 : u N = p0 by move: NiE; rewrite inE => /eqP.
(* maybe I should do a wlog *)
pose np2 : peg _ := v N.
have vN2 : v N = np2 by [].
pose np3 : peg _ := if np2 == p2 then p3 else p2.
have np2Dp0 : np2 != p0.
have /subsetP /(_ (v N)) := cH.
by rewrite /np2 !inE => /(_ (codom_f v N))/orP[]/eqP->.
have [np3Dp0 np3Dp2] : np3 != p0 /\ np3 != np2.
rewrite /np3; case: (_ =P p2) => [->|/eqP] => //.
by move=> H; split => //; rewrite eq_sym.
have {}cH : codom v \subset [:: np2; np3].
apply/subsetP=> i /(subsetP cH); rewrite /np3 /np2 !inE.
have := subsetP cH (v N); rewrite !inE codom_f => /(_ isT) /orP[] /eqP->.
by rewrite eqxx.
by rewrite orbC ifN.
have uDv : u != v.
by apply: contra_neq np2Dp0 => uE; rewrite -uN0 uE vN2.
have /gpath_connect [g gHuv] := connect_move u v.
have vIg : v \in g.
by have := mem_last u g; rewrite inE (gpath_last gHuv) eq_sym (negPf uDv).
pose E' := [set i | [exists c, (c \in (u :: g)) && (c i == np3)]] :&: E.
have [Ez|EnZ] := boolP (E' == set0).
pose P := [set~ np3].
have aH : all (cvalid E P) (u :: g).
apply/allP => c cIg; apply/cvalidP => /= i iIE.
rewrite !inE; apply/eqP=> ciP3.
have /eqP/setP/(_ i) := Ez.
rewrite [in _ \in set0]inE => /idP[].
rewrite 2!inE iIE andbT.
by apply/existsP; exists c; rewrite cIg; apply/eqP.
have p0Isp : p0 \in P by rewrite !inE eq_sym.
have F pg1 pg2 : pg1 \in P -> pg2 \in P -> rrel pg1 pg2 ->
rrel (enum_rank_in p0Isp pg1) (enum_rank_in p0Isp pg2).
rewrite !inE /rrel /= => pg1Dp3 pg2Dpg3 pg1Dpg2.
apply: contra_neq pg1Dpg2 => /enum_rank_in_inj.
by rewrite !inE; apply.
apply: leq_trans (gpath_cset2 F aH gHuv).
have -> : cset2 E p0Isp u = `c[enum_rank_in p0Isp p0].
apply/ffunP=> i.
rewrite !ffunE; congr (enum_rank_in _ _).
by have := enum_valP i; rewrite !inE => /eqP.
have -> : cset2 E p0Isp v = `c[enum_rank_in p0Isp np2].
apply/ffunP=> i.
rewrite !ffunE; congr (enum_rank_in _ _).
have := subsetP cH (v (enum_val i)); rewrite !inE codom_f => /(_ isT).
case/orP=> /eqP //.
have /eqP/setP/(_ (enum_val i)) := Ez.
have := enum_valP i.
rewrite !inE => -> /idP/negP; rewrite andbT negb_exists.
by move=> /forallP/(_ v); rewrite -{1}(gpath_last gHuv) mem_last => /= /eqP.
have : (enum_rank_in p0Isp p0) != (enum_rank_in p0Isp np2).
rewrite eq_sym; apply/eqP => /enum_rank_in_inj.
rewrite !inE eq_sym np3Dp2 eq_sym np3Dp0 => /(_ isT isT) H.
by case/eqP: np2Dp0.
have U : #|P| = 3.
have := cardsC [set np3]; rewrite -/P.
by rewrite cards1 add1n card_ord => [] [].
move: (enum_rank_in p0Isp p0) (enum_rank_in p0Isp np2).
rewrite U => u1 v1 u1Dv1.
rewrite gdist_rhanoi3p (negPf u1Dv1) muln1 -card_s2f.
by apply: psi_exp.
rewrite -card_gt0 in EnZ.
case: (eq_bigmax_cond (@nat_of_ord _) EnZ) => /= T TinE' Tmax.
have {}Tmax := sym_equal Tmax.
have uT0 : u T = p0.
by apply/eqP; move: TinE'; rewrite !inE => /andP[].
pose E'' := [set i in E | i > T].
pose K := #|E''|.
have memE'' c i : c \in u :: g -> i \in E'' -> c i != np3.
move=> cIug; rewrite inE => /andP[iIE].
rewrite ltnNge Tmax; apply: contra => ciE.
apply: leq_bigmax_cond; rewrite inE iIE andbT inE.
by apply/existsP; exists c; rewrite cIug.
pose ST1 := isO n.+1 T.+1.
have cST1 : #|ST1| = T.+1 by rewrite card_isO; apply/minn_idPr.
(* This 3.2 *)
have KTE : T + K <= n.
rewrite -ltnS -{2}[n.+1]card_ord -addSn.
rewrite -[_ + _]subn0 -(_ : #|ST1 :&: E''| = 0); last first.
apply/eqP; rewrite cards_eq0; apply/eqP/setP => i.
rewrite /ST1 !inE; apply/idP => /and3P[].
by rewrite ltnS leqNgt => /negPf->.
by rewrite -cST1 -cardsU max_card.
move: TinE'.
rewrite !inE => /andP[/existsP[/= c_p3 /andP[]]].
rewrite inE => /orP[/eqP->|]; first by rewrite uT0 eq_sym (negPf np3Dp0).
move=> c_p3Ig /eqP c_p3T3 _.
case (@split_first _ g (fun c : configuration _ _ => c(T) != p0)).
apply/negP=> /allP /(_ _ vIg); rewrite /= -topredE negbK.
have /subsetP/(_ (v T))/(_ (codom_f _ _)) := cH.
by rewrite !inE => /orP[] /eqP->; rewrite (negPf np2Dp0, negPf np3Dp0).
move=> [[x0s x0sb] x0sa] /= [/allP x0sbP0 x0TD0 gE].
pose x0 := last u x0sb.
move : (gHuv); rewrite gE => /gpath_catl; rewrite -/x0 => gHux0.
move : (gHuv); rewrite gE => /gpath_catr; rewrite -/x0 => gHx0v.
move : (gHuv); rewrite gE => /gdist_cat; rewrite -/x0 => duvE.
have x0T0 : x0 T = p0.
have := mem_last u x0sb; rewrite !inE /x0 => /orP[/eqP->|/x0sbP0] //.
by rewrite /= -topredE negbK => /eqP.
have x0TDx0sT : x0 T != x0s T by rewrite x0T0 eq_sym.
have x0sTD0 : x0s T != p0 by rewrite eq_sym -x0T0.
have x0Mx0s : x0 `-->_r x0s.
by move: (gpath_path gHuv); rewrite gE cat_path /= -/x0 => /and3P[].
case (@split_first _ (x0s :: x0sa)
(fun c : configuration _ _ => c(T) == np3)).
have c_p3Ix0sa : c_p3 \in x0s :: x0sa.
move: c_p3Ig; rewrite gE mem_cat => /orP[/x0sbP0|//].
by rewrite /= -topredE negbK c_p3T3 (negPf np3Dp0).
apply/negP=> /allP /(_ _ c_p3Ix0sa); rewrite /= -topredE /=.
by rewrite c_p3T3 eqxx.
move => [[x3 x3b] x3a] [/allP x3bP0 /eqP x3T3 x0sx0saE].
pose x3p := last x0 x3b.
move: (gHx0v); rewrite x0sx0saE -cat_rcons => /gpath_catl.
rewrite last_rcons => gHx0x3.
move: (gHx0v); rewrite x0sx0saE -cat_rcons => /gpath_catr.
rewrite last_rcons => gHx3v.
move: (gHx0v); rewrite x0sx0saE -cat_rcons => /gdist_cat.
rewrite last_rcons => dx0vE.
have x3pND3 : x3p T != np3.
have := mem_last x0 x3b; rewrite -/x3p inE => /orP[/eqP->|/x3bP0//].
by rewrite x0T0 eq_sym.
have x3pTDx3T : x3p T != x3 T by rewrite x3T3.
have x3pMx3 : x3p `-->_r x3.
by move: (gpath_path gHx0v); rewrite x0sx0saE cat_path /= => /and3P[].
case (@split_first _ g (fun c : configuration _ _ => c(N) != p0)) => /=.
apply/negP=> /allP /(_ _ vIg); rewrite /= -topredE negbK.
have /subsetP/(_ (v N))/(_ (codom_f _ _)) := cH.
by rewrite !inE => /orP[] /eqP->; rewrite (negPf np2Dp0, negPf np3Dp0).
move=> [[z0s z0sb] z0sa] /= [/allP z0sbP0 z0sND0 gE'].
pose z0 := last u z0sb.
have z0N0 : z0 N = p0.
have := mem_last u z0sb; rewrite !inE /z0 => /orP[/eqP->|/z0sbP0] //.
by rewrite /= -topredE negbK => /eqP.
have z0NDz0sN : z0 N != z0s N by rewrite z0N0 eq_sym.
have z0Mz0s : z0 `-->_r z0s.
by move: (gpath_path gHuv); rewrite gE' cat_path /= => /and3P[].
move: (gHuv); rewrite gE' => /gpath_catl; rewrite -/z0 => gHuz0.
move: (gHuv); rewrite gE' => /gpath_catr; rewrite -/z0 => gHz0v.
move: (gHuv); rewrite gE' => /gdist_cat; rewrite -/z0 => duvE1.
case (@split_last _ (z0 :: z0s :: z0sa)
(fun c : configuration _ _ => c(N) != np2)).
have z0Iz0sz0sa : z0 \in z0 :: z0s :: z0sa by rewrite inE eqxx.
apply/negP=> /allP /(_ _ z0Iz0sz0sa); rewrite /= -topredE negbK.
by rewrite z0N0 eq_sym (negPf np2Dp0).
move=> [[z2p z2b] [|z2 z2a]] /= [z2pN2 z2aDp2 z0sz0saE].
have : last z0 (z0s :: z0sa) = z2p.
by rewrite -[last _ _]/(last z0 (z0 :: z0s :: z0sa)) z0sz0saE last_cat.
move: (gpath_last gHuv); rewrite gE' last_cat /= => -> vEz2p.
by case/eqP: z2pN2; rewrite -vEz2p.
have {}z2aEp2 z : z \in z2 :: z2a -> z N = np2.
case/andP: z2aDp2; rewrite -topredE /= negbK => /eqP z2NEp2 /allP z2aDp2.
rewrite inE => /orP[/eqP->|/z2aDp2 /=] //.
by rewrite -topredE negbK => /eqP.
have z0Ez2p : z2b = [::] -> z0 = z2p by case: z2b z0sz0saE => [[]|].
have {}z0sz0saE : z0s :: z0sa = (rcons (behead (rcons z2b z2p)) z2) ++ z2a.
case: (z2b) z0sz0saE => [[_ -> ->]|zz ll [_ ->]] //=.
by rewrite !cat_rcons.
move: (gHz0v); rewrite z0sz0saE => /gpath_catl; rewrite last_rcons => gHz0z2.
move: (gHz0v); rewrite z0sz0saE => /gpath_catr; rewrite last_rcons => gHz2v.
move: (gHz0v); rewrite z0sz0saE => /gdist_cat; rewrite last_rcons => dz0vE.
have z2Ig : z2 \in g.
by rewrite gE' z0sz0saE !(inE, mem_cat, mem_rcons, eqxx, orbT).
have z2N2 : z2 N = np2 by apply: z2aEp2; rewrite inE eqxx.
have z2pNDz2N : z2p N != z2 N by rewrite z2N2.
have z2pMz2 : z2p `-->_r z2.
move: gHz0z2; case: (z2b) z0Ez2p => [->// /gpath_path/andP[] |a l _] //=.
by rewrite -cats1 => /gpath_catr; rewrite last_rcons => /gpath_path/andP[].
(* This is 3.3 *)
have duz0_leq : psi (s2f (E :\ N)) <= `d[u, z0]_rmove.
rewrite s2f_liftr.
have /peg4comp2[pp2 [pp3 [[H1 H2 H3] [H4 H5] H6]]] := z0sND0.
have cH1 : codom ↓[z0] \subset [::pp2; pp3].
apply/subsetP=> i; rewrite !inE => /codomP[j].
rewrite !ffunE => ->.
case: (H6 (z0 (trshift 1 j))) => [/eqP|/eqP|->|->]; last 2 first.
- by rewrite eqxx.
- by rewrite eqxx orbT.
- by rewrite (negPf ( move_on_toplDr z0Mz0s z0NDz0sN _)) // -ltnS.
by rewrite -z0N0 (negPf ( move_on_toplDl z0Mz0s z0NDz0sN _)) //=.
apply: leq_trans (gdist_cunlift (connect_move _ _)).
by apply: IH cH1.
(* This is 3.4 *)
pose ST := isO n.+1 T.
have cST : #|ST| = T by rewrite card_isO; apply/minn_idPr; rewrite ltnW.
have dux0_leq : psi ((s2f E) `&` `[T]) <= `d[u, x0]_rmove.
have TLN : T <= n.+1 by rewrite ltnW.
apply: leq_trans (gpath_cut TLN gHux0).
rewrite -(@isOE n.+1 T) // -s2fI s2f_cut.
have /peg4comp2[pp2 [pp3 [[H1 H2 H3] [H4 H5] H6]]] := x0sTD0.
have cH1 : codom (ccut TLN x0) \subset [:: pp2; pp3].
apply/subsetP=> i /codomP [j]; rewrite !inE !ffunE => ->.
case: (H6 (x0 (widen_ord TLN j))) => [/eqP|/eqP|->|->]; last 2 first.
- by rewrite eqxx.
- by rewrite eqxx orbT.
- by rewrite (negPf (move_on_toplDr x0Mx0s x0TDx0sT _)) //= // ltnW.
by rewrite -x0T0 (negPf (move_on_toplDl x0Mx0s x0TDx0sT _)) /=.
by apply: IH cH1.
have [KLT|TLK] := leqP (delta K) T; last first.
have K_gt0 : 0 < K by case: (K) TLK.
have TLN : T < N by apply: leq_trans KTE; rewrite -addn1 leq_add2l.
(* This is 3. 5 *)
have psiDN : psi (s2f E) - psi (s2f (E :\ N)) <= 2 ^ K.-1.
rewrite s2fD1.
apply: psi_delta => //; last by rewrite (mem_s2f _ N).
rewrite -s2fD_isO card_s2f.
apply: subset_leq_card.
apply/subsetP=> i; rewrite !inE -leqNgt.
case: (_ == _); rewrite /= !(andbT, andbF) // => KLi.
by apply: leq_trans KLi.
have gH5 : size (z0s :: z0sa) = `d[z0, v]_rmove by have := gpath_dist gHz0v.
rewrite duvE1.
apply: leq_trans (leq_add duz0_leq (leqnn _)).
rewrite -leq_subLR; apply: leq_trans psiDN _.
rewrite dz0vE -[_ ^ _]prednK ?expn_gt0 // -add1n.
apply: leq_add.
rewrite gdist_gt0.
by apply/eqP => /ffunP/(_ N) /eqP; rewrite z0N0 z2N2 eq_sym (negPf np2Dp0).
pose P := [set~ np3].
have aH : all (cvalid (E'' :\ N) P) (z2 :: z2a).
apply/allP => c cIg; apply/cvalidP => /= i iIE''.
rewrite !inE; apply: memE''; last first.
by move: iIE''; rewrite inE => /andP[].
by rewrite gE' z0sz0saE cat_rcons inE !mem_cat cIg !orbT.
have p0Isp : p0 \in P by rewrite !inE eq_sym.
have F pg1 pg2 : pg1 \in P -> pg2 \in P -> rrel pg1 pg2 ->
rrel (enum_rank_in p0Isp pg1) (enum_rank_in p0Isp pg2).
rewrite !inE /rrel /= => pg1Dp3 pg2Dpg3 pg1Dpg2.
apply: contra_neq pg1Dpg2 => /enum_rank_in_inj.
by rewrite !inE; apply.
case: (@peg4comp3 (z2p N) np2 np3) => // [||p1 [[p1Dnp3 p1Dnp2 p1Dz] Hz]].
- move: TLN; rewrite Tmax ltnNge.
apply: contra => /eqP z2pNE; apply: leq_bigmax_cond.
rewrite inE NiE andbT inE; apply/existsP; exists z2p.
rewrite z2pNE eqxx andbT gE' /z0 z0sz0saE.
case: (z2b) z0Ez2p => [<-//=|zz ll _ /=].
by rewrite -cat_cons -/z0 mem_cat (mem_last u z0sb).
by rewrite !(inE, mem_cat, mem_rcons, eqxx, orbT).
- by rewrite eq_sym.
apply: leq_trans (gpath_cset2 F aH gHz2v).
have -> : cset2 (E'' :\ N) p0Isp z2 = `c[enum_rank_in p0Isp p1].
apply/ffunP=> i.
rewrite !ffunE; congr (enum_rank_in _ _).
case: (Hz (z2 (enum_val i))) => // /eqP; rewrite -[_ == _]negbK; case/negP.
- by rewrite (negPf ( move_on_toprDl z2pMz2 z2pNDz2N _)) // -ltnS.
- rewrite -z2N2 (negPf (move_on_toprDr z2pMz2 z2pNDz2N _)) //.
have := enum_valP i; rewrite /= !inE => /andP[/eqP/val_eqP/=].
have := ltn_ord (enum_val i); rewrite leq_eqVlt /= eqSS ltnS.
by case: ltngtP.
apply: memE''; first by rewrite inE z2Ig orbT.
by have := enum_valP i; rewrite inE => /andP[].
have -> : cset2 (E'' :\ N) p0Isp v = `c[enum_rank_in p0Isp np2].
apply/ffunP=> i.
rewrite !ffunE; congr (enum_rank_in _ _).
have := subsetP cH (v (enum_val i)); rewrite !inE codom_f => /(_ isT).
case/orP=> /eqP //.
suff /eqP : v (enum_val i) != np3 by [].
apply: memE''; first by rewrite inE vIg orbT.
by have := enum_valP i; rewrite inE => /andP[].
have : (enum_rank_in p0Isp p1) != (enum_rank_in p0Isp np2).
rewrite eq_sym; apply/eqP => /enum_rank_in_inj.
rewrite !inE eq_sym np3Dp2 p1Dnp3 => /(_ isT isT) H.
by case/eqP: p1Dnp2.
have U : #|P| = 3.
have := cardsC [set np3]; rewrite -/P.
by rewrite cards1 add1n card_ord => [] [].
move: (enum_rank_in p0Isp p1) (enum_rank_in p0Isp np2).
rewrite U => u1 v1 u1Dv1.
rewrite gdist_rhanoi3p (negPf u1Dv1) muln1 /K.
by rewrite (cardsD1 N) inE NiE TLN.
pose s := ∇((T + K).+1).
(* This is 3.7 *)
have psiDN : psi (s2f E) - psi (s2f (E :\ N)) <= 2 ^ s.-1.
rewrite s2fD1.
apply: psi_delta; last by rewrite mem_s2f.
rewrite -s2fD_isO // card_s2f.
set tS1 := isO _ _; pose tS2 := isO n.+1 T.+1.
apply: leq_trans (_ : #| E'' :|: (tS2 :\: tS1) | <= s).
apply/subset_leq_card/subsetP => i.
by rewrite !inE ltnS => /andP[-> ->]; case: (leqP i T).
apply: leq_trans (_ : #| E''| + #| tS2 :\: tS1 | <= s).
by rewrite cardsU leq_subr.
rewrite -/K.
case: (leqP T.+1 (delta s)) => [TLd|dLT].
rewrite (_ : _ :\: _ = set0) ?cards0 ?addn0.
apply: leq_trans (_ : ∇ T <= _); first by rewrite root_delta_le.
by apply: troot_le; rewrite -addnS leq_addr.
apply/setP=> i; rewrite !inE.
case: leqP => //= H.
by rewrite ltnS leqNgt (leq_trans TLd).
rewrite -card_s2f.
rewrite (_ : s2f (tS2 :\: tS1) = sint (delta s) T.+1).
rewrite card_sint //.
rewrite -(@leq_add2r (delta s)) -addnA subnK; last by rewrite ltnW.
rewrite [s + _]addnC -ltnS -!addnS -deltaS !addnS.
by rewrite -root_delta_lt [K + _]addnC -/s.
by rewrite s2fD_isO // isOE // -sint_split.
(* This is 3.8 *)
have duz0_leq2 : psi (s2f E) - 2 ^ s.-1 <= `d[u, z0]_rmove.
by apply: leq_trans duz0_leq; rewrite leq_subCl.
have [|K_gt0] := leqP K 0.
rewrite leqn0 => /eqP KE0.
have TE : T = N.
apply/val_inj/eqP; rewrite eqn_leq [T <= _](ltn_ord T) /=.
suff : N \notin E'' by rewrite inE NiE -leqNgt.
suff -> : E'' = set0 by rewrite inE.
by apply: cards0_eq.
have x3Ircons : x3 \in rcons (behead (rcons z2b z2p)) z2.
have : x3 \in g by rewrite gE x0sx0saE !(inE, mem_cat, eqxx, orbT).
rewrite gE' z0sz0saE !(inE, mem_cat).
case/or3P => // [/z0sbP0 | iIz2].
by rewrite !inE negbK -TE x3T3 (negPf np3Dp0).
have /z2aEp2/eqP : x3 \in z2 :: z2a by rewrite inE iIz2 orbT.
by rewrite -TE x3T3 (negPf np3Dp2).
pose c := z2p N.
have x0Ez0 : x0 = z0.
move: gE; rewrite gE' => /split_head[|[l5 x0sbE]|[l5 z0sbE]].
- by rewrite /x0 /z0 => [] [->].
- have /x0sbP0 : z0s \in x0sb by rewrite x0sbE !(mem_cat, inE, eqxx, orbT).
by rewrite /= negbK TE (negPf z0sND0).
have /z0sbP0 : x0s \in z0sb by rewrite z0sbE !(mem_cat, inE, eqxx, orbT).
by rewrite /= negbK -TE (negPf x0sTD0).
case: (@peg4comp3 p0 np2 np3) => [|||p1 [[p1Dnp3 p1Dnp2 p1Dp0] Hz]];
try by rewrite eq_sym.
have cDnp2 : c != np2 by rewrite /c.
have /peg4comp2[pp2 [pp3 [[H1 H2 H3] [H4 H5] H6]]] := cDnp2.
pose a := if (pp2 \in [:: p0 ; np3]) && (pp3 \in [:: p0 ; p1])
then pp2 else pp3.
pose b := if (pp2 \in [:: p0 ; np3]) && (pp3 \in [:: p0 ; p1])
then pp3 else pp2.
have [aDc aD2 aDb bDc bDnp2] :
[/\ a != c, a != np2, a != b, b != c & b != np2].
by rewrite /a /b; case: (_ && _); split; rewrite // eq_sym.
have /andP[aI bI] : (a \in [:: p0; np3]) && (b \in [:: p0; p1]).
rewrite /a /b !inE;
case: (Hz c) cDnp2 H5 H4 H3 H2 H1 => ->;
rewrite /= ?(eqxx, andbT, andbF, orbT, orbF);
case: (Hz pp2) => ->; rewrite /= ?(eqxx, andbT, andbF, orbT, orbF) ;
case: (Hz pp3) => ->; rewrite /= ?(eqxx, andbT, andbF, orbT,orbF) //;
rewrite ?[_ == p1]eq_sym ?[_ == np2]eq_sym ?[_ == np3]eq_sym;
do 6 (case: eqP; rewrite ?eqxx ?orbT //=).
have Hz1 p : [\/ p = np2, p = c, p = a | p = b].
by rewrite /a /b; case: (_ && _); case: (H6 p);
(exact: Or41 ||exact: Or42 || exact: Or43 || exact: Or44).
pose A := [set i | ↓[z2] i == a].
pose B := [set i | ↓[z2] i == b].
have z2iD2 i : ↓[z2] i != np2.
rewrite !ffunE -z2N2.
by apply: move_on_toprDr z2pMz2 _ _ => //=.
have z2iDc i : ↓[z2] i != c.
rewrite /c ffunE.
by apply: move_on_toprDl z2pMz2 _ _; rewrite //= ltnW.
have ABE : A :|: B = setT.
apply/setP=> i; rewrite !inE.
by case: (Hz1 (↓[z2] i)) (z2iD2 i) (z2iDc i) => ->; rewrite eqxx ?orbT.
(* This is 3.9 *)
have psiAB_le :
2 ^ ∇(T + K + 1) + psi `[n] <= (psi (s2f A) + psi (s2f B)).+1.*2.
rewrite -leq_double -(leq_add2r 1) !doubleS !addSnnS.
have := @psi_cap_ge (s2f A) (s2f B).
rewrite -s2fU ABE s2f_setT card_sint subn0 => /(leq_trans _)-> //.
rewrite phi_3_5_4_phi !psi_sintS addn1 ltnS leq_double.
rewrite addnC -!addnA leq_add2l !addnA.
rewrite KE0 TE addn0 addn1 -leq_double doubleD -!mul2n -!expnS.
rewrite ![(troot _).-1.+1]prednK // expnS mul2n -addnn leq_add2l.
by rewrite leq_pexp2l // troot_le.
pose xa := if a == p0 then x0 else x3.
have xaIrcons : xa \in z0 :: rcons (behead (rcons z2b z2p)) z2.
by rewrite /xa; case: (_ == p0); rewrite !inE ?x0Ez0 ?eqxx // x3Ircons orbT.
pose p1a := if a == p0 then p0 else np3.
pose p2a := if a == p0 then x0s N else x3p N.
have p1aDp2a : p1a != p2a.
by rewrite /p1a /p2a; case: (a =P p0) => aP0 //; rewrite eq_sym -TE.
have /peg4comp2[p3a [p4a [[p4aDp3a p4aDp2a p4aDp1a] [p3aDp2a p3aDp1a] p1aH]]]
:= p1aDp2a.
have acodom : codom ↓[xa] \subset [:: p3a; p4a].
apply/subsetP => i /codomP[j ->]; rewrite !inE.
case: (p1aH (↓[xa] j)) => /eqP H; try by rewrite H ?orbT.
rewrite -[_ == _]negbK in H; case/negP: H.
rewrite /xa /p1a; case: (_ == p0); rewrite !ffunE -?x0T0 -?x3T3.
by apply: (move_on_toplDl x0Mx0s x0TDx0sT); rewrite TE /=.
apply: (move_on_toprDr x3pMx3 x3pTDx3T).
by rewrite TE /=.
rewrite -[_ == _]negbK in H; case/negP: H.
rewrite /xa /p2a; case: (_ == p0); rewrite !ffunE -?x0T0 -?x3T3 -TE.
by apply: (move_on_toplDr x0Mx0s x0TDx0sT); rewrite TE ltnW /=.
apply: (move_on_toprDl x3pMx3 x3pTDx3T).
by rewrite TE /= ltnW.
have psiA_le : psi (s2f A) <= `d[↓[xa], ↓[z2]]_rmove.
rewrite gdistC; last by apply/move_sym/rsym.
apply: IH acodom; first by rewrite -ltnS.
split => //.
move: aI p4aDp1a p4aDp2a; rewrite !inE /p1a /p2a.
by case eqP => [-> _|_ /= /eqP-> ].
move: aI p3aDp1a p3aDp2a; rewrite !inE /p1a /p2a.
by case eqP => [-> _|_ /= /eqP-> ].
have bcodom : codom ↓[v] \subset [:: np2; np3].
apply/subsetP => i; rewrite !inE => /codomP[j ->].
rewrite !ffunE.
have /subsetP /(_ (v (trshift 1 j))) := cH.
by rewrite !inE; apply; apply: codom_f.
rewrite duvE1.
have psiB_le : psi (s2f B) <= `d[↓[z2], ↓[v]]_rmove.
apply: IH bcodom; first by rewrite -ltnS.
split => //.
by have := bI; rewrite !inE => /orP[] /eqP->; rewrite // eq_sym.
by have := bI; rewrite !inE => /orP[] /eqP->; rewrite // eq_sym.
have dz0z2_leq : (psi (s2f A)).+1 < `d[z0, z2]_rmove.
rewrite (gpath_dist gHz0z2) //.
rewrite [size _](@path_shift _ _ _ 1 _ _ _ (gpath_path gHz0z2)); last first.
by apply: rirr.
rewrite -add2n; apply: leq_add.
pose sx3 := @clshift _ 1 _ x3; pose sz2 := @clshift _ 1 _ z2.
have CD : #|[set i in [:: sx3; sz2]]| = 2.
rewrite (cardsD1 sx3) (cardsD1 sz2); rewrite !inE !eqxx ?orbT /=.
case: eqP => /= sz2Rsx3; last first.
congr (S (S _)); apply: eq_card0 => i; rewrite !inE.
by do 2 case: (_ == _).
have /ffunP/(_ ord0) := sz2Rsx3.
rewrite !ffunE (_ : tlshift _ _ = (ord_max : 'I_(1 + n))).
move=> /eqP.
by rewrite /= z2N2 -[ord_max]TE x3T3 eq_sym (negPf np3Dp2).
by apply/val_eqP/eqP.
rewrite -{1}CD.
apply: size_rm_rep_subset => //.
move=> i; rewrite !inE => /orP[]/eqP->; apply: map_f => //.
by rewrite mem_rcons !inE eqxx.
rewrite !inE negb_or; apply/andP; split; apply/eqP.
move=> /ffunP /( _ ord_max) /eqP.
rewrite !ffunE (_ : tlshift _ _ = (ord_max : 'I_(1 + n))) /=.
by rewrite [z0 _]z0N0 -[ord_max]TE x3T3 eq_sym (negPf np3Dp0).
by apply/val_eqP.
move=> /ffunP /( _ ord_max) /eqP.
rewrite !ffunE (_ : tlshift _ _ = (ord_max : 'I_(1 + n))) /=.
by rewrite [z0 _]z0N0 [z2 _]z2N2 eq_sym (negPf np2Dp0).
by apply/val_eqP.
apply: leq_trans psiA_le _.
rewrite /xa; case: (_ == p0).
rewrite x0Ez0.
apply: gdist_path_le.
apply: @path_crshift _ _ 1 _ _ _ (gpath_path gHz0z2).
by rewrite last_rm_rep last_map last_rcons.
move: gHz0z2.
case: (in_split x3Ircons) => l1 [l2 rE].
rewrite rE -cat_rcons => /gpath_catr.
rewrite map_cat cat_rm_rep size_cat map_rcons !last_rcons => gH3.
apply: leq_trans (leq_addl _ _).
apply: gdist_path_le.
apply: @path_crshift _ _ 1 _ _ _ (gpath_path gH3).
rewrite last_rm_rep last_map.
suff <- : last x3 (l1 ++ x3 :: l2) = last x3 l2 by rewrite -rE last_rcons.
by rewrite last_cat.
apply: leq_trans (leq_add duz0_leq2 (leqnn _)).
rewrite dz0vE addnA.
apply: leq_trans (leq_add (leqnn _) (gdist_cunlift _)); last first.
by have /gpathP[z2Pz2a <- _] := gHz2v; apply/connectP; exists z2a.
apply: leq_trans (leq_add (leq_add (leqnn _) dz0z2_leq) psiB_le).
rewrite -addnA addnC -leq_subLR.
apply: leq_sub2l.
rewrite !addSn -[(_ + _).+2]addn1 -leq_double doubleD.
apply: leq_trans (leq_add psiAB_le (leqnn _)).
by rewrite /s -mul2n -expnS prednK // addn1 -addnA leq_addr.
have TLN : T < N by apply: leq_trans KTE; rewrite -addn1 leq_add2l.
have NiE'' : N \in E'' by rewrite inE TLN NiE.
pose c : disk _ := z2p N.
case: (@peg4comp3 p0 np2 np3); rewrite // 1?eq_sym //.
move=> p1 [[p1Dnp3 p1Dnp2 p1Dp0] Hz].
have cI01 : c \in [:: p0; p1].
rewrite !inE; case: (Hz c) => /eqP => [->//|||->]; rewrite ?orbT //.
by rewrite /c -z2N2 (negPf z2pNDz2N).
rewrite /c.
suff /memE''/(_ NiE'')/negPf-> : z2p \in u :: g by [].
rewrite gE' z0sz0saE.
case: (z2b) z0Ez2p => [<- //|zz1 ll1 _].
by rewrite /z0 -cat_cons mem_cat mem_last.
by rewrite /= !(inE, mem_cat, mem_rcons, eqxx, orbT).
pose d : disk _ := x3p T.
have dD3 : d != np3 by rewrite /d -x3T3.
pose a : disk 4 := if d == np2 then c else np2.
pose b : disk 4 := if d == np2 then if c == p0 then p1 else p0
else if d == p0 then p1 else p0.
have aI2c : a \in [:: np2; c].
by rewrite /a; case: (_ == _); rewrite !(inE, eqxx, orbT).
have bI01 : b \in [:: p0; p1].
by rewrite /b; do 2 case: (_ == _); rewrite !(inE, eqxx, orbT).
have dDa : d != a.
rewrite /a; case: (d =P np2) => [->|/eqP//].
by move: cI01; rewrite !inE => /orP[] /eqP-> //; rewrite eq_sym.
have dDb : d != b.
rewrite /b; case: (d =P np2) => [->|_].
by case: (_ == p0); rewrite // eq_sym.
by case: (d =P p0) => [->|/eqP//]; rewrite eq_sym.
have bD3 : b != np3.
by move: bI01; rewrite !inE => /orP[] /eqP-> ;rewrite // eq_sym.
have bDa : b != a.
rewrite /a /b; case: (_ =P p0) => [->|/eqP cDp0].
case: (_ == np2) => [//|].
by case: (_ == p0); rewrite // eq_sym.
case: (_ == np2) => [//|]; first by rewrite eq_sym.
by case: (_ == p0); rewrite // eq_sym.
have aD3 : a != np3.
rewrite /a; case: (_ == np2); last by rewrite eq_sym.
by move: cI01; rewrite !inE => /orP[] /eqP->; rewrite // eq_sym.
have Hza i : [\/ i = a, i = b, i = np3 | i = d].
case: (Hz i) => ->.
- rewrite /a /b; do 2 (case: eqP => [->|_] //).
- by apply: Or41.
- by apply: Or42.
- by apply: Or44.
by apply: Or42.
- rewrite /a /b; do 2 (case: eqP => [->|_] //).
- by apply: Or44.
- by apply: Or44.
- by apply: Or41.
by apply: Or41.
- by apply: Or43.
rewrite /a /b; case: eqP => [->|/eqP dD2]; case: eqP => [->|/eqP cD0].
- by apply: Or42.
- move: cI01 cD0; rewrite !inE => /orP[]/eqP->; first by rewrite eqxx.
by move=> _; apply: Or41.
- by apply: Or42.
case: (Hz d) dD2 cD0 dD3 => ->; rewrite ?eqxx //.
by move=> *; apply: Or44.
move: (gE); rewrite gE' z0sz0saE x0sx0saE.
have tln : T <= n.+1 by apply: ltnW.
rewrite !cat_rcons !catA => /split_tail[[lE z2Ex3 _]|[zz x3aE]|[zz z2aE]];
last 1 first.
- move: (gHz2v); rewrite z2aE -cat_rcons => /gpath_catl.
rewrite last_rcons => gHz2x3.
move: (gHz2v); rewrite z2aE -cat_rcons => /gpath_catr.
rewrite last_rcons => gHx3v1.
move: (gHz2v); rewrite z2aE -cat_rcons => /gdist_cat.
rewrite last_rcons => dz2vE.
pose A := [set i | ccut tln x3 i == a].
pose B := [set i | ccut tln x3 i == b].
have AIB : A :&: B = set0.
apply/setP => i; rewrite !inE !ffunE /=.
case: eqP => [->|] //=.
by rewrite eq_sym (negPf bDa).
have AUB : A :|: B = setT.
apply/setP => i; rewrite !inE !ffunE.
have : ccut tln x3 i != np3.
rewrite ffunE -x3T3.
by apply: (move_on_toprDr x3pMx3) => /=.
have : ccut tln x3 i != d.
rewrite ffunE /d.
by apply: (move_on_toprDl x3pMx3) => //; rewrite ltnW /=.
by case: (Hza (ccut tln x3 i)); rewrite !ffunE => ->; rewrite ?(eqxx, orbT).
have dz2x3_leq : psi (s2f A) <= `d[z2, x3]_rmove.
rewrite gdistC; last by apply/move_sym/rsym.
have cDnp2 : c != np2 by rewrite /c.
have /peg4comp2[pp1 [pp2 [[H1 H2 H3] [H4 H5] H6]]] := cDnp2.
have cH1 : codom (ccut tln z2) \subset [:: pp1; pp2].
apply/subsetP=> i /codomP[j]; rewrite !ffunE !inE => ->.
case: (H6 (z2 (widen_ord tln j))) => /eqP; try by move->; rewrite ?orbT.
rewrite /c -[_ == z2p _]negbK => /negP[].
apply: (move_on_toprDl z2pMz2) => //=.
by apply/ltnW/(leq_trans (ltn_ord _))/ltnW.
rewrite -z2N2 -[_ == z2 _]negbK => /negP[].
apply: (move_on_toprDr z2pMz2) => //=.
by apply: (leq_trans (ltn_ord _)) => /=; apply: ltnW.
apply: leq_trans (_ : `d[ccut tln x3, ccut tln z2]_rmove <= _).
apply: IH cH1; first by apply/(leq_trans TLN _)/ltnW.
split => //.
move: aI2c; rewrite !inE.
by case: (H6 a) => -> //; rewrite (negPf H2) (negPf H3).
move: aI2c; rewrite !inE.
case: (H6 a) => -> //; first by rewrite (negPf H4) (negPf H5).
by move=> *; rewrite eq_sym.
apply: gpath_cut (gpathC _ gHz2x3).
by apply/move_sym/rsym.
have dx3v_leq : psi (s2f B) <= `d[x3, v]_rmove.
have cH1 : codom (ccut tln v) \subset [:: np2; np3].
by apply: codom_cut.
apply: leq_trans (_ : `d[ccut tln x3, ccut tln v]_rmove <= _).
apply: IH cH1; first by apply: leq_trans TLN _; apply: ltnW.
by have := bI01; rewrite !inE => /orP[] /eqP->; split; rewrite // eq_sym.
by apply: gpath_cut gHx3v.
rewrite duvE1.
apply: leq_trans (leq_add duz0_leq2 (leqnn _)).
rewrite (gpath_dist gHz0v) z0sz0saE size_cat size_rcons addnCA addnA addSnnS.
apply: leq_trans (leq_add (leq_addl _ _) (leqnn _)).
rewrite -(gpath_dist gHz2v) dz2vE.
apply: leq_trans (leq_add (leqnn _) (leq_add dz2x3_leq dx3v_leq)).
rewrite addSnnS.
suff psiAB_le : 2 ^ s <= (psi (s2f A) + psi (s2f B)).+1.*2.
rewrite -leq_double doubleD doubleB.
apply: leq_trans (leq_add (leqnn _) psiAB_le).
rewrite addnC -leq_subLR leq_sub2l //.
by rewrite -mul2n -expnS prednK.
rewrite -leq_double -mul2n -expnS -ltnS !doubleS -[_.+4]addn1 !addSnnS.
apply: leq_trans _ (psi_cap_ge _ _).
rewrite -s2fU AUB s2f_setT -(@isOE n.+1) //.
rewrite card_s2f card_isO (minn_idPr _) //.
rewrite phi_3_5_4_phi ltnS expnS mul2n leq_double.
apply: leq_trans (psi_SS_le _).
rewrite leq_exp2l // -[s]prednK // ltnS root_delta_le.
have ->: delta s.-1 = delta s - s
by rewrite -{2}[s]prednK // deltaS prednK // addnK.
have -> : T = (T + K).+1 - K.+1 :> nat by rewrite subSS addnK.
apply: leq_sub; first by apply: delta_root_le.
by rewrite root_delta_le deltaS -addnS leq_add2r.
- have z2pEx3 : z2p = x3p.
rewrite /x3p /x0 -last_cat -lE.
case: (z2b) z0Ez2p => [<-//|zz ll _] /=; first by rewrite /z0 cats0.
by rewrite last_cat last_rcons.
have /(move_disk1 z2pMz2 z2pNDz2N)/eqP : N != T by rewrite neq_ltn TLN orbT.
by rewrite z2pEx3 z2Ex3 (negPf x3pTDx3T).
(* x0 is before z0 *)
move: (gE').
rewrite gE => /split_head[ [x0sbE x0sEz0s xsaE]
|[zz1 z0sbE] | [zz1 x0sbE]]; first 2 last.
- have : z0s \in x0sb by rewrite x0sbE !(mem_cat, inE, eqxx, orbT).
move/x0sbP0; rewrite /= negbK => /eqP z0sT0.
have z0T0 : z0 T = p0.
rewrite -z0sT0; apply: move_disk1 z0Mz0s z0NDz0sN _.
by rewrite neq_ltn TLN orbT.
have : z0 T != z0 N by apply: move_on_toplDl z0Mz0s _ _.
by rewrite z0N0 z0T0 eqxx.
- case/eqP : x0TDx0sT.
rewrite /x0 x0sbE -/z0 x0sEz0s; apply: move_disk1 z0Mz0s z0NDz0sN _.
by rewrite neq_ltn TLN orbT.
pose sd : {set disk n.+1} := isO n.+1 T.
have card_sdE : #|sd| = T.
by rewrite card_isO /minn ifN // -leqNgt -ltnS ltnW // ltnW.
pose u'' := ccut tln u.
pose x0'' := ccut tln x0.
pose z2'' := ccut tln z2.
pose x3'' := ccut tln x3.
clear b bI01 dDb bD3 bDa Hza.
pose b := if c == p0 then p1 else p0.
have np3Dc : np3 != c.
by move: cI01; rewrite !inE => /orP[] /eqP->; rewrite // eq_sym.
have np3Db : np3 != b.
by move: cI01; rewrite /b !inE => /orP[] /eqP->;
rewrite ?(eqxx, negPf p1Dp0) // eq_sym.
have np2Dc : np2 != c.
by move: cI01; rewrite !inE => /orP[] /eqP->; rewrite // eq_sym.
have np2Db : np2 != b.
by move: cI01; rewrite /b !inE => /orP[] /eqP->;
rewrite ?(eqxx, negPf p1Dp0) // eq_sym.
have cDb : c != b.
by move: cI01; rewrite /b !inE => /orP[] /eqP->;
rewrite ?(eqxx, negPf p1Dp0) // eq_sym.
have Hzb i : [\/ i = np3, i = np2, i = c | i = b].
by move: cI01; rewrite /b !inE => /orP[] /eqP->;
rewrite ?(eqxx, negPf p1Dp0); case: (Hz i) => ->;
(try by apply: Or41); (try by apply: Or42);
(try by apply: Or43); (try by apply: Or44).
have bI01 : b \in [:: p0; p1].
by move: cI01; rewrite /b !inE => /orP[] /eqP->;
rewrite ?(eqxx, negPf p1Dp0) // eq_sym.
pose A : {set disk T} := [set i | z2'' i == np3].
pose B : {set disk n} := [set i | ↓[z2] i == b].
have cH2 : codom ↓[z2] \subset [:: np3; b].
apply/subsetP=> i /codomP[j]; rewrite !ffunE !inE => ->.
case: (Hzb (z2 (trshift 1 j))) => /eqP; try by move->; rewrite ?orbT.
rewrite -[_ == np2]negbK -z2N2 => /negP[].
by apply: (move_on_toprDr z2pMz2) => /=.
rewrite -[_ == c]negbK /c => /negP[].
by apply: (move_on_toprDl z2pMz2) => //=; apply: ltnW.
have bsI (i : disk n.+1) : i \in E'' :\ N -> z2 i = b.
rewrite 2!inE; rewrite -val_eqE /= => /andP[iDn iIE'']; apply/eqP.
have iLn : i < n.
by move: (ltn_ord i); rewrite leq_eqVlt eqSS (negPf iDn).
have /subsetP := cH2.
move=> /(_ (↓[z2] (Ordinal iLn))(codom_f _ _)).
rewrite !inE !ffunE /= (_ : trshift _ _ = (i : 'I_(1 + n))); last first.
by apply: val_inj.
rewrite (negPf (memE'' _ _ _ _)) //=.
by rewrite gE' z0sz0saE !(inE, mem_cat, mem_rcons, eqxx, orbT).
have dz2''x3''_leq : psi (s2f A) <= `d[z2'', x3'']_rmove.
pose a1 : peg 4 := x3p T.
have a1Dnp3 : a1 != np3 by [].
have /peg4comp2[pp1 [pp2 [[H1 H2 H3] [H4 H5] H6]]] := a1Dnp3.
have cH3 : codom x3'' \subset [:: pp1; pp2].
apply/subsetP=> i /codomP[j]; rewrite !ffunE !inE => ->.
case: (H6 (x3 (widen_ord tln j))) => /eqP; try by move->; rewrite ?orbT.
rewrite -[_ == a1]negbK => /negP[].
by apply: (move_on_toprDl x3pMx3) => //=; apply: ltnW.
rewrite -[_ == np3]negbK -x3T3 => /negP[].
by apply: (move_on_toprDr x3pMx3) => /=.
by apply: IH cH3 => //; apply/(leq_trans TLN)/ltnW.
have du''x0''_leq : psi (s2f E `&` `[T]) <= `d[u'', x0'']_rmove.
have -> : s2f E `&` `[T] = s2f [set i | u'' i == p0].
by rewrite -(@isOE n.+1) // -s2fI -s2f_cut.
have /peg4comp2[pp2 [pp3 [[H1 H2 H3] [H4 H5] H6]]] := x0sTD0.
have cH1 : codom x0'' \subset [:: pp2; pp3].
apply/subsetP=> i /codomP[j]; rewrite !inE !ffunE => ->.
case: (H6 (x0 (widen_ord tln j))) => /eqP; try by move->; rewrite ?orbT.
rewrite -[_ == x0s T]negbK => /negP[].
by apply: (move_on_toplDr x0Mx0s) => //=; apply: ltnW.
rewrite -[_ == p0]negbK -x0T0 => /negP[].
by apply: (move_on_toplDl x0Mx0s) => /=.
by apply: IH cH1=> //; apply/(leq_trans TLN _)/ltnW.
have psiAB_leq : psi `[T + K + 1] <= (psi (s2f A) + psi (s2f B)).+1.*2.
rewrite -leq_double psi_sint_phi -ltnS prednK ?phi_gt0 //.
have ->: (T + K + 1).+1 = (T + K).-1.+3.
rewrite -{1}[T + K]prednK ?addn1 ?addnS ?addn_gt0 ?K_gt0 ?orbT //.
have : (T + K).-1 <= #|` (s2f A) `|` (s2f B)|.
have : (`[T] `|` (s2f (E'' :\ N))) `<=` ((s2f A) `|` (s2f B)).
apply/fsubsetP => i; rewrite inE mem_sint /=.
case/orP => [iLT|iIEN]; last first.
have iLn : i < n.
move: iIEN; rewrite s2fD !inE s2f1 //= in_fset1.
case/andP=> iDn /imfsetP[/= j _ iEj].
by have := ltn_ord j; rewrite -iEj leq_eqVlt eqSS (negPf iDn).
rewrite inE; apply/orP; right.
rewrite (@mem_s2f _ _ (Ordinal iLn)) inE !ffunE; apply/eqP.
by apply: bsI; rewrite -mem_s2f.
have iLn : i < n by apply: leq_trans iLT (ltnW _).
have /subsetP/(_ (↓[z2] (Ordinal iLn))(codom_f _ _)) := cH2.
rewrite !inE !ffunE /=.
rewrite (@mem_s2f _ _ (Ordinal iLn)) inE ffunE.
rewrite (@mem_s2f _ _ (Ordinal iLT)) inE ffunE.
rewrite (_ : trshift _ _ = widen_ord tln (Ordinal iLT) :> 'I_(1 + n)) //.
by apply: val_inj.
move => /fsubset_leq_card /(leq_trans _)->//.
rewrite -(leq_add2r 0) addn0.
suff {2}<- : #|` `[T] `&` s2f (n:=n.+1) (E'' :\ N)| = 0.
rewrite cardfsUI card_sint subn0 card_s2f /K (cardsD1 N).
by rewrite NiE'' addnS.
apply/eqP; rewrite cardfs_eq0; apply/eqP/fsetP => i.
rewrite !inE mem_sint; apply/idP => /= /andP[iLT /imfsetP[j /=]].
rewrite !inE => /and3P[_ _ TLj] iEj.
by move: iLT; rewrite ltnNge ltnW // iEj.
rewrite -3!ltnS => /phi_le/leq_trans-> //.
rewrite !doubleS -[_.+4]addn1 !addSnnS.
by apply: psi_cap_ge.
have duz2_leq : psi (s2f E `&` `[T]) + psi (s2f A) + 2 ^ K.-1 < `d[u,z2]_rmove.
have := (gHuv); rewrite gE' z0sz0saE catA => /gpath_catl.
rewrite last_cat last_rcons => gH1.
rewrite (gpath_dist gH1) (size_cut_tuc tln _ (gpath_path gH1)); last first.
by apply: rirr.
rewrite -addnS; apply: leq_add.
have := gE'; rewrite z0sz0saE gE x0sx0saE x3aE cat_rcons.
rewrite -!cat_cons !catA -rcons_cat => /cat_injr <-.
rewrite rcons_cat !map_cat !cat_rm_rep !size_cat -addnA.
apply: leq_add.
apply: leq_trans du''x0''_leq _.
apply: gdist_path_le.
apply: path_cut.
by move : gHuv; rewrite gE => /gpath_catl/gpath_path.
by rewrite last_rm_rep last_map.
apply: leq_trans _ (leq_addl _ _).
apply: leq_trans dz2''x3''_leq _.
rewrite rcons_cons [map _ (_ ::_)]/=.
apply: leq_trans (size_rm_rep_cons _ _ _).
rewrite gdistC; last by apply/move_sym/rsym.
apply: gdist_path_le.
apply: path_cut.
by have := gHx3v; rewrite x3aE -cat_rcons => /gpath_catl/gpath_path.
by rewrite last_rm_rep map_rcons last_rcons.
have := gHuv; rewrite gE' z0sz0saE catA => /gpath_catl.
rewrite last_cat last_rcons => gHuz2.
have Puz2 := path_tuc tln (gpath_path gHuz2).
have oLn : 0 < n.+1 - T by rewrite subn_gt0.
rewrite (size_cut_tuc oLn _ Puz2) -add1n; last by apply: rirr.
have Puz3 := path_tuc oLn Puz2.
apply: leq_add.
move: gE; rewrite gE'; rewrite z0sz0saE x0sx0saE x3aE -!cat_rcons !catA.
move=> /cat_injr ->.
set cc := rm_rep _ _.
suff : ccut oLn (ctuc tln x3) \in cc by case: cc.
apply: mem_rm_rep.
apply/eqP=> /ffunP/(_ ord0); rewrite !ffunE /=.
apply/eqP; rewrite (_ : tuc_ord _ _ = T); last by apply: val_inj.
by rewrite uT0 x3T3 np3Dp0.
apply/map_f/mem_rm_rep; last first.
by apply: map_f; rewrite !(inE, mem_rcons, mem_cat, eqxx, orbT).
have onT : 0 < n.+1 - T by rewrite subn_gt0.
apply/eqP=> /ffunP/(_ (Ordinal onT)); rewrite !ffunE /=.
apply/eqP; rewrite (_ : tuc_ord _ _ = T); last by apply: val_inj.
by rewrite uT0 x3T3 np3Dp0.
have nTLnT : (n - T).-1 <= n.+1 - T - 1.
by rewrite -subn1; do 2 apply: leq_sub2r.
rewrite (size_cut_tuc nTLnT _ Puz3); last by apply: rirr.
rewrite -[2 ^ _]prednK ?expn_gt0 // -addn1.
apply: leq_add; last first.
set cc := rm_rep _ _.
suff : ctuc nTLnT (ctuc oLn (ctuc tln z2)) \in cc by case: cc.
apply: mem_rm_rep.
have oLn1 : 0 < n.+1 - T - 1 - (n - T).-1.
rewrite -subnDA add1n subSn; last by rewrite ltnW.
rewrite prednK //; last by rewrite subn_gt0.
by rewrite subn_gt0.
apply/eqP=> /ffunP/(_ (Ordinal oLn1)); rewrite !ffunE /=.
apply/eqP; rewrite (_ : tuc_ord _ _ = N); last first.
apply: val_inj; rewrite /= add0n addn1 prednK ?subnK //.
by apply: ltnW.
by rewrite subn_gt0.
by rewrite z2N2 uN0.
apply/map_f/mem_rm_rep; last first.
apply/map_f/mem_rm_rep; last first.
by apply: map_f; rewrite !(inE, mem_rcons, mem_cat, eqxx, orbT).
have oLn1 : n - T < n.+1 - T by apply: ltn_sub2r.
apply/eqP=> /ffunP/(_ (Ordinal oLn1)); rewrite !ffunE /=.
apply/eqP; rewrite (_ : tuc_ord _ _ = N); last first.
by apply: val_inj; rewrite /= subnK // ltnW.
by rewrite z2N2 uN0.
have oLn1 : (n - T).-1 < n.+1 - T - 1.
rewrite -subn1; apply: ltn_sub2r.
by rewrite ltn_subRL ltnS addn1.
by apply: ltn_sub2r.
apply/eqP=> /ffunP/(_ (Ordinal oLn1)); rewrite !ffunE /=.
apply/eqP; rewrite (_ : tuc_ord _ _ = N); last first.
by apply: val_inj; rewrite /= addn1 prednK ?subnK ?subn_gt0 // ltnW.
by rewrite z2N2 uN0.
move=> {sd card_sdE}//.
have fproj (i : 'I_(n - T).-1) : i + T.+1 < n.+1.
rewrite {3}(_ : n.+1 = ((n - T).-1 + T.+1).+1).
by rewrite ltnS leq_add2r // ltnW.
by rewrite -subnS subnK.
pose oproj i := Ordinal (fproj i).
have oprojE i : oproj i =
tuc_ord tln (tuc_ord oLn (widen_ord nTLnT i)).
by apply/val_inj; rewrite /= addn1 addnS.
rewrite !(map_cat, cat_rm_rep, size_cat).
apply: leq_trans (leq_addr _ _).
pose f (i : configuration 4 _) := ccut nTLnT (ctuc oLn (ctuc tln i)).
have /gpath_path/(path_tuc tln)/(path_tuc oLn)/(path_cut nTLnT) := gHuz0.
pose u1 := f u; rewrite -[ccut _ _]/u1.
set cs := map _ _ => path1.
have csL : last u1 (rm_rep u1 cs) = f z0.
by rewrite /u1 /cs /f !(last_rm_rep, last_map).
pose sd1 := oproj @^-1: (E'' :\ N).
have card_sd1 : #|sd1| = K.-1.
have := TLN; rewrite leq_eqVlt => /orP[/eqP /= TEN| TLNN].
have := KTE; rewrite -{2}TEN -[T.+1]addn1 leq_add2l.
case: (K) K_gt0 => // [] [] //= _ _; apply/eqP.
rewrite cards_eq0; apply/eqP/setP; move: (sd1).
suff -> : (n - T).-1 = 0 by move=> sd [].
by rewrite -{1}TEN subSn // subnn.
have ov : 0 < (n - T).-1 by rewrite -subn1 !ltn_subRL addn0 addn1.
pose o := Ordinal ov.
rewrite /sd1 /K (cardsD1 N) NiE'' /= on_card_preimset //.
exists (fun i : disk n.+1 => insubd o (i - T.+1)) => i; rewrite !inE /=.
rewrite -val_eqE => /= /and3P[iDT uEp0 _].
by apply: val_inj; rewrite val_insubd /= addnK ltn_ord.
rewrite -val_eqE => /= /and3P[iDN uEp0 TLi].
apply: val_inj; rewrite /= val_insubd ifT ?subnK //.
rewrite subnS -!subn1 !ltn_sub2r //.
by rewrite -[_ - _]prednK // subn_gt0.
by rewrite ltn_neqAle iDN /= -ltnS.
pose sp1 := [set~ np3].
have card_sp1 : #|sp1| = 3.
by have := cardsC [set np3]; rewrite cards1 card_ord => [] [].
have p0Isp : p0 \in sp1 by rewrite !inE eq_sym.
have F1 pg1 pg2 : pg1 \in sp1 -> pg2 \in sp1 -> rrel pg1 pg2 ->
rrel (enum_rank_in p0Isp pg1) (enum_rank_in p0Isp pg2).
rewrite !inE /rrel /= => pg1Dp3 pg2Dpg3 pg1Dpg2.
apply: contra_neq pg1Dpg2 => /enum_rank_in_inj.
by rewrite !inE; apply.
have csV : all (cvalid sd1 sp1) (u1 :: `dup[ u1, cs]).
apply/allP=> i; rewrite !inE => /orP[/eqP-> | iId]; apply/cvalidP => j.
rewrite !inE !ffunE /= -val_eqE /= => /and3P[jTDn /eqP uP _].
by rewrite -oprojE uP eq_sym.
rewrite !inE -val_eqE /= => /and3P[jTDn uEp0 TLjT].
have /mapP[i1 /subset_rm_rep /mapP[i2]] := subset_rm_rep iId.
move=> /subset_rm_rep /mapP[i3 i3Iz0b] -> -> ->.
rewrite !ffunE -oprojE.
apply: memE''; first by rewrite gE' !(inE, mem_cat, i3Iz0b, orbT).
by rewrite !inE /= uEp0.
apply: leq_trans (gdist_cset2 F1 csV csL path1).
have -> : cset2 sd1 p0Isp u1 = `c[enum_rank_in p0Isp p0].
apply/ffunP => i ; rewrite !ffunE /=.
have := enum_valP i; rewrite !inE /=.
rewrite (_ : tuc_ord _ _ = oproj (enum_val i)).
by move=> /and3P[_ /eqP->].
by apply: val_inj => /=; rewrite addn1 addSnnS.
case: (@peg4comp3 (z0s N) p0 np3) => [|||np1 [[np1Dnp3 np1Dp0 np1Dz] Hnz]].
- by [].
- by apply: memE'' => //; rewrite gE' !(mem_cat, inE, eqxx, orbT).
- by rewrite eq_sym.
have -> : cset2 sd1 p0Isp (f z0) = `c[enum_rank_in p0Isp np1].
apply/ffunP => i ; rewrite !ffunE /=.
have := enum_valP i; rewrite !inE -val_eqE /= => /and3P[iTEN uEp0 TLiT].
rewrite -oprojE; case: (Hnz (z0 (oproj (enum_val i)))) => // /eqP.
- rewrite -[_ == z0s N]negbK; case/negP.
apply: (move_on_toplDr z0Mz0s) => //=.
by rewrite -{8}[n](subnK TLN) leq_add2r subnS ltnW.
- rewrite -[_ == p0]negbK; case/negP; rewrite -z0N0.
apply: (move_on_toplDl z0Mz0s) => //=.
by rewrite -{8}[n](subnK TLN) ltn_add2r subnS.
rewrite -[_ == np3]negbK; case/negP.
apply: memE''.
have := mem_last u z0sb; rewrite -/z0 gE' !inE !mem_cat.
by case/orP=> ->; rewrite ?orbT.
by rewrite !inE /= uEp0.
by move=> /eqP ->.
have : (enum_rank_in p0Isp np1 != (enum_rank_in p0Isp p0)).
apply/eqP => /enum_rank_in_inj.
rewrite !inE np1Dnp3 eq_sym np3Dp0 => /(_ isT isT) /eqP.
by rewrite (negPf np1Dp0).