Duck Proof Script A Lemma About Double Operation

 ```*** file: /net/cs/htdocs/users/goguen/kumo/sqrt2/sqrt2.duck ***************************************** style: beijing ***************************************** spec: /net/cs/htdocs/users/goguen/kumo/sqrt2/sqrt2.bob ***************************************** dir: /net/cs/htdocs/groups/tatami/kumo/exs/sqrt2 ***************************************** proof: <> goal: (forall M : Nat)(exists N : Nat) (M = 2 * N or M = 2 * N + 1) . by: induction on M with scheme {0, s}; <> exq-let N = 0 ; <> all-uq-elim; imp-elim >> {A1}; skolem A1 >> {A2}; case-anal A2 >> {A3 A4}; *** case 1 to-rule A3; exq-let N = n1 ; *** case 2 <> to-rule A4; exq-let N = n1 + 1 ; [] ************************************************************ proof: <> goal: (forall M : Nat) div2(2 * M) = M . by: induction on M with scheme {0, s}; [] ************************************************************ proof: <> goal: (forall M : Nat) mod2(2 * M) = 0 . by: induction on M with scheme {0, s}; [] ************************************************************ proof: <> goal: (forall M : Nat) mod2(2 * M + 1) = 1 . by: induction on M with scheme {0, s}; [] *********************************************************** proof: <> goal: (forall N M : Nat) ((M + N) - N) = M . by: induction on N with scheme {0, s}; [] ********************************************************** proof: <> goal: (forall K : NzNat) K > 0 . by: induction on K with scheme {1, s}; [] ********************************************************** proof: <> goal: (forall M : Nat)(forall K : NzNat) M + K > M . by: induction on M with scheme {0, s}; lemma NzNatGtZero; [] *********************************************************** proof: <> goal: (forall M N : Nat) (2 * M * M = N * N implies (exists K : Nat) N = 2 * K) . by: all-uq-elim; imp-elim >> { A1 }; lemma NatOddEven >> { Lemma }; instance Lemma with n >> { A2 }; skolem A2 >> { A3 }; case-anal A3 >> { A4 A5 }; *** case 1 to-rule A4; exq-let K = n1; red; *** case 2 eq-apply A5 A1 >> { A6 }; lemma Mod2Double; lemma Mod2DoublePlus1; op-apply mod2 A6 >> { A7 }; red A7; [] *********************************************************** proof: <> goal: (forall M N : Nat) (2 * M = 2 * N implies M = N) . by: all-uq-elim; imp-elim >> {A}; lemma Div2Time2; op-apply div2 A >> {B}; to-rule B; red; [] *********************************************************** induction-scheme: GCD sort NzNat . assertion P : NzNat NzNat . base P(1,1) . induction ops m n : -> NzNat . assume P(m, n) . prove P(m + n, n) . induction ops m n : -> NzNat . assume P(m, n) . prove P(m, m + n) . [] *********************************************************** proof: <> goal: (forall M N : NzNat) (gcd(2 * M , 2 * N) > 1) . by: lemma SumSubtr ; induction on with scheme GCD ; [] *********************************************************** proof: <> goal: not (exists M N : NzNat) (2 * M * M = N * N and gcd(M, N) = 1) . by: neg-elim; skolem; de-conj >> {A1 A2} ; lemma Lemma1 >> {Lemma1} ; modus Lemma1 A1 ; skolem >> {A3} ; eq-apply A3 A1; backward >> {A4} ; lemma Lemma2 >> {Lemma2} ; modus Lemma2 A4 >> {A5} ; modus Lemma1 A5; skolem >> {A6} ; eq-apply A3 A2 >> {A7} ; eq-apply A6 A7 >> {A8} ; lemma Lemma3 >> {Lemma3} ; instance Lemma3 with n4 n3 >> {A9} ; eq-apply A8 A9 >> {A10} ; [] *********************************************************** display: <> title: "A Natural Number Must be Odd or Even" <> [] *********************************************************** display: <> title: "Div2 is an inverse operation of double operation" <> [] ************************************************************ display: <> title: "A Lemma About Mod2" <> [] ************************************************************ display: <> title: "A Lemma About Mod2" <> [] ************************************************************ display: <> title: "A Relation between Sum and Subtract" <> [] *********************************************************** display: <> title: "NzNat is Greater than Zero" <> [] *********************************************************** display: <> title: "Increasing by Adding Positive Number" <> [] *********************************************************** display: <> title: "A Lemma About Double Operation" <> [] *********************************************************** display: <> title: "A Lemma About Double Operation" <> [] *********************************************************** display: <> title: "A Lemma About GCD" <> [] *********************************************************** display: <> title: "The Square Root of 2 is Irrational" <> intro: "We want to prove the square root of 2 is irrational. "+ "

By the definition of rational number, we will show that "+ "there are no numbers [itex]N[/itex] and [itex]M[/itex] "+ " such that [itex]2 * M * M = N * N[/itex] and "+ " [itex]gcd(M, N) = 1[/itex] ." [] ```