\settings { "#Proof-Settings-Config-File #Sat Jan 10 16:24:40 CET 2009 [General]SoundNotification=true [DecisionProcedure]SmtBenchmarkArchiving=false [View]FontIndex=4 [StrategyProperty]METHOD_OPTIONS_KEY=METHOD_EXPAND [StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF [StrategyProperty]LOOP_OPTIONS_KEY=LOOP_INVARIANT [StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF [StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF [SimultaneousUpdateSimplifier]DeleteEffectLessLocations=true [StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS [StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_NONE [General]SuggestiveVarNames=false [View]ShowWholeTaclet=false [General]ProofAssistant=false [View]MaxTooltipLines=40 [General]DnDDirectionSensitive=true [SimultaneousUpdateSimplifier]EagerSimplification=true [General]StupidMode=true [Strategy]Timeout=-1 [Strategy]MaximumNumberOfAutomaticApplications=8000 [Libraries]Default=acc.key-false, stringRules.key-false, deprecatedRules.key-false [StrategyProperty]QUERY_OPTIONS_KEY=QUERY_NONE [Choice]DefaultChoices=transactions-transactions\:transactionsOn , programRules-programRules\:Java , initialisation-initialisation\:disableStaticInitialisation , transactionAbort-transactionAbort\:abortOn , throughout-throughout\:toutOn , intRules-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:on , nullPointerPolicy-nullPointerPolicy\:nullCheck [DecisionProcedure]SmtZipProblemDir=false [DecisionProcedureForTest]=Cogent [Model]Source=1 [Choice]Choices=transactions-transactions\:transactionsOff-transactions\:transactionsOn , programRules-programRules\:ODL-programRules\:Java , throughout-throughout\:toutOff-throughout\:toutOn , initialisation-initialisation\:disableStaticInitialisation-initialisation\:enableStaticInitialisation , transactionAbort-transactionAbort\:abortOff-transactionAbort\:abortOn , intRules-intRules\:arithmeticSemanticsCheckingOF-intRules\:javaSemantics-intRules\:arithmeticSemanticsIgnoringOF , assertions-assertions\:safe-assertions\:off-assertions\:on , nullPointerPolicy-nullPointerPolicy\:noNullCheck-nullPointerPolicy\:nullCheck [DecisionProcedure]SmtUseQuantifiers=true [View]HideIntermediateProofsteps=false [DecisionProcedure]=SIMPLIFY [General]OuterRenaming=false [Strategy]ActiveStrategy=JavaCardDLStrategy [StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED " } // // UniversitĂ?t Karlsruhe // Institut fĂ?r Theoretische Informatik // Prof. Dr. Bernhard Beckert // Mattias Ulbrich // // Formale Systeme WS 08/09 // Uebungsblatt 7 - Aufgabe 3 // This a problem file to be used with the KeY verification tool. // // Copyright (C) 2008 Universitaet Karlsruhe, Germany, // Natuerliche Zahlen als Sorte \sorts { N; } // Addition, Nachfolgerfunktion und Null als Funktionen in der Signatur \functions { N Add(N,N); N S(N); N Null; } // Es folgt das Regelschema fuer die Induktion. In dieser // Regel treten einige "Dinge" auf, die spaeter eingesetzt werden // koennen. \schemaVariables { \formula phi; \variables N n; } // Das ist die Induktionsregel. \rules { INDUCTION { \find( ==> \forall n; phi ) "ind. base" : \replacewith( ==> {\subst n;Null}phi ); "ind. step" : \replacewith( ==> \forall n; (phi -> {\subst n;S(n)}phi ) ) }; } // Das Problem: // Um zu zeigen, dass die Addition auf den natuerlichen Zahlen kommutativ ist, // genuegt diese Teildefinition der Addition. \problem { \forall N x; \forall N y; Add(x, S(y)) = S(Add(x, y)) & \forall N x; \forall N y; Add(S(x), y) = S(Add(x, y)) -> \forall N x; \forall N y; Add(x, y) = Add(y, x) } \proof { (keyLog "0" (keyUser "beckert" ) (keyVersion "3f63b25cb9e5cc5bfa0575ff7bf2882202cfe4cc")) (branch "dummy ID" (rule "impRight" (formula "1") (userinteraction)) (rule "andLeft" (formula "1") (userinteraction)) (rule "INDUCTION" (formula "3") (userinteraction)) (branch " ind. base" (rule "INDUCTION" (formula "3") (userinteraction)) (branch " ind. base" (rule "eqClose" (formula "3") (userinteraction)) (rule "closeTrue" (formula "3") (userinteraction)) ) (branch " ind. step" (rule "allRight" (formula "3") (inst "sk=y_0") (userinteraction)) (rule "impRight" (formula "3") (userinteraction)) (rule "instAll" (formula "4") (term "0,0") (ifseqformula "2") (userinteraction)) (rule "instAll" (formula "5") (term "0,1,0") (ifseqformula "1") (userinteraction)) (rule "applyEq" (formula "6") (term "0") (ifseqformula "1") (userinteraction)) (rule "instAll" (formula "6") (term "0,0,1") (ifseqformula "5") (userinteraction)) (rule "instAll" (formula "7") (term "1,1") (ifseqformula "1") (userinteraction)) (rule "applyEq" (formula "8") (term "1") (ifseqformula "1") (userinteraction)) (rule "applyEq" (formula "8") (term "0,0") (ifseqformula "5") (userinteraction)) (rule "eqClose" (formula "8") (userinteraction)) (rule "closeTrue" (formula "8") (userinteraction)) ) ) (branch " ind. step" (rule "allRight" (formula "3") (inst "sk=x_0") (userinteraction)) (rule "impRight" (formula "3") (userinteraction)) (rule "allRight" (formula "4") (inst "sk=y_1") (userinteraction)) (rule "instAll" (formula "4") (term "0,0,0") (ifseqformula "3") (userinteraction)) (rule "instAll" (formula "5") (term "1,0") (ifseqformula "1") (userinteraction)) (rule "applyEq" (formula "6") (term "0") (ifseqformula "1") (userinteraction)) (rule "instAll" (formula "6") (term "0,1") (ifseqformula "4") (userinteraction)) (rule "instAll" (formula "7") (term "0,1,1") (ifseqformula "1") (userinteraction)) (rule "applyEq" (formula "8") (term "1") (ifseqformula "1") (userinteraction)) (rule "instAll" (formula "8") (term "1,0,0") (ifseqformula "5") (userinteraction)) (rule "applyEq" (formula "9") (term "0,0") (ifseqformula "1") (userinteraction)) (rule "eqClose" (formula "9") (userinteraction)) (rule "closeTrue" (formula "9") (userinteraction)) ) ) }