+alias symbol "pair" (instance 13) = "abstract pair".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "and" (instance 11) = "boolean and".
+alias symbol "plus" (instance 8) = "natural plus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "plus" (instance 6) = "natural plus".
+alias symbol "pair" (instance 5) = "abstract pair".
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias symbol "minus" (instance 3) = "natural minus".
+lemma max_gen: ∀a,b,p,f,x. a ≤b →
+ max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) = max_{i < b | leb a i ∧ p 〈i,x〉 }(f 〈i,x〉).
+#a #b #p #f #x @(bigop_I_gen ????? MaxA)
+qed.
+
+lemma max_prim_rec_base: ∀a,b,p,f,x. a ≤b →
+ max_{i < b| p 〈i,x〉 }(f 〈i,x〉) =
+ prim_rec (λi.0)
+ (λi.if p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
+#a #b #p #f #x #leab >max_gen // elim b
+ [normalize //
+ |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈i,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
+ max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
+ prim_rec (λi.0)
+ (λi.if leb a (fst i) ∧ p 〈fst i,x〉 then max (f 〈fst i,snd (snd i)〉) (fst (snd i)) else fst (snd i)) b x.
+#a #b #p #f #x #leab >max_gen // elim b
+ [normalize //
+ |#i #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >fst_pair
+ cases (true_or_false (leb a i ∧ p 〈i,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "plus" (instance 11) = "natural plus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "plus" (instance 13) = "natural plus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "plus" (instance 8) = "natural plus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "plus" (instance 6) = "natural plus".
+alias symbol "pair" (instance 5) = "abstract pair".
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias symbol "minus" (instance 3) = "natural minus".
+lemma max_prim_rec1: ∀a,b,p,f,x.
+ max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
+ prim_rec (λi.0)
+ (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
+ then max (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
+ else fst (snd i)) (b x-a x) 〈a x ,x〉.
+#a #b #p #f #x elim (b x-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+lemma sum_prim_rec1: ∀a,b,p,f,x.
+ ∑_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
+ prim_rec (λi.0)
+ (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
+ then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
+ else fst (snd i)) (b x-a x) 〈a x ,x〉.
+#a #b #p #f #x elim (b x-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "plus" (instance 11) = "natural plus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "plus" (instance 13) = "natural plus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "plus" (instance 8) = "natural plus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "pair" (instance 6) = "abstract pair".
+alias symbol "plus" (instance 4) = "natural plus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "minus" (instance 2) = "natural minus".
+lemma bigop_prim_rec: ∀a,b,c,p,f,x.
+ bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
+ prim_rec c
+ (λi.if p 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉
+ then plus (f 〈fst i +fst (snd (snd i)),snd (snd (snd i))〉) (fst (snd i))
+ else fst (snd i)) (b x-a x) 〈a x ,x〉.
+#a #b #c #p #f #x normalize elim (b x-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈i+a x,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "minus" (instance 11) = "natural minus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "minus" (instance 13) = "natural minus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "minus" (instance 8) = "natural minus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "pair" (instance 6) = "abstract pair".
+alias symbol "minus" (instance 4) = "natural minus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "minus" (instance 2) = "natural minus".
+lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
+ bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) =
+ prim_rec c
+ (λi.if p 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉
+ then plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i))
+ else fst (snd i)) (b x-a x) 〈b x ,x〉.
+#a #b #c #p #f #x normalize elim (b x-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+lemma bigop_prim_rec_dec1: ∀a,b,c,p,f,x.
+ bigop (S(b x)-a x) (λi:ℕ.p 〈b x - i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x- i,x〉) =
+ prim_rec c
+ (λi.if p 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉
+ then plus (f 〈fst (snd (snd i)) - (fst i),snd (snd (snd i))〉) (fst (snd i))
+ else fst (snd i)) (S(b x)-a x) 〈b x,x〉.
+#a #b #c #p #f #x elim (S(b x)-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ cases (true_or_false (p 〈b x - i,x〉)) #Hcase >Hcase
+ [<Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed.
+
+(*
+lemma bigop_aux_1: ∀k,c,f.
+ bigop (S k) (λi:ℕ.true) ? c plus (λi:ℕ.f i) =
+ f 0 + bigop k (λi:ℕ.true) ? c plus (λi:ℕ.f (S i)).
+#k #c #f elim k [normalize //] #i #Hind >bigop_Strue //
+
+lemma bigop_prim_rec_dec: ∀a,b,c,f,x.
+ bigop (b x-a x) (λi:ℕ.true) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) =
+ prim_rec c
+ (λi. plus (f 〈fst (snd (snd i)) - fst i,snd (snd (snd i))〉) (fst (snd i)))
+ (b x-a x) 〈b x ,x〉.
+#a #b #c #f #x normalize elim (b x-a x)
+ [normalize //
+ |#i #Hind >prim_rec_S
+ >fst_pair >snd_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ <Hind >bigop_Strue // |<Hind >bigop_Sfalse // ]
+ ]
+qed. *)
+
+lemma bigop_plus_c: ∀k,p,f,c.
+ c k + bigop k (λi.p i) ? 0 plus (λi.f i) =
+ bigop k (λi.p i) ? (c k) plus (λi.f i).
+#k #p #f elim k [normalize //]
+#i #Hind #c cases (true_or_false (p i)) #Hcase
+[>bigop_Strue // >bigop_Strue // <associative_plus >(commutative_plus ? (f i))
+ >associative_plus @eq_f @Hind
+|>bigop_Sfalse // >bigop_Sfalse //
+]
+qed.
+
+(* the argument is 〈b-a,〈a,x〉〉 *)
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "plus" (instance 3) = "natural plus".
+alias symbol "pair" (instance 2) = "abstract pair".
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias symbol "plus" (instance 5) = "natural plus".
+alias symbol "pair" (instance 4) = "abstract pair".
+definition max_unary_pr ≝ λp,f.unary_pr (λx.0)
+ (λi.
+ let k ≝ fst i in
+ let r ≝ fst (snd i) in
+ let a ≝ fst (snd (snd i)) in
+ let x ≝ snd (snd (snd i)) in
+ if p 〈k + a,x〉 then max (f 〈k+a,x〉) r else r).
+
+lemma max_unary_pr1: ∀a,b,p,f,x.
+ max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) =
+ ((max_unary_pr p f) ∘ (λx.〈b x - a x,〈a x,x〉〉)) x.
+#a #b #p #f #x normalize >fst_pair >snd_pair @max_prim_rec1
+qed.
+
+(*
+lemma max_unary_pr: ∀a,b,p,f,x.
+ max_{i ∈[a,b[ | p 〈i,x〉 }(f 〈i,x〉) =
+ prim_rec (λi.0)
+ (λi.if p 〈fst i +a,x〉 then max (f 〈fst i +a ,snd (snd i)〉) (fst (snd i)) else fst (snd i)) (b-a) x.
+*)
+
+(*
+definition unary_compl ≝ λp,f,hf.
+ unary_pr MSC
+ (λx:ℕ
+ .fst (snd x)
+ +hf
+ 〈fst x,
+ 〈unary_pr (λx0:ℕ.O)
+ (λi:ℕ
+ .(let (k:ℕ) ≝fst i in
+ let (r:ℕ) ≝fst (snd i) in
+ let (a:ℕ) ≝fst (snd (snd i)) in
+ let (x:ℕ) ≝snd (snd (snd i)) in
+ if p 〈k+a,x〉 then max (f 〈k+a,x〉) r else r )) 〈fst x,snd (snd x)〉,
+ snd (snd x)〉〉). *)
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "plus" (instance 6) = "natural plus".
+alias symbol "pair" (instance 5) = "abstract pair".
+alias symbol "plus" (instance 4) = "natural plus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "plus" (instance 2) = "natural plus".
+alias symbol "plus" (instance 1) = "natural plus".
+definition aux_compl ≝ λhp,hf.λi.
+ let k ≝ fst i in
+ let r ≝ fst (snd i) in
+ let a ≝ fst (snd (snd i)) in
+ let x ≝ snd (snd (snd i)) in
+ hp 〈k+a,x〉 + hf 〈k+a,x〉 + (* was MSC r*) MSC i .
+
+definition aux_compl1 ≝ λhp,hf.λi.
+ let k ≝ fst i in
+ let r ≝ fst (snd i) in
+ let a ≝ fst (snd (snd i)) in
+ let x ≝ snd (snd (snd i)) in
+ hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
+
+lemma aux_compl1_def: ∀k,r,m,hp,hf.
+ aux_compl1 hp hf 〈k,〈r,m〉〉 =
+ let a ≝ fst m in
+ let x ≝ snd m in
+ hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
+#k #r #m #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair //
+qed.
+
+lemma aux_compl1_def1: ∀k,r,a,x,hp,hf.
+ aux_compl1 hp hf 〈k,〈r,〈a,x〉〉〉 = hp 〈k+a,x〉 + hf 〈k+a,x〉 + MSC r.
+#k #r #a #x #hp #hf normalize >fst_pair >snd_pair >snd_pair >fst_pair
+>fst_pair >snd_pair //
+qed.
+
+
+axiom Oaux_compl: ∀hp,hf. O (aux_compl1 hp hf) (aux_compl hp hf).
+
+(*
+definition IF ≝ λb,f,g:nat →option nat. λx.
+ match b x with
+ [None ⇒ None ?
+ |Some n ⇒ if (eqb n 0) then f x else g x].
+*)
+
+axiom CF_if: ∀b:nat → bool. ∀f,g,s. CF s b → CF s f → CF s g →
+ CF s (λx. if b x then f x else g x).
+
+(*
+lemma IF_CF: ∀b,f,g,sb,sf,sg. CF sb b → CF sf f → CF sg g →
+ CF (λn. sb n + sf n + sg n) (IF b f g).
+#b #f #g #sb #sf #sg #Hb #Hf #Hg @IF_CF_new
+ [@(monotonic_CF … Hb) @O_plus_l @O_plus_l //
+ |@(monotonic_CF … Hf) @O_plus_l @O_plus_r //
+ |@(monotonic_CF … Hg) @O_plus_r //
+ ]
+qed.
+*)
+
+axiom CF_le: ∀h,f,g. CF h f → CF h g → CF h (λx. leb (f x) (g x)).
+axiom CF_max1: ∀h,f,g. CF h f → CF h g → CF h (λx. max (f x) (g x)).
+axiom CF_plus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x + g x).
+axiom CF_minus: ∀h,f,g. CF h f → CF h g → CF h (λx. f x - g x).
+
+axiom MSC_prop: ∀f,h. CF h f → ∀x. MSC (f x) ≤ h x.
+
+lemma MSC_max: ∀f,h,x. CF h f → MSC (max_{i < x}(f i)) ≤ max_{i < x}(h i).
+#f #h #x #hf elim x // #i #Hind >bigop_Strue [|//] >bigop_Strue [|//]
+whd in match (max ??);
+cases (true_or_false (leb (f i) (bigop i (λi0:ℕ.true) ? 0 max(λi0:ℕ.f i0))))
+#Hcase >Hcase
+ [@(transitive_le … Hind) @le_maxr //
+ |@(transitive_le … (MSC_prop … hf i)) @le_maxl //
+ ]
+qed.
+
+lemma CF_max: ∀a,b.∀p:nat →bool.∀f,ha,hb,hp,hf,s.
+ CF ha a → CF hb b → CF hp p → CF hf f →
+ O s (λx.ha x + hb x +
+ (∑_{i ∈[a x ,b x[ }
+ (hp 〈i,x〉 + hf 〈i,x〉 + max_{i ∈ [a x, b x [ }(hf 〈i,x〉)))) →
+ CF s (λx.max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉)).
+#a #b #p #f #ha #hb #hp #hf #s #CFa #CFb #CFp #CFf #HO
+@ext_CF1 [|#x @max_unary_pr1]
+@(CF_comp ??? (λx.ha x + hb x))
+ [|@CF_comp_pair
+ [@CF_minus [@(O_to_CF … CFb) @O_plus_r // |@(O_to_CF … CFa) @O_plus_l //]
+ |@CF_comp_pair
+ [@(O_to_CF … CFa) @O_plus_l //
+ | @(O_to_CF … CF_id) @O_plus_r @(proj1 … CFb)
+ ]
+ ]
+ |@(CF_prim_rec … MSC … (aux_compl1 hp hf))
+ [@CF_const
+ |@(O_to_CF … (Oaux_compl … ))
+ @CF_if
+ [@(CF_comp p … MSC … CFp)
+ [@CF_comp_pair
+ [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
+ |@CF_comp_snd @CF_comp_snd @CF_snd]
+ |@le_to_O #x normalize >commutative_plus >associative_plus @le_plus //
+ ]
+ |@CF_max1
+ [@(CF_comp f … MSC … CFf)
+ [@CF_comp_pair
+ [@CF_plus [@CF_fst| @CF_comp_fst @CF_comp_snd @CF_snd]
+ |@CF_comp_snd @CF_comp_snd @CF_snd]
+ |@le_to_O #x normalize >commutative_plus //
+ ]
+ |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
+ ]
+ |@CF_comp_fst @(monotonic_CF … CF_snd) normalize //
+ ]
+ |@O_refl
+ ]
+ |@(O_trans … HO) -HO
+ @(O_trans ? (λx:ℕ
+ .ha x+hb x
+ +bigop (b x-a x) (λi:ℕ.true) ? (MSC 〈a x,x〉) plus
+ (λi:ℕ
+ .(λi0:ℕ
+ .hp 〈i0,x〉+hf 〈i0,x〉
+ +bigop (b x-a x) (λi1:ℕ.true) ? 0 max
+ (λi1:ℕ.(λi2:ℕ.hf 〈i2,x〉) (i1+a x))) (i+a x))))
+ [
+ @le_to_O #n @le_plus // whd in match (unary_pr ???);
+ >fst_pair >snd_pair >bigop_prim_rec elim (b n - a n)
+ [normalize //
+ |#x #Hind >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >aux_compl1_def1
+ >prim_rec_S >fst_pair >snd_pair >fst_pair >snd_pair >fst_pair
+ >snd_pair normalize in ⊢ (??%); >commutative_plus @le_plus
+ [-Hind @le_plus // normalize >fst_pair >snd_pair
+ @(transitive_le ? (bigop x (λi1:ℕ.true) ? 0 (λn0:ℕ.λm:ℕ.if leb n0 m then m else n0 )
+ (λi1:ℕ.hf 〈i1+a n,n〉)))
+ [elim x [normalize @MSC_le]
+ #x0 #Hind >prim_rec_S >fst_pair >snd_pair >snd_pair >snd_pair
+ >fst_pair >fst_pair cases (p 〈x0+a n,n〉) normalize
+ [cases (true_or_false (leb (f 〈x0+a n,n〉)
+ (prim_rec (λx00:ℕ.O)
+ (λi:ℕ
+ .if p 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
+ then if leb (f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉)
+ (fst (snd i))
+ then fst (snd i)
+ else f 〈fst i+fst (snd (snd i)),snd (snd (snd i))〉
+ else fst (snd i) ) x0 〈a n,n〉))) #Hcase >Hcase normalize
+ [@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
+ |@(transitive_le … (MSC_prop … CFf …)) @(le_maxl … (le_n …))
+ ]
+ |@(transitive_le … Hind) -Hind @(le_maxr … (le_n …))
+ ]
+ |@(le_maxr … (le_n …))
+ ]
+ |@(transitive_le … Hind) -Hind
+ generalize in match (bigop x (λi:ℕ.true) ? 0 max
+ (λi1:ℕ.(λi2:ℕ.hf 〈i2,n〉) (i1+a n))); #c
+ generalize in match (hf 〈x+a n,n〉); #c1
+ elim x [//] #x0 #Hind
+ >prim_rec_S >prim_rec_S normalize >fst_pair >fst_pair >snd_pair
+ >snd_pair >snd_pair >snd_pair >snd_pair >snd_pair >fst_pair >fst_pair
+ >fst_pair @le_plus
+ [@le_plus // cases (true_or_false (leb c1 c)) #Hcase
+ >Hcase normalize // @lt_to_le @not_le_to_lt @(leb_false_to_not_le ?? Hcase)
+ |@Hind
+ ]
+ ]
+ ]
+ |@O_plus [@O_plus_l //] @le_to_O #x
+ <bigop_plus_c @le_plus // @(transitive_le … (MSC_pair …)) @le_plus
+ [@MSC_prop @CFa | @MSC_prop @(O_to_CF MSC … (CF_const x)) @(proj1 … CFb)]
+ ]
+qed.
+
+(* old