Commit 97e0a4f9 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Automate transfer using Dktactics

parent 5469e371
......@@ -2,6 +2,100 @@ open "basics";;
open "naturals";;
open "natural_zenon";;
species NatDivides =
inherit NatTimes, NatLt;
logical let divides(m, n) = ex p : Self, times(m, p) = n;
theorem divides_times : all m n : Self,
divides(m, n) <-> (ex p : Self, times(m, p) = n)
proof = by definition of divides;
end;;
species NatDividesZenon =
inherit NatDivides;
theorem divides_times_m : all m p : Self, divides(m, times(m, p))
proof = by property divides_times;
let select (p : Self -> bool) = internal Self
external
| dedukti -> {* dk_logic.select abst_T p *}
| coq -> {* *};
theorem choice : all p : Self -> bool,
all x : Self, p(x) -> p(select(p))
proof = dedukti proof definition of select
{* dk_logic.choice abst_T. *};
let quo_pred (m : Self, n : Self, p : Self) = times(m, p) = n;
let quo(m : Self, n : Self) : Self = select (quo_pred(m, n));
theorem choice_quopred : all m n p : Self, quo_pred(m, n, p) -> quo_pred(m, n, quo(m, n))
proof =
<1>1 assume m n p : Self,
prove quo_pred(m, n, p) -> quo_pred(m, n, quo(m, n))
dedukti proof definition of quo property choice
{* abst_choice (abst_quo_pred m n) p *}
<1>f conclude;
theorem div_quo :
all m n : Self, divides(m, n) -> times(m, quo(m, n)) = n
proof =
<1>1 assume m n : Self,
hypothesis H : divides(m, n),
prove times(m, quo(m, n)) = n
<2>1 prove ex p : Self, times(m, p) = n
by hypothesis H property divides_times
<2>2 assume p : Self,
hypothesis H2 : times(m, p) = n,
prove times(m, quo(m, n)) = n
<3>1 prove quo_pred(m, n, p)
by hypothesis H2 definition of quo_pred
<3>2 prove quo_pred(m, n, quo(m, n))
by step <3>1 property choice_quopred
<3>3 prove times(m, quo(m, n)) = n
by step <3>2 definition of quo_pred
<3>f conclude
<2>f conclude
<1>f conclude;
(* property divides_le : all m n : Self, *)
(* divides(m, n) -> *)
(* le(succ(succ(zero)), n) -> *)
(* le(m, n); *)
end;;
species NatStrictlyDivides =
inherit NatDivides, NatLt;
logical let sd(m, n) = divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m);
theorem sd_divides : all m n : Self, sd(m, n) -> divides(m, n)
proof = by definition of sd;
theorem sd_lt : all m n : Self, sd(m, n) -> lt(m, n)
proof = by definition of sd;
theorem sd_1 : all m n : Self, sd(m, n) -> lt(succ(zero), m)
proof = by definition of sd;
theorem sd_intro : all m n : Self,
divides(m, n) ->
lt(m, n) ->
lt(succ(zero), m) ->
sd(m, n)
proof = by definition of sd;
end;;
species NatPrime =
inherit NatStrictlyDivides;
logical let prime(p) = lt(succ(zero), p) /\ all d : Self, ~(sd(d, p));
theorem prime_1 : all p : Self, prime(p) -> lt(succ(zero), p)
proof = by definition of prime;
theorem prime_sd : all p d : Self, prime(p) -> ~(sd(d, p))
proof = by definition of prime;
theorem prime_intro :
all p : Self,
lt(succ(zero), p) ->
(all d : Self, ~(sd(d, p))) ->
prime(p)
proof = by definition of prime;
end;;
species NatPrimeDiv =
inherit NatPrime, NatDividesZenon;
property prime_divisor :
......
......@@ -129,57 +129,3 @@ species NatLeMinusZenon =
proof of le_plus = by property le_plus_minus, plus_le;
end;;
species NatDividesZenon =
inherit NatDivides;
theorem divides_times_m : all m p : Self, divides(m, times(m, p))
proof = by property divides_times;
let select (p : Self -> bool) = internal Self
external
| dedukti -> {* dk_logic.select abst_T p *}
| coq -> {* *};
theorem choice : all p : Self -> bool,
all x : Self, p(x) -> p(select(p))
proof = dedukti proof definition of select
{* dk_logic.choice abst_T. *};
let quo_pred (m : Self, n : Self, p : Self) = times(m, p) = n;
let quo(m : Self, n : Self) : Self = select (quo_pred(m, n));
theorem choice_quopred : all m n p : Self, quo_pred(m, n, p) -> quo_pred(m, n, quo(m, n))
proof =
<1>1 assume m n p : Self,
prove quo_pred(m, n, p) -> quo_pred(m, n, quo(m, n))
dedukti proof definition of quo property choice
{* abst_choice (abst_quo_pred m n) p *}
<1>f conclude;
theorem div_quo :
all m n : Self, divides(m, n) -> times(m, quo(m, n)) = n
proof =
<1>1 assume m n : Self,
hypothesis H : divides(m, n),
prove times(m, quo(m, n)) = n
<2>1 prove ex p : Self, times(m, p) = n
by hypothesis H property divides_times
<2>2 assume p : Self,
hypothesis H2 : times(m, p) = n,
prove times(m, quo(m, n)) = n
<3>1 prove quo_pred(m, n, p)
by hypothesis H2 definition of quo_pred
<3>2 prove quo_pred(m, n, quo(m, n))
by step <3>1 property choice_quopred
<3>3 prove times(m, quo(m, n)) = n
by step <3>2 definition of quo_pred
<3>f conclude
<2>f conclude
<1>f conclude;
(* property divides_le : all m n : Self, *)
(* divides(m, n) -> *)
(* le(succ(succ(zero)), n) -> *)
(* le(m, n); *)
end;;
......@@ -11,10 +11,10 @@ species NatDecl =
property succ_inj : all m n : Self, succ(m) = succ(n) -> m = n;
(* Highr-order axiom, cannot be given to Zenon *)
property ind : all p : Self -> prop,
p (zero) ->
(all n : Self, p(n) -> p(succ(n))) ->
all n : Self, p(n);
(* property ind : all p : Self -> prop, *)
(* p (zero) -> *)
(* (all n : Self, p(n) -> p(succ(n))) -> *)
(* all n : Self, p(n); *)
end;;
species NatCase =
......@@ -22,19 +22,19 @@ species NatCase =
(* When the induction hypothesis is not needed, we can use
reasoning by case which is better supported by Zenon *)
logical let casep (n : Self) = n = zero \/ ex m : Self, n = succ(m);
theorem case : all n : Self, n = zero \/ ex m : Self, n = succ(m)
proof =
<1>1 assume n : Self,
prove casep(n) <-> (n = zero \/ ex m : Self, n = succ(m))
by definition of casep
<1>2 prove casep(zero) ->
(all n : Self, casep(n) -> casep(succ(n))) ->
all n : Self, casep(n)
dedukti proof property ind
{* abst_ind abst_casep *}
<1>3 prove casep(zero) by step <1>1
<1>4 assume n : Self, prove casep(succ(n)) by step <1>1
<1>f conclude;
property case : all n : Self, n = zero \/ ex m : Self, n = succ(m);
(* proof = *)
(* <1>1 assume n : Self, *)
(* prove casep(n) <-> (n = zero \/ ex m : Self, n = succ(m)) *)
(* by definition of casep *)
(* <1>2 prove casep(zero) -> *)
(* (all n : Self, casep(n) -> casep(succ(n))) -> *)
(* all n : Self, casep(n) *)
(* dedukti proof property ind *)
(* {* abst_ind abst_casep *} *)
(* <1>3 prove casep(zero) by step <1>1 *)
(* <1>4 assume n : Self, prove casep(succ(n)) by step <1>1 *)
(* <1>f conclude; *)
end;;
species NatOne =
......@@ -104,44 +104,4 @@ species NatLt =
proof = by definition of lt;
end;;
species NatDivides =
inherit NatTimes, NatLt;
logical let divides(m, n) = ex p : Self, times(m, p) = n;
theorem divides_times : all m n : Self,
divides(m, n) <-> (ex p : Self, times(m, p) = n)
proof = by definition of divides;
end;;
species NatStrictlyDivides =
inherit NatDivides, NatLt;
logical let sd(m, n) = divides(m, n) /\ lt(m, n) /\ lt(succ(zero), m);
theorem sd_divides : all m n : Self, sd(m, n) -> divides(m, n)
proof = by definition of sd;
theorem sd_lt : all m n : Self, sd(m, n) -> lt(m, n)
proof = by definition of sd;
theorem sd_1 : all m n : Self, sd(m, n) -> lt(succ(zero), m)
proof = by definition of sd;
theorem sd_intro : all m n : Self,
divides(m, n) ->
lt(m, n) ->
lt(succ(zero), m) ->
sd(m, n)
proof = by definition of sd;
end;;
species NatPrime =
inherit NatStrictlyDivides;
logical let prime(p) = lt(succ(zero), p) /\ all d : Self, ~(sd(d, p));
theorem prime_1 : all p : Self, prime(p) -> lt(succ(zero), p)
proof = by definition of prime;
theorem prime_sd : all p d : Self, prime(p) -> ~(sd(d, p))
proof = by definition of prime;
theorem prime_intro :
all p : Self,
lt(succ(zero), p) ->
(all d : Self, ~(sd(d, p))) ->
prime(p)
proof = by definition of prime;
end;;
(* even, odd, factorial, pred, iter, pow, div, mod, bit0, bit1, distance, egcd, log, gcd, lcm, chineseRemainder *)
open "basics";;
open "naturals";;
species NatMorph (B is NatDecl) =
species NatInd =
inherit NatCase;
property ind : all p : Self -> prop,
p (zero) ->
(all n : Self, p(n) -> p(succ(n))) ->
all n : Self, p(n);
end;;
species NatMorph (B is NatInd) =
inherit NatInd;
signature morph : Self -> B;
property morph_zero : morph(zero) = B!zero;
property morph_succ : all n : Self, morph(succ(n)) = B!succ(morph(n));
......@@ -92,7 +101,9 @@ species NatMorph (B is NatDecl) =
<1>f conclude;
end;;
species NatPlusMorph (B is NatPlus) =
species NatPlusInd = inherit NatPlus, NatInd; end;;
species NatPlusMorph (B is NatPlusInd) =
inherit NatPlus, NatMorph(B);
logical let morph_plus_predicate (a1 : Self) =
......@@ -149,7 +160,9 @@ species NatPlusMorph (B is NatPlus) =
(* <1>f conclude; *)
end;;
species NatTimesMorph (B is NatTimes) =
species NatTimesInd = inherit NatTimes, NatInd; end;;
species NatTimesMorph (B is NatTimesInd) =
inherit NatTimes, NatPlusMorph(B);
logical let morph_times_predicate (a1 : Self) =
......@@ -193,7 +206,9 @@ species NatTimesMorph (B is NatTimes) =
proof = by definition of morph_times_predicate property morph_times_with_predicate;
end;;
species NatLeMorph(B is NatLe) =
species NatLeInd = inherit NatLe, NatInd; end;;
species NatLeMorph(B is NatLeInd) =
inherit NatLe, NatPlusMorph(B);
theorem morph_le :
......@@ -246,7 +261,9 @@ species NatLeMorph(B is NatLe) =
<1>2 conclude;
end;;
species NatLtMorph(B is NatLt) =
species NatLtInd = inherit NatLt, NatInd; end;;
species NatLtMorph(B is NatLtInd) =
inherit NatLt, NatLeMorph(B);
theorem morph_lt :
......@@ -287,199 +304,199 @@ species NatLtMorph(B is NatLt) =
<1>2 conclude;
end;;
species NatDividesMorph(B is NatDivides) =
inherit NatDivides, NatTimesMorph(B), NatLtMorph(B);
theorem morph_divides :
all a1 a2 : Self,
divides(a1, a2) -> B!divides(morph(a1), morph(a2))
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : divides(a1, a2),
prove B!divides(morph(a1), morph(a2))
<2>1 prove (ex a3 : Self, times(a1, a3) = a2)
by property divides_times hypothesis H
<2>2 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2))
by step <2>1
<2>3 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2))
by step <2>2 property morph_times
<2>4 prove (ex b : B, B!times(morph(a1), b) = morph(a2))
by step <2>3
<2>5 prove B!divides(morph(a1), morph(a2))
by step <2>4 property B!divides_times
<2>f conclude
<1>2 conclude;
theorem morph_divides_rev :
all a1 a2 : Self,
B!divides(morph(a1), morph(a2)) -> divides(a1, a2)
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : B!divides(morph(a1), morph(a2)),
prove divides(a1, a2)
<2>1 prove (ex b : B, B!times(morph(a1), b) = morph(a2))
by hypothesis H property B!divides_times
<2>2 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2))
by step <2>1 property morph_surjective
<2>3 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2))
by step <2>2 property morph_times
<2>4 prove (ex a3 : Self, times(a1, a3) = a2)
<3>1 assume a3 : Self,
notation a = times(a1, a3),
hypothesis H1 : morph(times(a1, a3)) = morph(a2),
prove times(a1, a3) = a2
<4>1 prove morph(a) = morph(a2)
by hypothesis H1 definition of a
<4>2 prove morph(a) = morph(a2) -> a = a2
dedukti proof
property morph_injective
{* abst_morph_injective a a2 *}
<4>3 qed by step <4>1, <4>2 definition of a
<3>2 qed by step <3>1, <2>3
<2>f qed by step <2>4 property divides_times
<1>2 conclude;
(* proof of divides_le = *)
(* <1>1 assume m n : Self, *)
(* hypothesis H1 : divides(m, n), *)
(* hypothesis H2 : le(succ(succ(zero)), n), *)
(* prove le(m, n) *)
(* <2>1 prove B!divides(morph(m), morph(n)) *)
(* by hypothesis H1 property morph_divides *)
(* <2>2 prove B!le(B!succ(B!succ(B!zero)), morph(n)) *)
(* by hypothesis H2 property morph_zero, morph_succ, morph_le *)
(* <2>3 prove B!le(morph(m), morph(n)) *)
(* by step <2>1, <2>2 property B!divides_le *)
(* <2>4 prove B!le(morph(m), morph(n)) -> le(m, n) *)
(* by property morph_le_rev *)
(* <2>f conclude *)
(* <1>f conclude; *)
end;;
species NatSDMorph (B is NatStrictlyDivides) =
inherit NatStrictlyDivides, NatDividesMorph(B), NatLtMorph(B);
theorem morph_sd :
all a1 a2 : Self,
sd(a1, a2) -> B!sd(morph(a1), morph(a2))
proof =
<1>1 assume a1 a2 : Self,
hypothesis H : sd(a1, a2),
prove B!sd(morph(a1), morph(a2))
<2>1 prove divides(a1, a2)
by property sd_divides hypothesis H
<2>2 prove B!divides(morph(a1), morph(a2))
by property morph_divides step <2>1
<2>3 prove lt(a1, a2)
by property sd_lt hypothesis H
<2>4 prove B!lt(morph(a1), morph(a2))
by property morph_lt step <2>3
<2>5 prove lt(succ(zero), a1)
by property sd_1 hypothesis H
<2>6 prove B!lt(B!succ(B!zero), morph(a1))
by property morph_succ, morph_zero, morph_lt
step <2>5
<2>7 prove B!sd(morph(a1), morph(a2))
by property B!sd_intro
step <2>2, <2>4, <2>6
<2>f conclude
<1>f conclude;
theorem morph_sd_rev :
all a1 a2 : Self,
B!sd(morph(a1), morph(a2)) ->
sd(a1, a2)
proof =
<1>1 assume a1 a2 : Self,
hypothesis H: B!sd(morph(a1), morph(a2)),
prove sd(a1, a2)
<2>1 prove B!divides(morph(a1), morph(a2))
by property B!sd_divides hypothesis H
<2>2 prove divides(a1, a2)
by property morph_divides_rev step <2>1
<2>3 prove B!lt(morph(a1), morph(a2))
by property B!sd_lt hypothesis H
<2>4 prove lt(a1, a2)
by property morph_lt_rev step <2>3
<2>5 prove B!lt(B!succ(B!zero), morph(a1))
by property B!sd_1 hypothesis H
<2>6 prove B!lt(morph(succ(zero)), morph(a1))
by property morph_succ, morph_zero step <2>5
<2>7 notation a = succ(zero),
prove lt(succ(zero), a1)
<3>1 prove B!lt(morph(a), morph(a1))
by step <2>6 definition of a
<3>2 prove lt(a, a1)
by step <3>1 property morph_lt_rev
<3>f qed by step <3>2 definition of a
<2>8 prove sd(a1, a2)
by property sd_intro
step <2>2, <2>4, <2>7
<2>f conclude
<1>f conclude;
end;;
(* species NatDividesMorph(B is NatDivides) = *)
(* inherit NatDivides, NatTimesMorph(B), NatLtMorph(B); *)
(* theorem morph_divides : *)
(* all a1 a2 : Self, *)
(* divides(a1, a2) -> B!divides(morph(a1), morph(a2)) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : divides(a1, a2), *)
(* prove B!divides(morph(a1), morph(a2)) *)
(* <2>1 prove (ex a3 : Self, times(a1, a3) = a2) *)
(* by property divides_times hypothesis H *)
(* <2>2 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2)) *)
(* by step <2>1 *)
(* <2>3 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2)) *)
(* by step <2>2 property morph_times *)
(* <2>4 prove (ex b : B, B!times(morph(a1), b) = morph(a2)) *)
(* by step <2>3 *)
(* <2>5 prove B!divides(morph(a1), morph(a2)) *)
(* by step <2>4 property B!divides_times *)
(* <2>f conclude *)
(* <1>2 conclude; *)
(* theorem morph_divides_rev : *)
(* all a1 a2 : Self, *)
(* B!divides(morph(a1), morph(a2)) -> divides(a1, a2) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : B!divides(morph(a1), morph(a2)), *)
(* prove divides(a1, a2) *)
(* <2>1 prove (ex b : B, B!times(morph(a1), b) = morph(a2)) *)
(* by hypothesis H property B!divides_times *)
(* <2>2 prove (ex a3 : Self, B!times(morph(a1), morph(a3)) = morph(a2)) *)
(* by step <2>1 property morph_surjective *)
(* <2>3 prove (ex a3 : Self, morph(times(a1, a3)) = morph(a2)) *)
(* by step <2>2 property morph_times *)
(* <2>4 prove (ex a3 : Self, times(a1, a3) = a2) *)
(* <3>1 assume a3 : Self, *)
(* notation a = times(a1, a3), *)
(* hypothesis H1 : morph(times(a1, a3)) = morph(a2), *)
(* prove times(a1, a3) = a2 *)
(* <4>1 prove morph(a) = morph(a2) *)
(* by hypothesis H1 definition of a *)
(* <4>2 prove morph(a) = morph(a2) -> a = a2 *)
(* dedukti proof *)
(* property morph_injective *)
(* {* abst_morph_injective a a2 *} *)
(* <4>3 qed by step <4>1, <4>2 definition of a *)
(* <3>2 qed by step <3>1, <2>3 *)
(* <2>f qed by step <2>4 property divides_times *)
(* <1>2 conclude; *)
(* (\* proof of divides_le = *\) *)
(* (\* <1>1 assume m n : Self, *\) *)
(* (\* hypothesis H1 : divides(m, n), *\) *)
(* (\* hypothesis H2 : le(succ(succ(zero)), n), *\) *)
(* (\* prove le(m, n) *\) *)
(* (\* <2>1 prove B!divides(morph(m), morph(n)) *\) *)
(* (\* by hypothesis H1 property morph_divides *\) *)
(* (\* <2>2 prove B!le(B!succ(B!succ(B!zero)), morph(n)) *\) *)
(* (\* by hypothesis H2 property morph_zero, morph_succ, morph_le *\) *)
(* (\* <2>3 prove B!le(morph(m), morph(n)) *\) *)
(* (\* by step <2>1, <2>2 property B!divides_le *\) *)
(* (\* <2>4 prove B!le(morph(m), morph(n)) -> le(m, n) *\) *)
(* (\* by property morph_le_rev *\) *)
(* (\* <2>f conclude *\) *)
(* (\* <1>f conclude; *\) *)
(* end;; *)
(* species NatSDMorph (B is NatStrictlyDivides) = *)
(* inherit NatStrictlyDivides, NatDividesMorph(B), NatLtMorph(B); *)
(* theorem morph_sd : *)
(* all a1 a2 : Self, *)
(* sd(a1, a2) -> B!sd(morph(a1), morph(a2)) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H : sd(a1, a2), *)
(* prove B!sd(morph(a1), morph(a2)) *)
(* <2>1 prove divides(a1, a2) *)
(* by property sd_divides hypothesis H *)
(* <2>2 prove B!divides(morph(a1), morph(a2)) *)
(* by property morph_divides step <2>1 *)
(* <2>3 prove lt(a1, a2) *)
(* by property sd_lt hypothesis H *)
(* <2>4 prove B!lt(morph(a1), morph(a2)) *)
(* by property morph_lt step <2>3 *)
(* <2>5 prove lt(succ(zero), a1) *)
(* by property sd_1 hypothesis H *)
(* <2>6 prove B!lt(B!succ(B!zero), morph(a1)) *)
(* by property morph_succ, morph_zero, morph_lt *)
(* step <2>5 *)
(* <2>7 prove B!sd(morph(a1), morph(a2)) *)
(* by property B!sd_intro *)
(* step <2>2, <2>4, <2>6 *)
(* <2>f conclude *)
(* <1>f conclude; *)
species NatPrimeMorph (B is NatPrime) =
inherit NatPrime, NatSDMorph(B);
(* theorem morph_sd_rev : *)
(* all a1 a2 : Self, *)
(* B!sd(morph(a1), morph(a2)) -> *)
(* sd(a1, a2) *)
(* proof = *)
(* <1>1 assume a1 a2 : Self, *)
(* hypothesis H: B!sd(morph(a1), morph(a2)), *)
(* prove sd(a1, a2) *)
(* <2>1 prove B!divides(morph(a1), morph(a2)) *)
(* by property B!sd_divides hypothesis H *)
(* <2>2 prove divides(a1, a2) *)
(* by property morph_divides_rev step <2>1 *)
(* <2>3 prove B!lt(morph(a1), morph(a2)) *)
(* by property B!sd_lt hypothesis H *)
(* <2>4 prove lt(a1, a2) *)
(* by property morph_lt_rev step <2>3 *)
(* <2>5 prove B!lt(B!succ(B!zero), morph(a1)) *)
(* by property B!sd_1 hypothesis H *)
(* <2>6 prove B!lt(morph(succ(zero)), morph(a1)) *)
(* by property morph_succ, morph_zero step <2>5 *)
(* <2>7 notation a = succ(zero), *)
(* prove lt(succ(zero), a1) *)
(* <3>1 prove B!lt(morph(a), morph(a1)) *)
(* by step <2>6 definition of a *)
(* <3>2 prove lt(a, a1) *)
(* by step <3>1 property morph_lt_rev *)
(* <3>f qed by step <3>2 definition of a *)
(* <2>8 prove sd(a1, a2) *)
(* by property sd_intro *)
(* step <2>2, <2>4, <2>7 *)
(* <2>f conclude *)
(* <1>f conclude; *)
theorem morph_prime : all p : Self, prime(p) -> B!prime(morph(p))
proof =
<1>1 assume p : Self,
hypothesis H : prime(p),
prove B!prime(morph(p))
<2>1 prove lt(succ(zero), p)
by property prime_1 hypothesis H
<2>2 prove B!lt(B!succ(B!zero), morph(p))
by property morph_lt, morph_succ, morph_zero step <2>1
<2>3 prove (all d : Self, ~(sd(d, p)))
by property prime_sd hypothesis H
<2>4 prove (all d : B, ~(B!sd(d, morph(p))))
<3>1 assume d : B,
hypothesis Hd : B!sd(d, morph(p)),
prove false
<4>1 prove (ex a : Self, d = morph(a))
by property morph_surjective
<4>2 assume a : Self,
hypothesis Ha : d = morph(a),
prove false
<5>1 prove B!sd(morph(a), morph(p))
by hypothesis Hd, Ha
<5>2 prove sd(a, p)
by step <5>1 property morph_sd_rev
<5>3 qed by step <5>2
property prime_sd
hypothesis H
<4>f conclude
<3>3 conclude
<2>5 qed by step <2>2, <2>4 property B!prime_intro
<1>2 conclude;
theorem morph_prime_rev : all p : Self, B!prime(morph(p)) -> prime(p)
proof =
<1>1 assume p : Self,
hypothesis H : B!prime(morph(p)),
prove prime(p)
<2>1 prove B!lt(B!succ(B!zero), morph(p))
by property B!prime_1 hypothesis H
<2>2 prove lt(succ(zero), p)
by property morph_lt_rev, morph_succ, morph_zero
step <2>1
<2>3 prove (all d : B, ~(B!sd(d, morph(p))))
by property B!prime_sd hypothesis H
<2>4 prove (all d : Self, ~(sd(d, p)))
<3>1 assume d : Self,
hypothesis Hd : sd(d, p),