| products/Sources/formale Sprachen/PVS/Bernstein/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: permutations_seq.prf Sprache: Unknown
|
Spracherkennung für: .tccs vermutete Sprache: Python {Python[70] Fortran[180] Ada[190]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] % 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.216 Sekunden ] |