/tmp/atelierb.tar0100664000021500002450000000015010216567201013527 0ustar cansellmodelatelierb_archive_Version_5 #DB_FILE Freek.db bdp exec sources m0 .mch sources m1 .mch sources m2 .mch sources/m0.mch0100644000021500002450000000104710216566054013052 0ustar cansellmodelMACHINE m0 PROPERTIES /* The structural inductive theorem */ !P.(P<:NATURAL & !x.(x:NATURAL&!y.(y:NATURAL&yy:P)=>x:P) => NATURAL<:P) ASSERTIONS /* it's a technical lemma used in the next one */ !n.(n:NATURAL& #x.(x:NATURAL&n*n=2*x) => #x.(x:NATURAL&n=2*x)); /* it's the difficult part of the theorem */ !(n,m).(n:NATURAL& m:NATURAL => (n*n=2*(m*m) => n=0)); /* the theorem */ !(n,m).(n:NATURAL& m:NATURAL => (n*n=2*(m*m)<=>(n=0&m=0))) END sources/m1.mch0100644000021500002450000000062510216567100013045 0ustar cansellmodelMACHINE m1 DEFINITIONS divide(n,m) ==( #k.(k:NATURAL & n=m*k)); coprime(n,m)==( !x.(x:NATURAL÷(n,x)÷(m,x)=>x=1)) ASSERTIONS /* it's a technical lemma used in the next one it's the same as the previous one using divide */ !n.(n:NATURAL& divide(n*n,2) => divide(n,2)); /* The statement */ not(#(n,m).(n:NATURAL&m:NATURAL1&n*n=2*(m*m) & coprime(n,m))) ENDsources/m2.mch0100644000021500002450000000054110216567167013060 0ustar cansellmodelMACHINE m2 DEFINITIONS divide(n,m) ==(#k.(k:NATURAL & n=m*k)); notcoprime(n,m)==(#x.(x:NATURAL÷(n,x)÷(m,x)&x/=1)) ASSERTIONS /* it's a technical lemma used in the next one */ !n.(n:NATURAL& divide(n*n,2) => divide(n,2)); /* The statement */ !(n,m).(n:NATURAL&m:NATURAL1&n*n=2*(m*m) => notcoprime(n,m)) ENDbdp/0040775000021500002450000000000010216567176011140 5ustar cansellmodelbdp/src/0040770000021500002450000000000010216565671011720 5ustar cansellmodelbdp/src/m0.mch0100664000021500002450000000126110216566070012721 0ustar cansellmodelMACHINE m0 PROPERTIES /* The structural inductive theorem */ ! P . ( P <: NATURAL & ! x . ( x : NATURAL & ! y . ( y : NATURAL & y < x => y : P ) => x : P ) => NATURAL <: P ) ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & # x . ( x : NATURAL & n * n = 2 * x ) => # x . ( x : NATURAL & n = 2 * x ) ) ; /* it's the difficult part of the theorem */ ! ( n , m ) . ( n : NATURAL & m : NATURAL => ( n * n = 2 * ( m * m ) => n = 0 ) ) ; /* the theorem */ ! ( n , m ) . ( n : NATURAL & m : NATURAL => ( n * n = 2 * ( m * m ) <=> ( n = 0 & m = 0 ) ) ) END bdp/src/m1.mch0100664000021500002450000000063610216564625012733 0ustar cansellmodelMACHINE m1 ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & ( # k . ( k : NATURAL & n * n = 2 * k ) ) => ( # k . ( k : NATURAL & n = 2 * k ) ) ) ; not ( # ( n , m ) . ( n : NATURAL & m : NATURAL1 & n * n = 2 * ( m * m ) & ( ! x . ( x : NATURAL & ( # k . ( k : NATURAL & n = x * k ) ) & ( # k . ( k : NATURAL & m = x * k ) ) => x = 1 ) ) ) ) END bdp/src/m2.mch0100664000021500002450000000062510216565346012733 0ustar cansellmodelMACHINE m2 ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & ( # k . ( k : NATURAL & n * n = 2 * k ) ) => ( # k . ( k : NATURAL & n = 2 * k ) ) ) ; ! ( n , m ) . ( n : NATURAL & m : NATURAL1 & n * n = 2 * ( m * m ) => ( # x . ( x : NATURAL & ( # k . ( k : NATURAL & n = x * k ) ) & ( # k . ( k : NATURAL & m = x * k ) ) & x /= 1 ) ) ) END bdp/.lib0100664000021500002450000000000010124771160011656 0ustar cansellmodelbdp/m0.nf0100664000021500002450000001013210216566070011763 0ustar cansellmodelNormalised( THEORY MagicNumberX IS MagicNumber(Machine(m0))==(3.5) END & THEORY UpperLevelX IS First_Level(Machine(m0))==(Machine(m0)); Level(Machine(m0))==(0) END & THEORY LoadedStructureX IS Machine(m0) END & THEORY ListSeesX IS List_Sees(Machine(m0))==(?) END & THEORY ListUsesX IS List_Uses(Machine(m0))==(?) END & THEORY ListIncludesX IS Inherited_List_Includes(Machine(m0))==(?); List_Includes(Machine(m0))==(?) END & THEORY ListPromotesX IS List_Promotes(Machine(m0))==(?) END & THEORY ListExtendsX IS List_Extends(Machine(m0))==(?) END & THEORY ListVariablesX IS External_Context_List_Variables(Machine(m0))==(?); Context_List_Variables(Machine(m0))==(?); Abstract_List_Variables(Machine(m0))==(?); Local_List_Variables(Machine(m0))==(?); List_Variables(Machine(m0))==(?); External_List_Variables(Machine(m0))==(?) END & THEORY ListVisibleVariablesX IS Inherited_List_VisibleVariables(Machine(m0))==(?); Abstract_List_VisibleVariables(Machine(m0))==(?); External_List_VisibleVariables(Machine(m0))==(?); Expanded_List_VisibleVariables(Machine(m0))==(?); List_VisibleVariables(Machine(m0))==(?); Internal_List_VisibleVariables(Machine(m0))==(?) END & THEORY ListInvariantX IS Gluing_Seen_List_Invariant(Machine(m0))==(btrue); Gluing_List_Invariant(Machine(m0))==(btrue); Expanded_List_Invariant(Machine(m0))==(btrue); Abstract_List_Invariant(Machine(m0))==(btrue); Context_List_Invariant(Machine(m0))==(btrue); List_Invariant(Machine(m0))==(btrue) END & THEORY ListAssertionsX IS Expanded_List_Assertions(Machine(m0))==(btrue); Abstract_List_Assertions(Machine(m0))==(btrue); Context_List_Assertions(Machine(m0))==(btrue); List_Assertions(Machine(m0))==(!n.(n: NATURAL & #x.(x: NATURAL & n*n = 2*x) => #x.(x: NATURAL & n = 2*x));!(n,m).(n: NATURAL & m: NATURAL => (n*n = 2*(m*m) => n = 0));!(n,m).(n: NATURAL & m: NATURAL => n*n = 2*(m*m) <=> (n = 0 & m = 0))) END & THEORY ListInitialisationX IS Expanded_List_Initialisation(Machine(m0))==(skip); Context_List_Initialisation(Machine(m0))==(skip); List_Initialisation(Machine(m0))==(skip) END & THEORY ListParametersX IS List_Parameters(Machine(m0))==(?) END & THEORY ListInstanciatedParametersX END & THEORY ListConstraintsX IS List_Context_Constraints(Machine(m0))==(btrue); List_Constraints(Machine(m0))==(btrue) END & THEORY ListOperationsX IS Internal_List_Operations(Machine(m0))==(?); List_Operations(Machine(m0))==(?) END & THEORY ListInputX END & THEORY ListOutputX END & THEORY ListHeaderX END & THEORY ListPreconditionX END & THEORY ListSubstitutionX END & THEORY ListConstantsX IS List_Valuable_Constants(Machine(m0))==(?); Inherited_List_Constants(Machine(m0))==(?); List_Constants(Machine(m0))==(?) END & THEORY ListSetsX IS Context_List_Enumerated(Machine(m0))==(?); Context_List_Defered(Machine(m0))==(?); Context_List_Sets(Machine(m0))==(?); List_Valuable_Sets(Machine(m0))==(?); Inherited_List_Enumerated(Machine(m0))==(?); Inherited_List_Defered(Machine(m0))==(?); Inherited_List_Sets(Machine(m0))==(?); List_Enumerated(Machine(m0))==(?); List_Defered(Machine(m0))==(?); List_Sets(Machine(m0))==(?) END & THEORY ListHiddenConstantsX IS Abstract_List_HiddenConstants(Machine(m0))==(?); Expanded_List_HiddenConstants(Machine(m0))==(?); List_HiddenConstants(Machine(m0))==(?); External_List_HiddenConstants(Machine(m0))==(?) END & THEORY ListPropertiesX IS Abstract_List_Properties(Machine(m0))==(btrue); Context_List_Properties(Machine(m0))==(btrue); Inherited_List_Properties(Machine(m0))==(btrue); List_Properties(Machine(m0))==(!P.(P <: NATURAL & !x.(x: NATURAL & !y.(y: NATURAL & y y: P) => x: P) => NATURAL <: P)) END & THEORY ListSeenInfoX END & THEORY ListOfIdsX IS List_Of_Ids(Machine(m0)) == (? | ? | ? | ? | ? | ? | ? | ? | m0); List_Of_HiddenCst_Ids(Machine(m0)) == (? | ?); List_Of_VisibleCst_Ids(Machine(m0)) == (?); List_Of_VisibleVar_Ids(Machine(m0)) == (? | ?); List_Of_Ids_SeenBNU(Machine(m0)) == (?: ?) END & THEORY TCIntRdX IS predB0 == OK; extended_sees == KO; B0check_tab == KO; local_op == OK; abstract_constants_visible_in_values == KO END ) bdp/m0.po0100664000021500002450000000412710216566071012006 0ustar cansellmodelTHEORY ProofList IS _f(1) & AssertionLemmas.5,(_f(11) & _f(9) => _f(12)); _f(1) & AssertionLemmas.4,(_f(8) & _f(9) => _f(10)); _f(1) & AssertionLemmas.3,(_f(8) & _f(9) => _f(7)); _f(1) & AssertionLemmas.2,(_f(5) & _f(6) => _f(7)); _f(1) & AssertionLemmas.1,(_f(2) & _f(3) => _f(4)) END & THEORY Formulas IS ("`Component properties'" & !P.(P: POW(NATURAL) & !x.(x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & y+1<=x => y: P) => x: P) => NATURAL: POW(P))); ("`Local hypotheses'" & n: INTEGER & 0<=n & x: INTEGER & 0<=x & n*n = 2*x); "`Check assertion (!n.(n: NATURAL & #x.(x: NATURAL & n*n = 2*x) => #x.(x: NATURAL & n = 2*x))) deduction - ref 3.2, 4.2, 5.3'"; (#x.(x: INTEGER & 0<=x & n = 2*x)); ("`Local hypotheses'" & !n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)) & n: INTEGER & 0<=n & m: INTEGER & 0<=m & n*n = 2*(m*m)); "`Check assertion (!(n,m).(n: NATURAL & m: NATURAL => (n*n = 2*(m*m) => n = 0))) deduction - ref 3.2, 4.2, 5.3'"; (n = 0); ("`Local hypotheses'" & !n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)) & !(n,m$0).(n: INTEGER & 0<=n & (m$0: INTEGER & 0<=m$0) & n*n = 2*(m$0*m$0) => n = 0) & n: INTEGER & 0<=n & m: INTEGER & 0<=m & n*n = 2*(m*m)); "`Check assertion (!(n,m).(n: NATURAL & m: NATURAL => n*n = 2*(m*m) <=> (n = 0 & m = 0))) deduction - ref 3.2, 4.2, 5.3'"; (m = 0); ("`Local hypotheses'" & !n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)) & !(n,m$0).(n: INTEGER & 0<=n & (m$0: INTEGER & 0<=m$0) & n*n = 2*(m$0*m$0) => n = 0) & n: INTEGER & 0<=n & m: INTEGER & 0<=m & n = 0 & m = 0); (n*n = 2*(m*m)); ("`Component assertions'" & !n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)) & !(n,m).(n: INTEGER & 0<=n & (m: INTEGER & 0<=m) & n*n = 2*(m*m) => n = 0) & !(n,m).(n: INTEGER & 0<=n & (m: INTEGER & 0<=m) => (n*n = 2*(m*m) => n = 0 & m = 0) & (n = 0 & m = 0 => n*n = 2*(m*m)))) END & THEORY EnumerateX END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/m1.nf0100664000021500002450000001001310216564625011766 0ustar cansellmodelNormalised( THEORY MagicNumberX IS MagicNumber(Machine(m1))==(3.5) END & THEORY UpperLevelX IS First_Level(Machine(m1))==(Machine(m1)); Level(Machine(m1))==(0) END & THEORY LoadedStructureX IS Machine(m1) END & THEORY ListSeesX IS List_Sees(Machine(m1))==(?) END & THEORY ListUsesX IS List_Uses(Machine(m1))==(?) END & THEORY ListIncludesX IS Inherited_List_Includes(Machine(m1))==(?); List_Includes(Machine(m1))==(?) END & THEORY ListPromotesX IS List_Promotes(Machine(m1))==(?) END & THEORY ListExtendsX IS List_Extends(Machine(m1))==(?) END & THEORY ListVariablesX IS External_Context_List_Variables(Machine(m1))==(?); Context_List_Variables(Machine(m1))==(?); Abstract_List_Variables(Machine(m1))==(?); Local_List_Variables(Machine(m1))==(?); List_Variables(Machine(m1))==(?); External_List_Variables(Machine(m1))==(?) END & THEORY ListVisibleVariablesX IS Inherited_List_VisibleVariables(Machine(m1))==(?); Abstract_List_VisibleVariables(Machine(m1))==(?); External_List_VisibleVariables(Machine(m1))==(?); Expanded_List_VisibleVariables(Machine(m1))==(?); List_VisibleVariables(Machine(m1))==(?); Internal_List_VisibleVariables(Machine(m1))==(?) END & THEORY ListInvariantX IS Gluing_Seen_List_Invariant(Machine(m1))==(btrue); Gluing_List_Invariant(Machine(m1))==(btrue); Expanded_List_Invariant(Machine(m1))==(btrue); Abstract_List_Invariant(Machine(m1))==(btrue); Context_List_Invariant(Machine(m1))==(btrue); List_Invariant(Machine(m1))==(btrue) END & THEORY ListAssertionsX IS Expanded_List_Assertions(Machine(m1))==(btrue); Abstract_List_Assertions(Machine(m1))==(btrue); Context_List_Assertions(Machine(m1))==(btrue); List_Assertions(Machine(m1))==(!n.(n: NATURAL & #k.(k: NATURAL & n*n = 2*k) => #k.(k: NATURAL & n = 2*k));not(#(n,m).(n: NATURAL & m: NATURAL1 & n*n = 2*(m*m) & !x.(x: NATURAL & #k.(k: NATURAL & n = x*k) & #k.(k: NATURAL & m = x*k) => x = 1)))) END & THEORY ListInitialisationX IS Expanded_List_Initialisation(Machine(m1))==(skip); Context_List_Initialisation(Machine(m1))==(skip); List_Initialisation(Machine(m1))==(skip) END & THEORY ListParametersX IS List_Parameters(Machine(m1))==(?) END & THEORY ListInstanciatedParametersX END & THEORY ListConstraintsX IS List_Context_Constraints(Machine(m1))==(btrue); List_Constraints(Machine(m1))==(btrue) END & THEORY ListOperationsX IS Internal_List_Operations(Machine(m1))==(?); List_Operations(Machine(m1))==(?) END & THEORY ListInputX END & THEORY ListOutputX END & THEORY ListHeaderX END & THEORY ListPreconditionX END & THEORY ListSubstitutionX END & THEORY ListConstantsX IS List_Valuable_Constants(Machine(m1))==(?); Inherited_List_Constants(Machine(m1))==(?); List_Constants(Machine(m1))==(?) END & THEORY ListSetsX IS Context_List_Enumerated(Machine(m1))==(?); Context_List_Defered(Machine(m1))==(?); Context_List_Sets(Machine(m1))==(?); List_Valuable_Sets(Machine(m1))==(?); Inherited_List_Enumerated(Machine(m1))==(?); Inherited_List_Defered(Machine(m1))==(?); Inherited_List_Sets(Machine(m1))==(?); List_Enumerated(Machine(m1))==(?); List_Defered(Machine(m1))==(?); List_Sets(Machine(m1))==(?) END & THEORY ListHiddenConstantsX IS Abstract_List_HiddenConstants(Machine(m1))==(?); Expanded_List_HiddenConstants(Machine(m1))==(?); List_HiddenConstants(Machine(m1))==(?); External_List_HiddenConstants(Machine(m1))==(?) END & THEORY ListPropertiesX IS Abstract_List_Properties(Machine(m1))==(btrue); Context_List_Properties(Machine(m1))==(btrue); Inherited_List_Properties(Machine(m1))==(btrue); List_Properties(Machine(m1))==(btrue) END & THEORY ListSeenInfoX END & THEORY ListOfIdsX IS List_Of_Ids(Machine(m1)) == (? | ? | ? | ? | ? | ? | ? | ? | m1); List_Of_HiddenCst_Ids(Machine(m1)) == (? | ?); List_Of_VisibleCst_Ids(Machine(m1)) == (?); List_Of_VisibleVar_Ids(Machine(m1)) == (? | ?); List_Of_Ids_SeenBNU(Machine(m1)) == (?: ?) END & THEORY TCIntRdX IS predB0 == OK; extended_sees == KO; B0check_tab == KO; local_op == OK; abstract_constants_visible_in_values == KO END ) bdp/m1.po0100664000021500002450000000244110216564627012011 0ustar cansellmodelTHEORY ProofList IS AssertionLemmas.2,(_f(4) & _f(5) => _f(6)); AssertionLemmas.1,(_f(1) & _f(2) => _f(3)) END & THEORY Formulas IS ("`Local hypotheses'" & n: INTEGER & 0<=n & k: INTEGER & 0<=k & n*n = 2*k); "`Check assertion (!n.(n: NATURAL & #k.(k: NATURAL & n*n = 2*k) => #k.(k: NATURAL & n = 2*k))) deduction - ref 3.2, 4.2, 5.3'"; (#k.(k: INTEGER & 0<=k & n = 2*k)); ("`Local hypotheses'" & !n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k))); "`Check assertion (not(#(n,m).(n: NATURAL & m: NATURAL1 & n*n = 2*(m*m) & !x.(x: NATURAL & #k.(k: NATURAL & n = x*k) & #k.(k: NATURAL & m = x*k) => x = 1)))) deduction - ref 3.2, 4.2, 5.3'"; (not(#(n,m).(n: INTEGER & 0<=n & (m: INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m) & !x.(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) => x = 1)))); ("`Component assertions'" & !n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k)) & not(#(n,m).(n: INTEGER & 0<=n & (m: INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m) & !x.(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) => x = 1)))) END & THEORY EnumerateX END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/m2.nf0100664000021500002450000001000510216565346011771 0ustar cansellmodelNormalised( THEORY MagicNumberX IS MagicNumber(Machine(m2))==(3.5) END & THEORY UpperLevelX IS First_Level(Machine(m2))==(Machine(m2)); Level(Machine(m2))==(0) END & THEORY LoadedStructureX IS Machine(m2) END & THEORY ListSeesX IS List_Sees(Machine(m2))==(?) END & THEORY ListUsesX IS List_Uses(Machine(m2))==(?) END & THEORY ListIncludesX IS Inherited_List_Includes(Machine(m2))==(?); List_Includes(Machine(m2))==(?) END & THEORY ListPromotesX IS List_Promotes(Machine(m2))==(?) END & THEORY ListExtendsX IS List_Extends(Machine(m2))==(?) END & THEORY ListVariablesX IS External_Context_List_Variables(Machine(m2))==(?); Context_List_Variables(Machine(m2))==(?); Abstract_List_Variables(Machine(m2))==(?); Local_List_Variables(Machine(m2))==(?); List_Variables(Machine(m2))==(?); External_List_Variables(Machine(m2))==(?) END & THEORY ListVisibleVariablesX IS Inherited_List_VisibleVariables(Machine(m2))==(?); Abstract_List_VisibleVariables(Machine(m2))==(?); External_List_VisibleVariables(Machine(m2))==(?); Expanded_List_VisibleVariables(Machine(m2))==(?); List_VisibleVariables(Machine(m2))==(?); Internal_List_VisibleVariables(Machine(m2))==(?) END & THEORY ListInvariantX IS Gluing_Seen_List_Invariant(Machine(m2))==(btrue); Gluing_List_Invariant(Machine(m2))==(btrue); Expanded_List_Invariant(Machine(m2))==(btrue); Abstract_List_Invariant(Machine(m2))==(btrue); Context_List_Invariant(Machine(m2))==(btrue); List_Invariant(Machine(m2))==(btrue) END & THEORY ListAssertionsX IS Expanded_List_Assertions(Machine(m2))==(btrue); Abstract_List_Assertions(Machine(m2))==(btrue); Context_List_Assertions(Machine(m2))==(btrue); List_Assertions(Machine(m2))==(!n.(n: NATURAL & #k.(k: NATURAL & n*n = 2*k) => #k.(k: NATURAL & n = 2*k));!(n,m).(n: NATURAL & m: NATURAL1 & n*n = 2*(m*m) => #x.(x: NATURAL & #k.(k: NATURAL & n = x*k) & #k.(k: NATURAL & m = x*k) & x/=1))) END & THEORY ListInitialisationX IS Expanded_List_Initialisation(Machine(m2))==(skip); Context_List_Initialisation(Machine(m2))==(skip); List_Initialisation(Machine(m2))==(skip) END & THEORY ListParametersX IS List_Parameters(Machine(m2))==(?) END & THEORY ListInstanciatedParametersX END & THEORY ListConstraintsX IS List_Context_Constraints(Machine(m2))==(btrue); List_Constraints(Machine(m2))==(btrue) END & THEORY ListOperationsX IS Internal_List_Operations(Machine(m2))==(?); List_Operations(Machine(m2))==(?) END & THEORY ListInputX END & THEORY ListOutputX END & THEORY ListHeaderX END & THEORY ListPreconditionX END & THEORY ListSubstitutionX END & THEORY ListConstantsX IS List_Valuable_Constants(Machine(m2))==(?); Inherited_List_Constants(Machine(m2))==(?); List_Constants(Machine(m2))==(?) END & THEORY ListSetsX IS Context_List_Enumerated(Machine(m2))==(?); Context_List_Defered(Machine(m2))==(?); Context_List_Sets(Machine(m2))==(?); List_Valuable_Sets(Machine(m2))==(?); Inherited_List_Enumerated(Machine(m2))==(?); Inherited_List_Defered(Machine(m2))==(?); Inherited_List_Sets(Machine(m2))==(?); List_Enumerated(Machine(m2))==(?); List_Defered(Machine(m2))==(?); List_Sets(Machine(m2))==(?) END & THEORY ListHiddenConstantsX IS Abstract_List_HiddenConstants(Machine(m2))==(?); Expanded_List_HiddenConstants(Machine(m2))==(?); List_HiddenConstants(Machine(m2))==(?); External_List_HiddenConstants(Machine(m2))==(?) END & THEORY ListPropertiesX IS Abstract_List_Properties(Machine(m2))==(btrue); Context_List_Properties(Machine(m2))==(btrue); Inherited_List_Properties(Machine(m2))==(btrue); List_Properties(Machine(m2))==(btrue) END & THEORY ListSeenInfoX END & THEORY ListOfIdsX IS List_Of_Ids(Machine(m2)) == (? | ? | ? | ? | ? | ? | ? | ? | m2); List_Of_HiddenCst_Ids(Machine(m2)) == (? | ?); List_Of_VisibleCst_Ids(Machine(m2)) == (?); List_Of_VisibleVar_Ids(Machine(m2)) == (? | ?); List_Of_Ids_SeenBNU(Machine(m2)) == (?: ?) END & THEORY TCIntRdX IS predB0 == OK; extended_sees == KO; B0check_tab == KO; local_op == OK; abstract_constants_visible_in_values == KO END ) bdp/m2.po0100664000021500002450000000241710216565350012007 0ustar cansellmodelTHEORY ProofList IS AssertionLemmas.2,(_f(4) & _f(5) => _f(6)); AssertionLemmas.1,(_f(1) & _f(2) => _f(3)) END & THEORY Formulas IS ("`Local hypotheses'" & n: INTEGER & 0<=n & k: INTEGER & 0<=k & n*n = 2*k); "`Check assertion (!n.(n: NATURAL & #k.(k: NATURAL & n*n = 2*k) => #k.(k: NATURAL & n = 2*k))) deduction - ref 3.2, 4.2, 5.3'"; (#k.(k: INTEGER & 0<=k & n = 2*k)); ("`Local hypotheses'" & !n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k)) & n: INTEGER & 0<=n & m: INTEGER & 0<=m & not(m = 0) & n*n = 2*(m*m)); "`Check assertion (!(n,m).(n: NATURAL & m: NATURAL1 & n*n = 2*(m*m) => #x.(x: NATURAL & #k.(k: NATURAL & n = x*k) & #k.(k: NATURAL & m = x*k) & x/=1))) deduction - ref 3.2, 4.2, 5.3'"; (#x.(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) & not(x = 1))); ("`Component assertions'" & !n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k)) & !(n,m).(n: INTEGER & 0<=n & (m: INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m) => #x.(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) & not(x = 1)))) END & THEORY EnumerateX END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/Freek.db0100664000021500002450000000663410216566077012510 0ustar cansellmodel4Vy«Ìºiÿÿÿÿ œ«Ìºm«Ìºn$«ÌºhÕ ÿÿÿÿ «Ìºh  ÿÿÿÿ«ÌºgÙ ÿÿÿÿ ›«Ìºgÿÿÿÿ ˜«Ìºh  ÿÿÿÿ«Ìºo«Ìºü«ÌºÞ«Ìºß«ÌºÚ«Ìºò«Ìº«Ìºgÿÿÿÿ —«Ìº© «Ìºl» «Ìºô «Ìºl´«Ìºý «Ìº«Ìºö «Ìºl¼«Ìºv «Ìºw «Ìºm¼ !«Ìº„ «Ìºmµ !«Ìº‡ «Ìºm½ !«Ìº*%«Ìº÷ x¨ØH¸(˜ 8 h ˜ È  P¨HD@˜È”Äô `  ü , ˜ Ì!/home/cansell/B/Freek/bdp/src/home/cansell/B/Freek/bdp/expand_src/home/cansell/B/Freek/sourcesm0mchcansellm21d16b7175065f9cc39e40fc4e5c330b04384319d7e6bc55a2141c8e14cebe711m11d0d8fcd8e59a6579dea0e45ee71624300f04a7de7df87e5b215d9c204e2bbab4c87fc7322f80f9c5bc51030911a0f28724b23fd4b72960647aa9a6e0464fa3f2e8d268d4e8a58bc5f41938056a4bcfaINITIALISATION00000000000000000000000000000000 ü bdp/m1.pmi.bbt0100644000021500002450000000610710216564704012723 0ustar cansellmodelTHEORY BBTTE IS cmd(0 | cl) & gol(0 | not(#(n,m).(n : INTEGER & 0<=n & (m : INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m) & !x.(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1)))) & cmd(1 | xp) & cmd(1 | rn) & gol(1 | not(n : INTEGER & 0<=n & (m : INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m) & !x.(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))) & cmd(2 | rn) & gol(2 | not(n : INTEGER & 0<=n & (m : INTEGER & 0<=m & not(m = 0)) & n*n = 2*(m*m)) or not(!x.(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))) & cmd(3 | rd) & gol(3 | not(!x.(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))) & cmd(4 | rn) & gol(4 | #x.not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1)) & cmd(5 | ct) & gol(5 | bfalse) & cmd(6 | rn(not(#x.not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1)))) & cmd(6 | ds(!x.(x = x => not(not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))))) & cmd(6 | ph(n,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(6 | #k.(k : INTEGER & 0<=k & n*n = 2*k)) & cmd(7 | se(m*m)) & gol(7 | m*m : INTEGER) & cmd(8 | pp(rp.0)) & gol(7 | 0<=m*m) & cmd(8 | pp(rp.0)) & cmd(6 | ph(m,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(6 | #k.(k : INTEGER & 0<=k & m*m = 2*k)) & cmd(7 | rx(#k.(k : INTEGER & 0<=k & n = 2*k))) & cmd(7 | se(k*k)) & gol(7 | k*k : INTEGER) & cmd(8 | pp(rp.0)) & gol(7 | 0<=k*k) & cmd(8 | pp(rp.0)) & gol(7 | m*m = 2*(k*k)) & cmd(8 | pp(rp.0)) & cmd(6 | ph(2,!x.(x = x => not(not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))))) & cmd(6 | mh(2 : INTEGER & 0<=2 & #k.(k : INTEGER & 0<=k & n = 2*k) & #k.(k : INTEGER & 0<=k & m = 2*k) => 2 = 1)) & gol(6 | 2 : INTEGER) & cmd(7 | pp(rp.0)) & gol(6 | 0<=2) & cmd(7 | pp(rp.0)) & gol(0 | SUCCESS); cmd(0 | cl) & gol(0 | #k.(k : INTEGER & 0<=k & n = 2*k)) & cmd(1 | xp) & cmd(1 | ah(#x.(x : NATURAL & (n = 2*x or n = 2*x+1)))) & gol(1 | #x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & cmd(2 | se(n/2)) & gol(2 | n/2 : NATURAL) & cmd(3 | pp(rp.0)) & gol(2 | n = 2*(n/2) or n = 2*(n/2)+1) & cmd(3 | pp(rp.0)) & cmd(1 | rx(#x.(x : NATURAL & (n = 2*x or n = 2*x+1)))) & cmd(1 | dcs(n = 2*x or n = 2*x+1)) & gol(1 | #k.(k : INTEGER & 0<=k & 2*x = 2*k)) & cmd(2 | pp(rp.0)) & gol(1 | #k.(k : INTEGER & 0<=k & 2*x+1 = 2*k)) & cmd(2 | ah(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1))) & gol(2 | #y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & cmd(3 | se(2*x*x+2*x)) & gol(3 | 2*x*x+2*x : NATURAL) & cmd(4 | pp(rp.0)) & gol(3 | (2*x+1)*(2*x+1) = 2*(2*x*x+2*x)+1) & cmd(4 | pp(rp.0)) & cmd(2 | rx(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1))) & cmd(2 | ah(y #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(1 | #k.(k : INTEGER & 0<=k & n*n = 2*k)) & cmd(2 | se(m*m)) & gol(2 | m*m : INTEGER) & cmd(3 | pp(rp.0)) & gol(2 | 0<=m*m) & cmd(3 | pp(rp.0)) & cmd(1 | se(2)) & gol(1 | 2 : INTEGER) & cmd(2 | pp(rp.0)) & gol(1 | 0<=2) & cmd(2 | pp(rp.0)) & gol(1 | #k.(k : INTEGER & 0<=k & m = 2*k)) & cmd(2 | rx(#k.(k : INTEGER & 0<=k & n = 2*k))) & cmd(2 | ph(m,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(2 | #k.(k : INTEGER & 0<=k & m*m = 2*k)) & cmd(3 | se(k*k)) & gol(3 | k*k : INTEGER) & cmd(4 | pp(rp.0)) & gol(3 | 0<=k*k) & cmd(4 | pp(rp.0)) & gol(3 | m*m = 2*(k*k)) & cmd(4 | pp(rp.0)) & gol(1 | not(2 = 1)) & cmd(2 | pp(rp.0)) & gol(0 | SUCCESS); ? END bdp/m0.opo0100664000021500002450000000053710216566071012166 0ustar cansellmodelTHEORY OPOBalanceX IS m0,1; AssertionLemmas,0; Initialisation,1 END & THEORY OPOProofList IS _f(1) & Initialisation.1,(_of(1) => _of(2)) END & THEORY OPOFormulas IS "`Check that the invariant (btrue) is established by the initialisation - ref 3.3'"; (btrue) END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/m0.pmi0100644000021500002450000000340510216566071012151 0ustar cansellmodelTHEORY BalanceX IS m0,5,2,0,2,1,0,0; AssertionLemmas,5,2,0,2,1,0,0; Initialisation,0,0,0,0,0,0,0 END & THEORY ProofState IS Proved(0); Proved(1); Proved(0); Proved(Util); Proved(Util) END & THEORY MethodList IS pr; pr; pr; cl & xp & ph({n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)},!P.(P <: NATURAL & !x.(x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & 1+y<=x => y: P) => x: P) => NATURAL <: P)) & pp(rp.0) & pp(rp.0) & ct & ph(x,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & se(m$0*m$0) & pp(rp.0) & pp(rp.0) & rx(#(x$0).(x$0: INTEGER & 0<=x$0 & x = 2*x$0)) & ph(m$0,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & pp(rp.0) & pp(rp.0) & se(x$0*x$0) & pp(rp.0) & pp(rp.0) & pp(rp.0) & rx(#x.(x: INTEGER & 0<=x & m$0 = 2*x)) & ph(x$0,!y.(y: INTEGER & 0<=y & 1+y<=2*x$0 => y: {n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)})) & pp(rp.0) & ph(x$1,!m.(m: NATURAL & x$0*x$0 = 2*(m*m) => x$0 = 0)) & pp(rp.0) & pp(rp.0) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x$0 or n = 2*x$0+1) & pp(rp.0) & ah(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & se(2*x$0*x$0+2*x$0) & pp(rp.0) & pp(rp.0) & rx(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & ah(k _of(2)) END & THEORY OPOFormulas IS "`Check that the invariant (btrue) is established by the initialisation - ref 3.3'"; (btrue) END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/m1.pmi0100644000021500002450000000321410216564704012151 0ustar cansellmodelTHEORY BalanceX IS m1,2,2,0,0,0,0,0; AssertionLemmas,2,2,0,0,0,0,0; Initialisation,0,0,0,0,0,0,0 END & THEORY ProofState IS Proved(Util); Proved(Util) END & THEORY MethodList IS cl & xp & rn & rn & rd & rn & ct & rn(not(#x.not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1))) & ds(!x.(x = x => not(not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1)))) & ph(n,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k))) & se(m*m) & pp(rp.0) & pp(rp.0) & ph(m,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k))) & rx(#k.(k : INTEGER & 0<=k & n = 2*k)) & se(k*k) & pp(rp.0) & pp(rp.0) & pp(rp.0) & ph(2,!x.(x = x => not(not(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) => x = 1)))) & mh(2 : INTEGER & 0<=2 & #k.(k : INTEGER & 0<=k & n = 2*k) & #k.(k : INTEGER & 0<=k & m = 2*k) => 2 = 1) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x or n = 2*x+1) & pp(rp.0) & ah(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & se(2*x*x+2*x) & pp(rp.0) & pp(rp.0) & rx(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & ah(y _of(2)) END & THEORY OPOFormulas IS "`Check that the invariant (btrue) is established by the initialisation - ref 3.3'"; (btrue) END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK) END bdp/m2.pmi0100644000021500002450000000223710216565636012163 0ustar cansellmodelTHEORY BalanceX IS m2,2,2,0,0,0,0,0; AssertionLemmas,2,2,0,0,0,0,0; Initialisation,0,0,0,0,0,0,0 END & THEORY ProofState IS Proved(Util); Proved(Util) END & THEORY MethodList IS cl & xp & ph(n,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k))) & se(m*m) & pp(rp.0) & pp(rp.0) & se(2) & pp(rp.0) & pp(rp.0) & rx(#k.(k : INTEGER & 0<=k & n = 2*k)) & ph(m,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k))) & se(k*k) & pp(rp.0) & pp(rp.0) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x or n = 2*x+1) & pp(rp.0) & ah(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & se(2*x*x+2*x) & pp(rp.0) & pp(rp.0) & rx(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & ah(y n = 0)},!P.(P <: NATURAL & !x.(x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & 1+y<=x => y: P) => x: P) => NATURAL <: P)) & pp(rp.0) & pp(rp.0) & ct & ph(x,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & se(m$0*m$0) & pp(rp.0) & pp(rp.0) & rx(#(x$0).(x$0: INTEGER & 0<=x$0 & x = 2*x$0)) & ph(m$0,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & pp(rp.0) & pp(rp.0) & se(x$0*x$0) & pp(rp.0) & pp(rp.0) & pp(rp.0) & rx(#x.(x: INTEGER & 0<=x & m$0 = 2*x)) & ph(x$0,!y.(y: INTEGER & 0<=y & 1+y<=2*x$0 => y: {n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)})) & pp(rp.0) & ph(x$1,!m.(m: NATURAL & x$0*x$0 = 2*(m*m) => x$0 = 0)) & pp(rp.0) & pp(rp.0) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x$0 or n = 2*x$0+1) & pp(rp.0) & ah(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & se(2*x$0*x$0+2*x$0) & pp(rp.0) & pp(rp.0) & rx(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & ah(k n = 0)},!P.(P <: NATURAL & !x.(x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & 1+y<=x => y: P) => x: P) => NATURAL <: P)) & pp(rp.0) & pp(rp.0) & ct & ph(x,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & se(m$0*m$0) & pp(rp.0) & pp(rp.0) & rx(#(x$0).(x$0: INTEGER & 0<=x$0 & x = 2*x$0)) & ph(m$0,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x))) & pp(rp.0) & pp(rp.0) & se(x$0*x$0) & pp(rp.0) & pp(rp.0) & pp(rp.0) & rx(#x.(x: INTEGER & 0<=x & m$0 = 2*x)) & ph(x$0,!y.(y: INTEGER & 0<=y & 1+y<=2*x$0 => y: {n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)})) & pp(rp.0) & ph(x$1,!m.(m: NATURAL & x$0*x$0 = 2*(m*m) => x$0 = 0)) & pp(rp.0) & pp(rp.0) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x$0 or n = 2*x$0+1) & pp(rp.0) & ah(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & se(2*x$0*x$0+2*x$0) & pp(rp.0) & pp(rp.0) & rx(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & ah(k x = 1))) & ds(!x.(x = x => not(not(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) => x = 1)))) & ph(n,!n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k))) & se(m*m) & pp(rp.0) & pp(rp.0) & ph(m,!n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k))) & rx(#k.(k: INTEGER & 0<=k & n = 2*k)) & se(k*k) & pp(rp.0) & pp(rp.0) & pp(rp.0) & ph(2,!x.(x = x => not(not(x: INTEGER & 0<=x & #k.(k: INTEGER & 0<=k & n = x*k) & #k.(k: INTEGER & 0<=k & m = x*k) => x = 1)))) & mh(2: INTEGER & 0<=2 & #k.(k: INTEGER & 0<=k & n = 2*k) & #k.(k: INTEGER & 0<=k & m = 2*k) => 2 = 1) & pp(rp.0) & pp(rp.0); cl & xp & ah(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & se(n/2) & pp(rp.0) & pp(rp.0) & rx(#x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & dcs(n = 2*x or n = 2*x+1) & ds(n = 2*x) & pp(rp.0) & ah(#y.(y: NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & se(2*x*x+2*x) & pp(rp.0) & pp(rp.0) & rx(#y.(y: NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & ah(y #k.(k: INTEGER & 0<=k & n = 2*k))) & se(m*m) & pp(rp.0) & pp(rp.0) & se(2) & pp(rp.0) & pp(rp.0) & rx(#k.(k: INTEGER & 0<=k & n = 2*k)) & ph(m,!n.(n: INTEGER & 0<=n & #k.(k: INTEGER & 0<=k & n*n = 2*k) => #k.(k: INTEGER & 0<=k & n = 2*k))) & se(k*k) & pp(rp.0) & pp(rp.0) & pp(rp.0) & pp(rp.0); ? END & THEORY PassList IS Force(0),?; Force(0),? END & THEORY ManForms END & THEORY Version IS POVersion(V3.8.1)(CLT == "V3.7.4")(local_op == OK); PRVersion("V3.3.3.p18.jra.bbt")(CLT == "V3.7.4") END bdp/.project0100664000021500002450000000000010124771160012556 0ustar cansellmodelbdp/m0.pmi.bbt0100644000021500002450000000551510212110006012676 0ustar cansellmodelTHEORY BBTTE IS cmd(0 | pr); cmd(0 | pr); cmd(0 | pr); cmd(0 | cl) & gol(0 | n = 0) & cmd(1 | xp) & cmd(1 | ph({n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)},!P.(P <: NATURAL & !x.(x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & 1+y<=x => y: P) => x: P) => NATURAL <: P))) & gol(1 | SET(n).(n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)): POW(NATURAL)) & cmd(2 | pp(rp.0)) & gol(1 | x: INTEGER & 0<=x & !y.(y: INTEGER & 0<=y & 1+y<=x => y: SET(n).(n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0))) => x: SET(n).(n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0))) & gol(2 | x: NATURAL) & cmd(3 | pp(rp.0)) & gol(2 | m$0: NATURAL & x*x = 2*(m$0*m$0) => x = 0) & gol(3 | x = 0) & cmd(4 | ct) & gol(4 | bfalse) & cmd(5 | ph(x,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)))) & gol(5 | #(x$0).(x$0: INTEGER & 0<=x$0 & x*x = 2*x$0)) & cmd(6 | se(m$0*m$0)) & gol(6 | m$0*m$0: INTEGER) & cmd(7 | pp(rp.0)) & gol(6 | 0<=m$0*m$0) & cmd(7 | pp(rp.0)) & cmd(5 | rx(#(x$0).(x$0: INTEGER & 0<=x$0 & x = 2*x$0))) & cmd(5 | ph(m$0,!n.(n: INTEGER & 0<=n & #x.(x: INTEGER & 0<=x & n*n = 2*x) => #x.(x: INTEGER & 0<=x & n = 2*x)))) & gol(5 | m$0: INTEGER) & cmd(6 | pp(rp.0)) & gol(5 | 0<=m$0) & cmd(6 | pp(rp.0)) & gol(5 | #x.(x: INTEGER & 0<=x & m$0*m$0 = 2*x)) & cmd(6 | se(x$0*x$0)) & gol(6 | x$0*x$0: INTEGER) & cmd(7 | pp(rp.0)) & gol(6 | 0<=x$0*x$0) & cmd(7 | pp(rp.0)) & gol(6 | m$0*m$0 = 2*(x$0*x$0)) & cmd(7 | pp(rp.0)) & cmd(5 | rx(#x.(x: INTEGER & 0<=x & m$0 = 2*x))) & cmd(5 | ph(x$0,!y.(y: INTEGER & 0<=y & 1+y<=2*x$0 => y: {n | n: NATURAL & !m.(m: NATURAL & n*n = 2*(m*m) => n = 0)}))) & gol(5 | 1+x$0<=2*x$0) & cmd(6 | pp(rp.0)) & cmd(5 | ph(x$1,!m.(m: NATURAL & x$0*x$0 = 2*(m*m) => x$0 = 0))) & gol(5 | x$1: NATURAL) & cmd(6 | pp(rp.0)) & gol(5 | x$0*x$0 = 2*(x$1*x$1)) & cmd(6 | pp(rp.0)) & cmd(5 | pp(rp.0)) & cmd(1 | pp(rp.0)) & gol(0 | SUCCESS); cmd(0 | cl) & gol(0 | #x.(x: INTEGER & 0<=x & n = 2*x)) & cmd(1 | xp) & cmd(1 | ah(#x.(x: NATURAL & (n = 2*x or n = 2*x+1)))) & gol(1 | #x.(x: NATURAL & (n = 2*x or n = 2*x+1))) & cmd(2 | se(n/2)) & gol(2 | n/2: NATURAL) & cmd(3 | pp(rp.0)) & gol(2 | n = 2*(n/2) or n = 2*(n/2)+1) & cmd(3 | pp(rp.0)) & cmd(1 | rx(#x.(x: NATURAL & (n = 2*x or n = 2*x+1)))) & cmd(1 | dcs(n = 2*x$0 or n = 2*x$0+1)) & gol(1 | #x.(x: INTEGER & 0<=x & 2*x$0 = 2*x)) & cmd(2 | pp(rp.0)) & gol(1 | #x.(x: INTEGER & 0<=x & 2*x$0+1 = 2*x)) & cmd(2 | ah(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1))) & gol(2 | #k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1)) & cmd(3 | se(2*x$0*x$0+2*x$0)) & gol(3 | 2*x$0*x$0+2*x$0: NATURAL) & cmd(4 | pp(rp.0)) & gol(3 | (2*x$0+1)*(2*x$0+1) = 2*(2*x$0*x$0+2*x$0)+1) & cmd(4 | pp(rp.0)) & cmd(2 | rx(#k.(k: NATURAL & (2*x$0+1)*(2*x$0+1) = 2*k+1))) & cmd(2 | ah(k y : P ) => x : P ) => NATURAL <: P ) ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & # x . ( x : NATURAL & n * n = 2 * x ) => # x . ( x : NATURAL & n = 2 * x ) ) ; /* it's the difficult part of the theorem */ ! ( n , m ) . ( n : NATURAL & m : NATURAL => ( n * n = 2 * ( m * m ) => n = 0 ) ) ; /* the theorem */ ! ( n , m ) . ( n : NATURAL & m : NATURAL => ( n * n = 2 * ( m * m ) <=> ( n = 0 & m = 0 ) ) ) END bdp/expand_src/m1.mch0100664000021500002450000000067410216564625014274 0ustar cansellmodelMACHINE m1 DEFINITIONS divide ( n , m ) == ( # k . ( k : NATURAL & n = m * k ) ) ; coprime ( n , m ) == ( ! x . ( x : NATURAL & divide ( n , x ) & divide ( m , x ) => x = 1 ) ) ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & divide ( n * n , 2 ) => divide ( n , 2 ) ) ; not ( # ( n , m ) . ( n : NATURAL & m : NATURAL1 & n * n = 2 * ( m * m ) & coprime ( n , m ) ) ) END bdp/expand_src/m2.mch0100664000021500002450000000067110216565346014273 0ustar cansellmodelMACHINE m2 DEFINITIONS divide ( n , m ) == ( # k . ( k : NATURAL & n = m * k ) ) ; notcoprime ( n , m ) == ( # x . ( x : NATURAL & divide ( n , x ) & divide ( m , x ) & x /= 1 ) ) ASSERTIONS /* it's a technical lemma used in the next one */ ! n . ( n : NATURAL & divide ( n * n , 2 ) => divide ( n , 2 ) ) ; ! ( n , m ) . ( n : NATURAL & m : NATURAL1 & n * n = 2 * ( m * m ) => notcoprime ( n , m ) ) END bdp/m2.pmi.bbt0100644000021500002450000000357710216565636012741 0ustar cansellmodelTHEORY BBTTE IS cmd(0 | cl) & gol(0 | #x.(x : INTEGER & 0<=x & #k.(k : INTEGER & 0<=k & n = x*k) & #k.(k : INTEGER & 0<=k & m = x*k) & not(x = 1))) & cmd(1 | xp) & cmd(1 | ph(n,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(1 | #k.(k : INTEGER & 0<=k & n*n = 2*k)) & cmd(2 | se(m*m)) & gol(2 | m*m : INTEGER) & cmd(3 | pp(rp.0)) & gol(2 | 0<=m*m) & cmd(3 | pp(rp.0)) & cmd(1 | se(2)) & gol(1 | 2 : INTEGER) & cmd(2 | pp(rp.0)) & gol(1 | 0<=2) & cmd(2 | pp(rp.0)) & gol(1 | #k.(k : INTEGER & 0<=k & m = 2*k)) & cmd(2 | rx(#k.(k : INTEGER & 0<=k & n = 2*k))) & cmd(2 | ph(m,!n.(n : INTEGER & 0<=n & #k.(k : INTEGER & 0<=k & n*n = 2*k) => #k.(k : INTEGER & 0<=k & n = 2*k)))) & gol(2 | #k.(k : INTEGER & 0<=k & m*m = 2*k)) & cmd(3 | se(k*k)) & gol(3 | k*k : INTEGER) & cmd(4 | pp(rp.0)) & gol(3 | 0<=k*k) & cmd(4 | pp(rp.0)) & gol(3 | m*m = 2*(k*k)) & cmd(4 | pp(rp.0)) & gol(1 | not(2 = 1)) & cmd(2 | pp(rp.0)) & gol(0 | SUCCESS); cmd(0 | cl) & gol(0 | #k.(k : INTEGER & 0<=k & n = 2*k)) & cmd(1 | xp) & cmd(1 | ah(#x.(x : NATURAL & (n = 2*x or n = 2*x+1)))) & gol(1 | #x.(x : NATURAL & (n = 2*x or n = 2*x+1))) & cmd(2 | se(n/2)) & gol(2 | n/2 : NATURAL) & cmd(3 | pp(rp.0)) & gol(2 | n = 2*(n/2) or n = 2*(n/2)+1) & cmd(3 | pp(rp.0)) & cmd(1 | rx(#x.(x : NATURAL & (n = 2*x or n = 2*x+1)))) & cmd(1 | dcs(n = 2*x or n = 2*x+1)) & gol(1 | #k.(k : INTEGER & 0<=k & 2*x = 2*k)) & cmd(2 | pp(rp.0)) & gol(1 | #k.(k : INTEGER & 0<=k & 2*x+1 = 2*k)) & cmd(2 | ah(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1))) & gol(2 | #y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1)) & cmd(3 | se(2*x*x+2*x)) & gol(3 | 2*x*x+2*x : NATURAL) & cmd(4 | pp(rp.0)) & gol(3 | (2*x+1)*(2*x+1) = 2*(2*x*x+2*x)+1) & cmd(4 | pp(rp.0)) & cmd(2 | rx(#y.(y : NATURAL & (2*x+1)*(2*x+1) = 2*y+1))) & cmd(2 | ah(y