|
% Subtype TCC generated (at line 104, column 8) for
% single_outminmax(thiscoeff, thisachval, thisvar, depth)
% expected type {omm: Outminmax |
% (FORALL
% (nf: CoeffMono):
% (FORALL
% (i: below(nvars)):
% nf(i) <= bsdegmono(i)
% AND
% (v <= i IMPLIES f(i) = nf(i)))
% IMPLIES
% omm`lb_min
% <=
% multibscoeff
% (bspoly, bsdegmono, cf, nvars, terms)
% (nf)
% AND
% multibscoeff
% (bspoly, bsdegmono, cf, nvars, terms)
% (nf)
% <=
% omm`ub_max)
% AND unit_box_lb?(bspoly,
% bsdegmono,
% nvars,
% terms,
% cf,
% intendpts)
% (omm)
% AND unit_box_ub?(bspoly,
% bsdegmono,
% nvars,
% terms,
% cf,
% intendpts)
% (omm)
% AND length_eq?(nvars)(omm)
% AND omm`max_depth = depth}
% proved - complete
Bern_coeffs_minmax_rec_TCC1: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, cf: Coeff,
nvars: posnat, terms: posnat, f: CoeffMono, depth: nat,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
v = 0 IMPLIES
(FORALL (coefffun: [CoeffMono -> real]):
coefffun = multibscoeff(bspoly, bsdegmono, cf, nvars, terms) IMPLIES
(FORALL (thiscoeff: real):
thiscoeff = coefffun(f) IMPLIES
(FORALL (thisvar: list[real]):
thisvar = IF ep THEN corner_to_point(f, nvars) ELSE null ENDIF
IMPLIES
(FORALL (thisachval: real):
thisachval = IF ep THEN thiscoeff ELSE 0 ENDIF IMPLIES
FORALL (nf: CoeffMono):
(FORALL (i: below(nvars)):
nf(i) <= bsdegmono(i) AND
(v <= i IMPLIES f(i) = nf(i)))
IMPLIES
single_outminmax(thiscoeff,
thisachval,
thisvar,
depth)`lb_min
<=
multibscoeff(bspoly, bsdegmono, cf, nvars, terms)
(nf)
AND
multibscoeff(bspoly, bsdegmono, cf, nvars, terms)
(nf)
<=
single_outminmax(thiscoeff,
thisachval,
thisvar,
depth)`ub_max
AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf,
intendpts)
(single_outminmax(thiscoeff,
thisachval,
thisvar,
depth))
AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf,
intendpts)
(single_outminmax(thiscoeff,
thisachval,
thisvar,
depth))
AND length_eq?(nvars)
(single_outminmax(thiscoeff,
thisachval,
thisvar,
depth))
AND single_outminmax(thiscoeff,
thisachval,
thisvar,
depth)`max_depth
= depth))));
% Subtype TCC generated (at line 107, column 33) for v - 1
% expected type nat
% proved - complete
Bern_coeffs_minmax_rec_TCC2: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, f: CoeffMono,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES
(FORALL (iepts: [bool, bool]):
iepts = intendpts(v - 1) IMPLIES v - 1 >= 0);
% Subtype TCC generated (at line 113, column 89) for nep
% expected type (edge_point?(bsdegmono, nvars, nf, intendpts, v - 1))
% proved - complete
Bern_coeffs_minmax_rec_TCC3: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, f: CoeffMono,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES
(FORALL (iepts: [bool, bool]):
iepts = intendpts(v - 1) IMPLIES
(FORALL (d: upto(bsdegmono(v - 1)), nf: CoeffMono):
nf = f WITH [(v - 1) := d] IMPLIES
(FORALL (nep: boolean):
nep =
(ep AND
(d = 0 AND iepts`1 OR
bsdegmono(v - 1) /= 0 AND
d = bsdegmono(v - 1) AND iepts`2))
IMPLIES
edge_point?(bsdegmono, nvars, nf, intendpts, v - 1)(nep))));
% Termination TCC generated (at line 113, column 11) for
% Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms, nf,
% depth, intendpts, v - 1, nep)
% proved - complete
Bern_coeffs_minmax_rec_TCC4: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, f: CoeffMono,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES
(FORALL (iepts: [bool, bool]):
iepts = intendpts(v - 1) IMPLIES
(FORALL (d: upto(bsdegmono(v - 1)), nf: CoeffMono):
nf = f WITH [(v - 1) := d] IMPLIES
(FORALL (nep: boolean):
nep =
(ep AND
(d = 0 AND iepts`1 OR
bsdegmono(v - 1) /= 0 AND
d = bsdegmono(v - 1) AND iepts`2))
IMPLIES v - 1 < v)));
% Subtype TCC generated (at line 108, column 9) for
% LAMBDA (d: upto(bsdegmono(v - 1))):
% LET nf = f WITH [(v - 1) := d],
% nep =
% ep AND
% (d = 0 AND iepts`1 OR
% bsdegmono(v - 1) /= 0 AND
% d = bsdegmono(v - 1) AND iepts`2)
% IN
% Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms, nf,
% depth, intendpts, v - 1, nep)
% expected type IterateBody[Outminmax](0, bsdegmono(v - 1))
% proved - complete
Bern_coeffs_minmax_rec_TCC5: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, f: CoeffMono,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES
(FORALL (iepts: [bool, bool]):
iepts = intendpts(v - 1) IMPLIES
(FORALL (x: int):
x >= 0 AND x <= bsdegmono(v - 1) IFF
0 <= x AND x <= bsdegmono(v - 1)));
% Subtype TCC generated (at line 107, column 8) for
% iterate_left(0, bsdegmono(v - 1),
% LAMBDA (d: upto(bsdegmono(v - 1))):
% LET nf = f WITH [(v - 1) := d],
% nep =
% ep AND
% (d = 0 AND iepts`1 OR
% bsdegmono(v - 1) /= 0 AND
% d = bsdegmono(v - 1) AND iepts`2)
% IN
% Bern_coeffs_minmax_rec(bspoly,
% bsdegmono,
% cf,
% nvars,
% terms,
% nf,
% depth,
% intendpts,
% v - 1,
% nep),
% combine)
% expected type {omm: Outminmax |
% (FORALL
% (nf: CoeffMono):
% (FORALL
% (i: below(nvars)):
% nf(i) <= bsdegmono(i)
% AND
% (v <= i IMPLIES f(i) = nf(i)))
% IMPLIES
% omm`lb_min
% <=
% multibscoeff
% (bspoly, bsdegmono, cf, nvars, terms)
% (nf)
% AND
% multibscoeff
% (bspoly, bsdegmono, cf, nvars, terms)
% (nf)
% <=
% omm`ub_max)
% AND unit_box_lb?(bspoly,
% bsdegmono,
% nvars,
% terms,
% cf,
% intendpts)
% (omm)
% AND unit_box_ub?(bspoly,
% bsdegmono,
% nvars,
% terms,
% cf,
% intendpts)
% (omm)
% AND length_eq?(nvars)(omm)
% AND omm`max_depth = depth}
% proved - complete
Bern_coeffs_minmax_rec_TCC6: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, cf: Coeff,
nvars: posnat, terms: posnat, f: CoeffMono, depth: nat,
intendpts: IntervalEndpoints, v: nat,
v1:
[d1:
{z:
[MultiBernstein, bsdegmono: DegreeMono, Coeff, nvars: posnat,
posnat, f: CoeffMono, nat, intendpts: IntervalEndpoints,
v: nat, (edge_point?(bsdegmono, nvars, f, intendpts, v))] |
z`9 < v} ->
{omm: Outminmax |
FORALL (nf: CoeffMono):
(FORALL (i: below(d1`4)):
nf(i) <= d1`2(i) AND
(d1`9 <= i IMPLIES d1`6(i) = nf(i)))
IMPLIES
omm`lb_min <=
multibscoeff(d1`1, d1`2, d1`3, d1`4, d1`5)(nf)
AND
multibscoeff(d1`1, d1`2, d1`3, d1`4, d1`5)(nf)
<= omm`ub_max
AND unit_box_lb?(d1`1, d1`2, d1`4, d1`5, d1`3, d1`8)
(omm)
AND unit_box_ub?(d1`1, d1`2, d1`4, d1`5, d1`3, d1`8)
(omm)
AND length_eq?(d1`4)(omm) AND omm`max_depth = d1`7}],
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES
(FORALL (iepts: [bool, bool]):
iepts = intendpts(v - 1) IMPLIES
FORALL (nf_1: CoeffMono):
(FORALL (i: below(nvars)):
nf_1(i) <= bsdegmono(i) AND (v <= i IMPLIES f(i) = nf_1(i)))
IMPLIES
iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep AND
(d = 0 AND iepts`1 OR
bsdegmono(v - 1) /= 0 AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf, depth,
intendpts, v - 1, nep),
combine)`lb_min
<= multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf_1)
AND
multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(nf_1) <=
iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep AND
(d = 0 AND iepts`1 OR
bsdegmono(v - 1) /= 0 AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf, depth,
intendpts, v - 1, nep),
combine)`ub_max
AND unit_box_lb?(bspoly, bsdegmono, nvars, terms, cf, intendpts)
(iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep
AND
(d = 0 AND iepts`1
OR
bsdegmono(v - 1) /= 0
AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf,
depth, intendpts, v - 1, nep),
combine))
AND unit_box_ub?(bspoly, bsdegmono, nvars, terms, cf, intendpts)
(iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep
AND
(d = 0 AND iepts`1
OR
bsdegmono(v - 1) /= 0
AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf,
depth, intendpts, v - 1, nep),
combine))
AND length_eq?(nvars)
(iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep AND
(d = 0 AND iepts`1
OR
bsdegmono(v - 1) /= 0
AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf,
depth, intendpts, v - 1, nep),
combine))
AND iterate_left[Outminmax]
(0, bsdegmono(v - 1),
LAMBDA (d: upto(bsdegmono(v - 1))):
LET nf = f WITH [(v - 1) := d],
nep =
ep AND
(d = 0 AND iepts`1 OR
bsdegmono(v - 1) /= 0 AND
d = bsdegmono(v - 1) AND iepts`2)
IN
v1(bspoly, bsdegmono, cf, nvars, terms, nf, depth,
intendpts, v - 1, nep),
combine)`max_depth
= depth);
% Subtype TCC generated (at line 106, column 28) for v - 1
% expected type nat
% proved - complete
Bern_coeffs_minmax_rec_TCC7: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, f: CoeffMono,
intendpts: IntervalEndpoints, v: nat,
(ep: (edge_point?(bsdegmono, nvars, f, intendpts, v)))):
NOT v = 0 IMPLIES v - 1 >= 0;
% The subtype TCC (at line 109, column 32) in decl Bern_coeffs_minmax_rec for v - 1
% expected type <#store-print-type nat>
% is subsumed by Bern_coeffs_minmax_rec_TCC2
% The subtype TCC (at line 111, column 41) in decl Bern_coeffs_minmax_rec for v - 1
% expected type <#store-print-type nat>
% is subsumed by Bern_coeffs_minmax_rec_TCC2
% The subtype TCC (at line 112, column 43) in decl Bern_coeffs_minmax_rec for v - 1
% expected type <#store-print-type nat>
% is subsumed by Bern_coeffs_minmax_rec_TCC2
% The subtype TCC (at line 113, column 85) in decl Bern_coeffs_minmax_rec for v - 1
% expected type <#store-print-type nat>
% is subsumed by Bern_coeffs_minmax_rec_TCC2
% Subtype TCC generated (at line 120, column 88) for TRUE
% expected type (edge_point?(bsdegmono, nvars, LAMBDA (i: nat): 0,
% intendpts, nvars))
% proved - complete
Bern_coeffs_minmax_TCC1: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, intendpts: IntervalEndpoints):
edge_point?(bsdegmono, nvars, LAMBDA (i: nat): 0, intendpts, nvars)(TRUE);
% Subtype TCC generated (at line 120, column 4) for
% Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms,
% LAMBDA (i: nat): 0, depth, intendpts, nvars,
% TRUE)
% expected type (sound?(bspoly, bsdegmono, nvars, terms, cf,
% intendpts))
% proved - complete
Bern_coeffs_minmax_TCC2: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, cf: Coeff,
nvars: posnat, terms: posnat, depth: nat,
intendpts: IntervalEndpoints):
sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts)
(Bern_coeffs_minmax_rec(bspoly, bsdegmono, cf, nvars, terms,
LAMBDA (i: nat): 0, depth, intendpts, nvars,
TRUE));
% Subtype TCC generated (at line 180, column 14) for depth - level
% expected type naturalnumber
% proved - complete
Bernstein_minmax_rec_TCC1: OBLIGATION
FORALL (depth: nat, (level: upto(depth))): depth - level >= 0;
% Subtype TCC generated (at line 154, column 54) for v
% expected type nat
% unfinished
Bernstein_minmax_rec_TCC2: OBLIGATION
FORALL (bsdegmono: DegreeMono, nvars: posnat, terms: posnat, cf: Coeff,
depth: nat, (level: upto(depth)), localexit: [Outminmax -> bool],
globalexit: [Outminmax -> bool], intendpts: IntervalEndpoints,
omm: Outminmax, bp: [nat -> [nat -> [nat -> real]]],
minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
NOT level = depth AND
NOT localexit(minmax) AND
NOT between?(omm, minmax) AND NOT globalexit(minmax)
IMPLIES (FORALL (v: {k | abs(k) < abs(nvars)}): v >= 0);
% Subtype TCC generated (at line 149, column 8) for minmax
% expected type (sound?(bspoly, bsdegmono, nvars, terms, cf,
% intendpts))
% unfinished
Bernstein_minmax_rec_TCC3: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, nvars: posnat,
terms: posnat, cf: Coeff, depth: nat, (level: upto(depth)),
localexit: [Outminmax -> bool], globalexit: [Outminmax -> bool],
intendpts: IntervalEndpoints, omm: Outminmax,
bp: [nat -> [nat -> [nat -> real]]]):
bp = translist(polylist(bspoly, bsdegmono, nvars, terms)) IMPLIES
(FORALL (minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
(level = depth OR
localexit(minmax) OR between?(omm, minmax) OR globalexit(minmax))
AND
minmax =
Bern_coeffs_minmax(bp, bsdegmono, cf, nvars, terms, level, intendpts)
IMPLIES
sound?(bspoly, bsdegmono, nvars, terms, cf, intendpts)(minmax));
% Subtype TCC generated (at line 164, column 81) for level
% expected type upto(depth)
% proved - complete
Bernstein_minmax_rec_TCC4: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, nvars: posnat,
terms: posnat, cf: Coeff, depth: nat, (level: upto(depth)),
localexit: [Outminmax -> bool], globalexit: [Outminmax -> bool],
intendpts: IntervalEndpoints, varselect: VarSelector, omm: Outminmax,
bp: [nat -> [nat -> [nat -> real]]]):
bp = translist(polylist(bspoly, bsdegmono, nvars, terms)) IMPLIES
(FORALL (minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
NOT level = depth AND NOT localexit(minmax)
AND NOT between?(omm, minmax) AND NOT globalexit(minmax)
AND minmax =
Bern_coeffs_minmax(bp, bsdegmono, cf, nvars, terms, level,
intendpts)
IMPLIES
(FORALL (varsel: [bool, nat]):
varsel = varselect(bp, bsdegmono, nvars, terms, cf, level) IMPLIES
(FORALL (v: {k | abs(k) < abs(nvars)}):
v = mod(varsel`2, nvars) IMPLIES
(FORALL (spleft: [nat -> Polyproduct]):
(spleft =
(LAMBDA (k: nat):
Bern_split_left_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (spright: [nat -> Polyproduct]):
(spright =
(LAMBDA (k: nat):
Bern_split_right_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (ipleft: IntervalEndpoints):
ipleft = intendpts WITH [(v)`2 := TRUE] IMPLIES
(FORALL (ipright: IntervalEndpoints):
ipright = intendpts WITH [(v)`1 := TRUE]
IMPLIES
(FORALL (LR1: [nat -> Polyproduct],
LR2: [nat -> Polyproduct]):
LR2 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`2
AND
LR1 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`1
IMPLIES
(FORALL (LR1intendpts: IntervalEndpoints):
LR1intendpts
=
IF varsel`1
THEN ipleft
ELSE ipright
ENDIF
IMPLIES
(FORALL
(LR2intendpts: IntervalEndpoints):
LR2intendpts
=
IF varsel`1
THEN ipright
ELSE ipleft
ENDIF
IMPLIES
(FORALL
(combine_this:
[[nat, Outminmax, Outminmax] ->
Outminmax]):
combine_this
=
IF varsel`1
THEN combine_l
ELSE combine_r
ENDIF
IMPLIES
(FORALL
(newmm1: Outminmax):
newmm1 = combine(omm, minmax)
IMPLIES
(FORALL
(level1: posint):
level1 = level + 1
IMPLIES
level1 <= depth)))))))))))));
% Termination TCC generated (at line 164, column 25) for
% Bernstein_minmax_rec(LR1, bsdegmono, nvars, terms, cf, depth, level,
% localexit, globalexit, LR1intendpts, varselect,
% newmm1)
% proved - complete
Bernstein_minmax_rec_TCC5: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, nvars: posnat,
terms: posnat, cf: Coeff, depth: nat, (level: upto(depth)),
localexit: [Outminmax -> bool], globalexit: [Outminmax -> bool],
intendpts: IntervalEndpoints, varselect: VarSelector, omm: Outminmax,
bp: [nat -> [nat -> [nat -> real]]]):
bp = translist(polylist(bspoly, bsdegmono, nvars, terms)) IMPLIES
(FORALL (minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
NOT level = depth AND NOT localexit(minmax)
AND NOT between?(omm, minmax) AND NOT globalexit(minmax)
AND minmax =
Bern_coeffs_minmax(bp, bsdegmono, cf, nvars, terms, level,
intendpts)
IMPLIES
(FORALL (varsel: [bool, nat]):
varsel = varselect(bp, bsdegmono, nvars, terms, cf, level) IMPLIES
(FORALL (v: {k | abs(k) < abs(nvars)}):
v = mod(varsel`2, nvars) IMPLIES
(FORALL (spleft: [nat -> Polyproduct]):
(spleft =
(LAMBDA (k: nat):
Bern_split_left_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (spright: [nat -> Polyproduct]):
(spright =
(LAMBDA (k: nat):
Bern_split_right_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (ipleft: IntervalEndpoints):
ipleft = intendpts WITH [(v)`2 := TRUE] IMPLIES
(FORALL (ipright: IntervalEndpoints):
ipright = intendpts WITH [(v)`1 := TRUE]
IMPLIES
(FORALL (LR1: [nat -> Polyproduct],
LR2: [nat -> Polyproduct]):
LR2 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`2
AND
LR1 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`1
IMPLIES
(FORALL (LR1intendpts: IntervalEndpoints):
LR1intendpts
=
IF varsel`1
THEN ipleft
ELSE ipright
ENDIF
IMPLIES
(FORALL
(LR2intendpts: IntervalEndpoints):
LR2intendpts
=
IF varsel`1
THEN ipright
ELSE ipleft
ENDIF
IMPLIES
(FORALL
(combine_this:
[[nat, Outminmax, Outminmax] ->
Outminmax]):
combine_this
=
IF varsel`1
THEN combine_l
ELSE combine_r
ENDIF
IMPLIES
(FORALL
(newmm1: Outminmax):
newmm1 = combine(omm, minmax)
IMPLIES
(FORALL
(level1: posint):
level1 = level + 1
IMPLIES
depth - level1
<
depth - level)))))))))))));
% Subtype TCC generated (at line 168, column 12) for
% combine_this(v, bslr1, minmax)
% expected type (sound?(bspoly, bsdegmono, nvars, terms, cf,
% intendpts))
% unfinished
Bernstein_minmax_rec_TCC6: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, nvars: posnat,
terms: posnat, cf: Coeff, depth: nat, (level: upto(depth)),
v1:
[d1:
{z:
[MultiBernstein, DegreeMono, posnat, posnat, Coeff,
depth: nat, upto(depth), [Outminmax -> bool],
[Outminmax -> bool], IntervalEndpoints, VarSelector,
Outminmax] |
z`6 - z`7 < depth - level} ->
(sound?(d1`1, d1`2, d1`3, d1`4, d1`5, d1`10))],
localexit: [Outminmax -> bool], globalexit: [Outminmax -> bool],
intendpts: IntervalEndpoints, varselect: VarSelector, omm: Outminmax,
bp: [nat -> [nat -> [nat -> real]]]):
bp = translist(polylist(bspoly, bsdegmono, nvars, terms)) IMPLIES
(FORALL (minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
NOT level = depth AND NOT localexit(minmax)
AND NOT between?(omm, minmax) AND NOT globalexit(minmax)
AND minmax =
Bern_coeffs_minmax(bp, bsdegmono, cf, nvars, terms, level,
intendpts)
IMPLIES
(FORALL (varsel: [bool, nat]):
varsel = varselect(bp, bsdegmono, nvars, terms, cf, level) IMPLIES
(FORALL (v: {k | abs(k) < abs(nvars)}):
v = mod(varsel`2, nvars) IMPLIES
(FORALL (spleft: [nat -> Polyproduct]):
(spleft =
(LAMBDA (k: nat):
Bern_split_left_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (spright: [nat -> Polyproduct]):
(spright =
(LAMBDA (k: nat):
Bern_split_right_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (ipleft: IntervalEndpoints):
ipleft = intendpts WITH [(v)`2 := TRUE] IMPLIES
(FORALL (ipright: IntervalEndpoints):
ipright = intendpts WITH [(v)`1 := TRUE]
IMPLIES
(FORALL (LR1: [nat -> Polyproduct],
LR2: [nat -> Polyproduct]):
LR2 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`2
AND
LR1 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`1
IMPLIES
(FORALL (LR1intendpts: IntervalEndpoints):
LR1intendpts
=
IF varsel`1
THEN ipleft
ELSE ipright
ENDIF
IMPLIES
(FORALL
(LR2intendpts: IntervalEndpoints):
LR2intendpts
=
IF varsel`1
THEN ipright
ELSE ipleft
ENDIF
IMPLIES
(FORALL
(combine_this:
[[nat, Outminmax, Outminmax] ->
Outminmax]):
combine_this
=
IF varsel`1
THEN combine_l
ELSE combine_r
ENDIF
IMPLIES
(FORALL
(newmm1: Outminmax):
newmm1 = combine(omm, minmax)
IMPLIES
(FORALL
(level1: posint):
level1 = level + 1
IMPLIES
(FORALL
(bslr1:
(sound?
(LR1,
bsdegmono,
nvars,
terms,
cf,
LR1intendpts))):
globalexit(bslr1)
AND
bslr1
=
v1
(LR1,
bsdegmono,
nvars,
terms,
cf,
depth,
level1,
localexit,
globalexit,
LR1intendpts,
varselect,
newmm1)
IMPLIES
sound?
(bspoly,
bsdegmono,
nvars,
terms,
cf,
intendpts)
(combine_this
(v, bslr1, minmax))))))))))))))));
% Subtype TCC generated (at line 177, column 14) for
% combine_lr(v, bslrleft, bslrright)
% expected type (sound?(bspoly, bsdegmono, nvars, terms, cf,
% intendpts))
% unfinished
Bernstein_minmax_rec_TCC7: OBLIGATION
FORALL (bspoly: MultiBernstein, bsdegmono: DegreeMono, nvars: posnat,
terms: posnat, cf: Coeff, depth: nat, (level: upto(depth)),
v1:
[d1:
{z:
[MultiBernstein, DegreeMono, posnat, posnat, Coeff,
depth: nat, upto(depth), [Outminmax -> bool],
[Outminmax -> bool], IntervalEndpoints, VarSelector,
Outminmax] |
z`6 - z`7 < depth - level} ->
(sound?(d1`1, d1`2, d1`3, d1`4, d1`5, d1`10))],
localexit: [Outminmax -> bool], globalexit: [Outminmax -> bool],
intendpts: IntervalEndpoints, varselect: VarSelector, omm: Outminmax,
bp: [nat -> [nat -> [nat -> real]]]):
bp = translist(polylist(bspoly, bsdegmono, nvars, terms)) IMPLIES
(FORALL (minmax: (sound?(bp, bsdegmono, nvars, terms, cf, intendpts))):
NOT level = depth AND NOT localexit(minmax)
AND NOT between?(omm, minmax) AND NOT globalexit(minmax)
AND minmax =
Bern_coeffs_minmax(bp, bsdegmono, cf, nvars, terms, level,
intendpts)
IMPLIES
(FORALL (varsel: [bool, nat]):
varsel = varselect(bp, bsdegmono, nvars, terms, cf, level) IMPLIES
(FORALL (v: {k | abs(k) < abs(nvars)}):
v = mod(varsel`2, nvars) IMPLIES
(FORALL (spleft: [nat -> Polyproduct]):
(spleft =
(LAMBDA (k: nat):
Bern_split_left_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (spright: [nat -> Polyproduct]):
(spright =
(LAMBDA (k: nat):
Bern_split_right_mono(bp(k), bsdegmono)(v)))
IMPLIES
(FORALL (ipleft: IntervalEndpoints):
ipleft = intendpts WITH [(v)`2 := TRUE] IMPLIES
(FORALL (ipright: IntervalEndpoints):
ipright = intendpts WITH [(v)`1 := TRUE]
IMPLIES
(FORALL (LR1: [nat -> Polyproduct],
LR2: [nat -> Polyproduct]):
LR2 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`2
AND
LR1 =
IF varsel`1 THEN (spleft, spright)
ELSE (spright, spleft)
ENDIF`1
IMPLIES
(FORALL (LR1intendpts: IntervalEndpoints):
LR1intendpts
=
IF varsel`1
THEN ipleft
ELSE ipright
ENDIF
IMPLIES
(FORALL
(LR2intendpts: IntervalEndpoints):
LR2intendpts
=
IF varsel`1
THEN ipright
ELSE ipleft
ENDIF
IMPLIES
(FORALL
(combine_this:
[[nat, Outminmax, Outminmax] ->
Outminmax]):
combine_this
=
IF varsel`1
THEN combine_l
ELSE combine_r
ENDIF
IMPLIES
(FORALL
(newmm1: Outminmax):
newmm1 = combine(omm, minmax)
IMPLIES
(FORALL
(level1: posint):
level1 = level + 1
IMPLIES
(FORALL
(bslr1:
(sound?
(LR1,
bsdegmono,
nvars,
terms,
cf,
LR1intendpts))):
NOT globalexit(bslr1)
AND
bslr1
=
v1
(LR1,
bsdegmono,
nvars,
terms,
cf,
depth,
level1,
localexit,
globalexit,
LR1intendpts,
varselect,
newmm1)
IMPLIES
(FORALL
(newmm2: Outminmax):
newmm2 = combine(newmm1, bslr1)
IMPLIES
(FORALL
(bslr2:
(sound?
(LR2,
bsdegmono,
nvars,
terms,
cf,
LR2intendpts))):
bslr2
=
v1
(LR2,
bsdegmono,
nvars,
terms,
cf,
depth,
level1,
localexit,
globalexit,
LR2intendpts,
varselect,
newmm2)
IMPLIES
(FORALL
(bslrleft: Outminmax):
bslrleft
=
IF varsel`1
THEN bslr1
ELSE bslr2
ENDIF
IMPLIES
(FORALL
(bslrright: Outminmax):
bslrright
=
IF varsel`1
THEN bslr2
ELSE bslr1
ENDIF
IMPLIES
sound?
(bspoly,
bsdegmono,
nvars,
terms,
cf,
intendpts)
(combine_lr
(v,
bslrleft,
bslrright))))))))))))))))))));
% The subtype TCC (at line 155, column 55) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% The subtype TCC (at line 154, column 54) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% The subtype TCC (at line 156, column 35) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% The subtype TCC (at line 157, column 35) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% The subtype TCC (at line 168, column 25) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% The subtype TCC (at line 172, column 81) in decl Bernstein_minmax_rec for level
% expected type <#store-print-type upto(depth)>
% is subsumed by Bernstein_minmax_rec_TCC4
% The termination TCC (at line 172, column 25) in decl Bernstein_minmax_rec for
% Bernstein_minmax_rec(LR2, bsdegmono, nvars, terms, cf, depth, level,
% localexit, globalexit, LR2intendpts, varselect,
% newmm2)
% is subsumed by Bernstein_minmax_rec_TCC5
% The subtype TCC (at line 177, column 25) in decl Bernstein_minmax_rec for v
% expected type <#store-print-type nat>
% is subsumed by Bernstein_minmax_rec_TCC2
% Subtype TCC generated (at line 184, column 63) for 0
% expected type upto(depth)
% proved - complete
Bernstein_minmax_TCC1: OBLIGATION FORALL (depth: nat): 0 <= depth;
[ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
]
|
