|
(sigma_swap
(IMP_sigma_TCC1 0
(IMP_sigma_TCC1-1 nil 3479639154
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil sigma_swap nil)) nil))
(sigma_swap 0
(sigma_swap-1 nil 3479639154
(""
(case "NOT (FORALL (lowz: T_low, highz: T_high): NOT lowz > highz IMPLIES T_pred(highz))")
(("1" (hide 2)
(("1" (skosimp* t)
(("1" (assert)
(("1" (skosimp*)
(("1" (typepred "j!1")
(("1" (lemma "connected_domain")
(("1" (inst - "lowz!1" "j!1" "highz!1")
(("1" (assert) nil nil)
("2" (prop)
(("2" (skosimp*)
(("2" (lemma "connected_domain")
(("2" (assert)
(("2" (inst - "j!2" "j!1" "lowz!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (label "Tplem" -1)
(("2" (hide "Tplem")
(("2" (skeep)
(("2" (case "high1 >= low1 AND high2 >= low2")
(("1" (flatten)
(("1" (name "k1" "high1-low1")
(("1" (name "k2" "high2-low2")
(("1"
(case "high1 = low1 + k1 AND high2 = low2 + k2")
(("1" (flatten)
(("1" (replace -1)
(("1" (replace -2)
(("1"
(case "FORALL (kk1: nat): T_high?(low1+kk1) IMPLIES sigma(low1,low1+kk1,LAMBDA (i: T): sigma(low2, low2 + k2, LAMBDA (j: T): F(i, j))) = sigma(low2, low2 + k2,
LAMBDA (j: T): sigma(low1, low1 + kk1, LAMBDA (i: T): F(i, j)))")
(("1" (inst - "k1")
(("1"
(assert)
(("1"
(typepred "high1")
(("1"
(split -)
(("1"
(inst + "high1")
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (hide 2)
(("2"
(induct "kk1")
(("1"
(flatten)
(("1"
(assert)
(("1"
(expand "sigma" 1 1)
(("1"
(expand "sigma" 1 1)
(("1"
(expand "sigma" 1 3)
(("1"
(expand "sigma" 1 3)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(split -)
(("1"
(case "NOT T_pred(low1+(j!1+1))")
(("1"
(reveal "Tplem")
(("1"
(inst - "low1" "1+j!1+low1")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(inst + "j!2")
nil
nil))
nil))
nil))
nil)
("2"
(lemma "sigma_split")
(("2"
(inst
-
"LAMBDA (i: T): sigma(low2, low2 + k2, LAMBDA (j: T): F(i, j))"
"low1 + (j!1+1)"
"low1"
"low1 + j!1")
(("2"
(assert)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand "sigma" 1 1)
(("2"
(expand
"sigma"
1
1)
(("2"
(replace -2)
(("2"
(hide -2)
(("2"
(rewrite
"sigma_sum")
(("1"
(expand
"sigma"
1
4)
(("1"
(propax)
nil
nil))
nil)
("2"
(skosimp*)
(("2"
(inst
+
"j!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "j!2")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3" (inst + "j!1") nil nil))
nil)
("4"
(skosimp*)
(("4"
(typepred "high2")
(("4" (assert) nil nil))
nil))
nil)
("5"
(skosimp*)
(("5"
(typepred "high2")
(("5" (assert) nil nil))
nil))
nil)
("6" (skosimp*) nil nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst + "j!1") nil nil)) nil)
("4" (skosimp*) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (split)
(("1" (expand "sigma" 2 1)
(("1" (assert)
(("1" (expand "sigma" 2 2)
(("1" (lemma "sigma_zero")
(("1" (inst - "high2" "low2")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "sigma" 2 2)
(("2" (assert)
(("2" (expand "sigma" 2 2)
(("2" (lemma "sigma_zero")
(("2" (inst - "high1" "low1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_zero formula-decl nil sigma nil)
(sigma_nat application-judgement "nat" sigma_swap nil)
(sigma_nnreal application-judgement "nnreal" sigma_swap nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(j!1 skolem-const-decl "nat" sigma_swap nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(sigma_sum formula-decl nil sigma nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma_split formula-decl nil sigma nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(low2 skolem-const-decl "T_low[T]" sigma_swap nil)
(k2 skolem-const-decl "int" sigma_swap nil)
(low1 skolem-const-decl "T_low[T]" sigma_swap nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(k1 skolem-const-decl "int" sigma_swap nil)
(high1 skolem-const-decl "T_high[T]" sigma_swap nil)
(sigma def-decl "real" sigma nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(>= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lowz!1 skolem-const-decl "T_low[T]" sigma_swap nil)
(integer nonempty-type-from-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected_domain formula-decl nil sigma_swap nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(T_pred const-decl "[int -> boolean]" sigma_swap nil)
(T formal-subtype-decl nil sigma_swap nil)
(<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil))
shostak))
(sigma_swap_triangle 0
(sigma_swap_triangle-1 nil 3479644309
("" (skeep)
(("" (label "highge" -1)
(("" (hide "highge")
(("" (lemma "sigma_swap")
((""
(name "G"
"LAMBDA (i,j: T): IF j)
(("" (inst - "G" "high1" "high2" "low1" "low1")
(("" (lemma "sigma_restrict_eq")
((""
(inst-cp -
"LAMBDA (i: T): sigma(low1, high2, LAMBDA (j: T): G(i, j))"
"LAMBDA (i: T): sigma(i, high2, LAMBDA (j: T): F(i, j))"
"high1" "low1")
((""
(inst -
"LAMBDA (j: T): sigma(low1, high1, LAMBDA (i: T): G(i, j))"
"LAMBDA (j: T): sigma(low1, j, LAMBDA (i: T): F(i, j))"
"high2" "low1")
(("" (split -)
(("1" (split -)
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (decompose-equality)
(("2" (expand "restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(lemma "sigma_split")
(("2"
(inst
-
"LAMBDA (j: T): G(x!1, j)"
"high2"
"low1"
"x!1-1")
(("2"
(assert)
(("2"
(split -)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst
-
"LAMBDA (j: T): G(x!1, j)"
"LAMBDA (j: T): 0"
"x!1-1"
"low1")
(("1"
(split -1)
(("1"
(replace -1)
(("1"
(lemma
"sigma_zero")
(("1"
(inst?)
(("1"
(replace
-1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
4)
(("1"
(decompose-equality)
(("1"
(expand
"restrict")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(replace
-3
+
:dir
rl)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 4)
(("2"
(decompose-equality)
(("2"
(expand
"restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(replace
-2
+
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "sigma" + 2)
(("2"
(assert)
(("2"
(lemma "sigma_zero")
(("2"
(inst
-
"high2"
"low1")
(("2"
(replace
-1
+
:dir
rl)
(("2"
(lemma
"sigma_restrict_eq")
(("2"
(inst?)
(("2"
(assert)
(("2"
(decompose-equality)
(("2"
(expand
"restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(replace
-3
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (hide -1)
(("2" (decompose-equality)
(("2" (expand "restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(lemma "sigma_split")
(("2"
(inst
-
"LAMBDA (i: T): G(i, x!1)"
"high1"
"low1"
"x!1")
(("2"
(assert)
(("2"
(split -)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst
-
"LAMBDA (i: T): G(i, x!1)"
"LAMBDA (i: T): 0"
"high1"
"1+x!1")
(("1"
(split -)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"sigma_zero")
(("1"
(inst?)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(assert)
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide
4)
(("1"
(decompose-equality)
(("1"
(expand
"restrict")
(("1"
(lift-if)
(("1"
(ground)
(("1"
(replace
-1
:dir
rl)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(decompose-equality)
(("2"
(expand
"restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(replace
-1
:dir
rl)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(reveal "highge")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sigma_swap formula-decl nil sigma_swap nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma nil)
(T_low type-eq-decl nil sigma nil)
(sigma def-decl "real" sigma nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma_nat application-judgement "nat" sigma_swap nil)
(sigma_nnreal application-judgement "nnreal" sigma_swap nil)
(sigma_zero formula-decl nil sigma nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_split formula-decl nil sigma nil)
(restrict const-decl "[T -> real]" sigma nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_restrict_eq formula-decl nil sigma nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(T_pred const-decl "[int -> boolean]" sigma_swap nil)
(T formal-subtype-decl nil sigma_swap nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.41Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
