|
(axiomatic
(inference_tree?_TCC1 0
(inference_tree?_TCC1-1 nil 3399608346 ("" (termination-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC2 0
(inference_tree?_TCC2-1 nil 3399608346 ("" (subtype-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC3 0
(inference_tree?_TCC3-1 nil 3399608346 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
(S const-decl "Stm" axiomatic nil))
nil))
(inference_tree?_TCC4 0
(inference_tree?_TCC4-1 nil 3399608883 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
(S const-decl "Stm" axiomatic nil))
nil))
(inference_tree?_TCC5 0
(inference_tree?_TCC5-1 nil 3399608883 ("" (subtype-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC6 0
(inference_tree?_TCC6-1 nil 3399608883 ("" (subtype-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC7 0
(inference_tree?_TCC7-1 nil 3399608883 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
(S const-decl "Stm" axiomatic nil))
nil))
(inference_tree?_TCC8 0
(inference_tree?_TCC8-1 nil 3399608883 ("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
(S const-decl "Stm" axiomatic nil))
nil))
(inference_tree?_TCC9 0
(inference_tree?_TCC9-1 nil 3399608883 ("" (subtype-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC10 0
(inference_tree?_TCC10-1 nil 3399608883
("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil)
(S const-decl "Stm" axiomatic nil))
nil))
(inference_tree?_TCC11 0
(inference_tree?_TCC11-1 nil 3399608883 ("" (subtype-tcc) nil nil)
((S const-decl "Stm" axiomatic nil)) nil))
(inference_tree?_TCC12 0
(inference_tree?_TCC12-1 nil 3399608883
("" (termination-tcc) nil nil)
((<< adt-def-decl "(strict_well_founded?[tree])" axiomatic nil))
nil))
(inference_tree_TCC1 0
(inference_tree_TCC1-1 nil 3399608346
("" (expand "inference_tree?")
(("" (expand "S")
(("" (expand "P") (("" (expand "Q") (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((S const-decl "Stm" axiomatic nil)
(Q const-decl "Predicate" axiomatic nil)
(P const-decl "Predicate" axiomatic nil)
(inference_tree? def-decl "bool" axiomatic nil))
nil))
(wlp_is_precondition 0
(wlp_is_precondition-1 nil 3399619747
("" (skosimp)
(("" (expand "wlp")
(("" (expand "|=")
(("" (skosimp*)
(("" (inst - "s1!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((wlp const-decl "bool" axiomatic nil)
(State nonempty-type-eq-decl nil State nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(V formal-nonempty-type-decl nil axiomatic nil)
(\|= const-decl "bool" axiomatic nil))
shostak))
(wlp_is_weakest 0
(wlp_is_weakest-1 nil 3399619791
("" (skosimp*)
(("" (expand "|>")
(("" (skosimp)
(("" (expand "|=")
(("" (expand "wlp")
(("" (skosimp)
(("" (inst - "s!1" "s1!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((\|> const-decl "bool" axiomatic nil)
(\|= const-decl "bool" axiomatic nil)
(State nonempty-type-eq-decl nil State nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(V formal-nonempty-type-decl nil axiomatic nil)
(wlp const-decl "bool" axiomatic nil))
shostak))
(soundness 0
(soundness-1 nil 3399608945
("" (expand "|-")
(("" (case "forall (t:inference_tree): |=(H(t))")
(("1" (skosimp)
(("1" (skosimp)
(("1" (inst - "t!1")
(("1" (replace -2) (("1" (propax) nil nil)) nil)) nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "t")
(("1" (typepred "t!1") (("1" (propax) nil nil)) nil)
("2" (skolem + ("HH"))
(("2" (flatten)
(("2" (expand "|=")
(("2" (skosimp)
(("2" (expand "H")
(("2" (expand "inference_tree?")
(("2" (flatten)
(("2" (expand "assign")
(("2" (expand "Q")
(("2" (expand "P")
(("2"
(expand "S")
(("2"
(replace -2 -3 rl)
(("2"
(assert)
(("2"
(hide -2)
(("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(skosimp)
(("2"
(expand "tr")
(("2"
(expand "step")
(("2"
(expand "tr")
(("2"
(prop)
(("2"
(decompose-equality)
(("2"
(replace -1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem + ("HH"))
(("3" (flatten)
(("3" (expand "|=")
(("3" (skosimp)
(("3" (expand "inference_tree?")
(("3" (flatten)
(("3" (expand "H")
(("3" (expand "Q")
(("3" (expand "P")
(("3"
(rewrite "SS_deterministic" -4 :dir rl)
(("3"
(skosimp)
(("3"
(expand "tr")
(("3"
(expand "step")
(("3"
(assert)
(("3"
(expand "S")
(("3"
(assert)
(("3"
(expand "tr")
(("3"
(prop)
(("3"
(decompose-equality)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (skolem + ("HH" "T1" "T2"))
(("4" (flatten)
(("4" (expand "inference_tree?" -3)
(("4" (flatten)
(("4" (expand "H" 1)
(("4" (expand "|=")
(("4" (skosimp)
(("4" (replace -6)
(("4" (replace -7)
(("4" (hide -6 -7)
(("4"
(expand "S" (-4 -5))
(("4"
(expand "P")
(("4"
(expand "Q")
(("4"
(replace -6)
(("4"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("4"
(skosimp)
(("4"
(expand "S")
(("4"
(lemma
"tr_split"
("k"
"n!1"
"S1"
"S1(HH`2)"
"S2"
"S2(HH`2)"
"s0"
"s!1"
"s2"
"s1!1"))
(("4"
(case-replace
"Sequence(S1(HH`2), S2(HH`2))=HH`2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(replace -8)
(("1"
(replace -9)
(("1"
(replace -11)
(("1"
(replace
-12)
(("1"
(hide
-7
-8
-9
-10
-11
-12
-1)
(("1"
(inst
-
"s!1"
"s1!2")
(("1"
(replace
-6)
(("1"
(split
-4)
(("1"
(inst
-
"s1!2"
"s1!1")
(("1"
(replace
-1)
(("1"
(split
-5)
(("1"
(propax)
nil
nil)
("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst
+
"k2!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst
+
"k1!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(decompose-equality)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (skolem + ("HH" "T1" "T2"))
(("5" (flatten)
(("5" (expand "inference_tree?" -3)
(("5" (flatten)
(("5" (assert)
(("5" (expand "S")
(("5" (expand "P")
(("5" (expand "Q")
(("5" (expand "|=")
(("5" (expand "H" 1)
(("5"
(skosimp)
(("5"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("5"
(skosimp)
(("5"
(replace -8)
(("5"
(replace -9)
(("5"
(replace -10)
(("5"
(replace -11)
(("5"
(hide
-6
-7
-8
-9
-10
-11)
(("5"
(inst - "s!1" "s1!1")
(("5"
(inst - "s!1" "s1!1")
(("5"
(expand "&")
(("5"
(replace -6)
(("5"
(expand "~")
(("5"
(case-replace
"B(b(HH`2))(s!1)")
(("1"
(split -2)
(("1"
(propax)
nil
nil)
("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst
+
"n!1-1")
(("1"
(expand
"tr"
-6)
(("1"
(expand
"step")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"tr")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1)
(("2"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst
+
"n!1-1")
(("1"
(expand
"tr"
-5)
(("1"
(expand
"step")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"tr")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(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))
nil)
("6" (assert)
(("6" (skolem + ("HH" "T1"))
(("6" (flatten)
(("6" (copy -2)
(("6" (expand "inference_tree?" -1)
(("6" (flatten)
(("6" (assert)
(("6" (expand "H" 1)
(("6" (expand "|=")
(("6" (skosimp)
(("6"
(expand "S")
(("6"
(expand "P")
(("6"
(expand "Q")
(("6"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("6"
(skosimp)
(("6"
(replace -3)
(("6"
(replace -4)
(("6"
(replace -5)
(("6"
(hide -3 -4 -5)
(("6"
(expand "&")
(("6"
(expand "~")
(("6"
(lemma
"NAT_induction"
("p"
"lambda (k: nat): FORALL (x, y: State):
HH`1(x) AND tr(k)(I(HH`2, x), T(y)) => NOT B(b(HH`2))(y) AND HH`1(y)"))
(("1"
(split -1)
(("1"
(inst
-
"n!1")
(("1"
(inst
-
"s!1"
"s1!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
-2
-5
-6
-7
2)
(("2"
(skosimp*)
(("2"
(expand
"tr"
-3)
(("2"
(expand
"step"
-3)
(("2"
(assert)
(("2"
(case-replace
"j!1=0")
(("2"
(assert)
(("2"
(expand
"tr"
-3)
(("2"
(expand
"step"
-3)
(("2"
(case-replace
"j!1 - 1 = 0")
(("2"
(assert)
(("2"
(case-replace
"B(b(HH`2))(x!1)")
(("1"
(lemma
"tr_split"
("k"
"j!1-2"
"S1"
"S1(HH`2)"
"S2"
"HH`2"
"s0"
"x!1"
"s2"
"y!1"))
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst
-
"k2!1")
(("1"
(assert)
(("1"
(inst
-
"s1!2"
"y!1")
(("1"
(replace
-2)
(("1"
(inst
-
"x!1"
"s1!2")
(("1"
(replace
-4)
(("1"
(replace
-6)
(("1"
(split
-10)
(("1"
(replace
-1)
(("1"
(propax)
nil
nil))
nil)
("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst
+
"k1!1")
(("2"
(replace
-9)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"tr"
-3)
(("2"
(expand
"step"
-3)
(("2"
(expand
"tr"
-3)
(("2"
(prop)
(("1"
(copy
-3)
(("1"
(decompose-equality)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(decompose-equality)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("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)
("7" (skolem + ("HH" "T1"))
(("7" (flatten)
(("7" (expand "|=")
(("7" (skosimp)
(("7" (expand "H" -3)
(("7" (expand "H" -4)
(("7" (expand "H" 1)
(("7" (expand "inference_tree?" -2)
(("7" (flatten)
(("7" (replace -2)
(("7"
(inst - "s!1" "s1!1")
(("7"
(expand "S")
(("7"
(replace -3 * rl)
(("7"
(expand "P")
(("7"
(expand "Q")
(("7"
(assert)
(("7"
(expand "|>")
(("7"
(inst - "s!1")
(("7"
(assert)
(("7"
(assert)
(("7"
(inst - "s1!1")
(("7"
(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))
nil))
nil)
((H def-decl "Hoare" axiomatic nil)
(Hoare nonempty-type-eq-decl nil axiomatic nil)
(\|= const-decl "bool" axiomatic nil) (Stm type-decl nil Stm nil)
(Predicate nonempty-type-eq-decl nil axiomatic nil)
(State nonempty-type-eq-decl nil State nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(V formal-nonempty-type-decl nil axiomatic nil)
(inference_tree nonempty-type-eq-decl nil axiomatic nil)
(inference_tree? def-decl "bool" axiomatic nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(tree type-decl nil axiomatic nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(tree_induction formula-decl nil axiomatic nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(assign const-decl "bool" axiomatic nil)
(P const-decl "Predicate" axiomatic nil)
(step def-decl "[Config]" sos nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Config type-decl nil sos nil)
(T? adt-recognizer-decl "[Config -> boolean]" sos nil)
(s1 adt-accessor-decl "[(T?) -> State[V]]" sos nil)
(T adt-constructor-decl "[State[V] -> (T?)]" sos nil)
(assign const-decl "State" State nil)
(Assign? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(x adt-accessor-decl "[(Assign?) -> V]" Stm nil)
(AExp type-decl nil AExp nil)
(A def-decl "[State -> int]" AExp nil)
(a adt-accessor-decl "[(Assign?) -> AExp[V]]" Stm nil)
(tr def-decl "bool" sos nil)
(SS_deterministic formula-decl nil sos nil)
(S const-decl "Stm" axiomatic nil)
(Q const-decl "Predicate" axiomatic nil)
(tr_split formula-decl nil sos nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Sequence? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(Conditional? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(While? adt-recognizer-decl "[Stm -> boolean]" Stm nil)
(S1 shared-adt-accessor-decl
"[{x: Stm | Sequence?(x) OR Conditional?(x) OR While?(x)} -> Stm]"
Stm nil)
(S2 shared-adt-accessor-decl
"[{x: Stm | Sequence?(x) OR Conditional?(x)} -> Stm]" Stm nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Stm_Sequence_extensionality formula-decl nil Stm nil)
(HH skolem-const-decl "Hoare" axiomatic nil)
(Sequence adt-constructor-decl "[[Stm, Stm] -> (Sequence?)]" Stm
nil)
(b shared-adt-accessor-decl
"[{x: Stm | Conditional?(x) OR While?(x)} -> BExp[V]]" Stm nil)
(B def-decl "[State -> bool]" BExp nil)
(BExp type-decl nil BExp nil)
(n!1 skolem-const-decl "nat" axiomatic nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(~ const-decl "bool" axiomatic nil)
(& const-decl "bool" axiomatic nil)
(I adt-constructor-decl "[[Stm[V], State[V]] -> (I?)]" sos nil)
(I? adt-recognizer-decl "[Config -> boolean]" sos nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(NAT_induction formula-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(\|> const-decl "bool" axiomatic nil)
(\|- const-decl "bool" axiomatic nil))
shostak))
(completeness 0
(completeness-1 nil 3399619607
("" (case "FORALL (Q: Predicate, S: Stm): |-(wlp(S,Q), S, Q)")
(("1" (skosimp)
(("1" (inst - "Q!1" "S!1")
(("1" (lemma "wlp_is_weakest" ("P" "P!1" "S" "S!1" "Q" "Q!1"))
(("1" (assert)
(("1" (hide -3)
(("1" (expand "|-")
(("1" (skosimp)
(("1" (inst + "cons((P!1, S!1, Q!1),t!1)")
(("1" (expand "H" 1) (("1" (propax) nil nil)) nil)
("2" (typepred "t!1")
(("2" (expand "inference_tree?" 1)
(("2" (replace -3)
(("2" (expand "S")
(("2" (expand "P")
(("2"
(expand "Q")
(("2"
(expand "|>")
(("2" (skosimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (induct "S")
(("1" (skolem + ("x!1" "a!1"))
(("1" (skosimp)
(("1" (expand "|-")
(("1"
(inst +
"ass((wlp(Assign(x!1, a!1), Q!1), Assign(x!1, a!1), Q!1))")
(("1" (expand "H") (("1" (propax) nil nil)) nil)
("2" (expand "inference_tree?")
(("2" (assert)
(("2" (expand "S")
(("2" (expand "Q")
(("2" (expand "P")
(("2" (expand "wlp")
(("2" (apply-extensionality :hide? t)
(("2"
(case-replace
"assign(x!1, a!1)(Q!1)(x!2)")
(("1"
(skosimp)
(("1"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("1"
(skosimp)
(("1"
(expand "tr")
(("1"
(expand "step")
(("1"
(expand "tr")
(("1"
(prop)
(("1"
(decompose-equality)
(("1"
(expand "assign" -3)
(("1"
(replace -1)
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1)
(("2"
(assert)
(("2"
(expand "assign" 1)
(("2"
(inst
-
"assign(x!1, A(a!1))(x!2)")
(("2"
(assert)
(("2"
(rewrite
"SS_deterministic"
*
:dir
rl)
(("2"
(inst + "1")
(("2"
(expand "tr")
(("2"
(expand "step")
(("2"
(expand "tr")
(("2"
(propax)
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" (skosimp)
(("2" (expand "|-")
(("2" (inst + "skip((wlp(Skip, Q!1), Skip, Q!1))")
(("1" (expand "H") (("1" (propax) nil nil)) nil)
("2" (expand "inference_tree?")
(("2" (expand "S")
(("2" (expand "P")
(("2" (expand "Q")
(("2" (expand "wlp")
(("2" (apply-extensionality :hide? t)
(("2" (case-replace "Q!1(x!1)")
(("1" (skosimp)
(("1"
(rewrite "SS_deterministic" * :dir rl)
(("1"
(skosimp)
(("1"
(expand "tr")
(("1"
(expand "step")
(("1"
(expand "tr")
(("1"
(prop)
(("1"
(decompose-equality)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(inst - "x!1")
(("2"
(split)
(("1" (propax) nil nil)
("2"
(rewrite
"SS_deterministic"
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.48Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Entwicklung einer Software für die statische Quellcodeanalyse
|
