X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FTPTP%2FHEQ%2FNUM017-2.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FTPTP%2FHEQ%2FNUM017-2.ma;h=4e711a4577649a555787ceb0dba3f8ee5c1f3c48;hb=2af96fc83e36af5270b1181864855791ed38fbb8;hp=73a75f06b4d257eb533a28b1320eddce3e367ece;hpb=f68f477d76866de24ebdb5351912754a7dccbda5;p=helm.git

diff --git a/helm/software/matita/contribs/TPTP/HEQ/NUM017-2.ma b/helm/software/matita/contribs/TPTP/HEQ/NUM017-2.ma
index 73a75f06b..4e711a457 100644
--- a/helm/software/matita/contribs/TPTP/HEQ/NUM017-2.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/NUM017-2.ma
@@ -47,7 +47,7 @@ include "logic/equality.ma".
 
 (* -------------------------------------------------------------------------- *)
 theorem prove_there_is_no_common_divisor:
- ∀Univ:Set.∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀a:Univ.∀b:Univ.∀c:Univ.∀d:Univ.∀divides:∀_:Univ.∀_:Univ.Prop.∀e:Univ.∀multiply:∀_:Univ.∀_:Univ.Univ.∀prime:∀_:Univ.Prop.∀product:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀second_divided_by_1st:∀_:Univ.∀_:Univ.Univ.∀H0:product a e d.∀H1:product c c e.∀H2:product b b d.∀H3:prime a.∀H4:∀A:Univ.∀B:Univ.∀C:Univ.∀_:divides A B.∀_:product C C B.∀_:prime A.divides A C.∀H5:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.divides A C.∀H6:∀A:Univ.∀B:Univ.∀_:divides A B.product A (second_divided_by_1st A B) B.∀H7:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A B C.∀_:product A B D.eq Univ D C.∀H8:∀A:Univ.∀B:Univ.∀C:Univ.∀_:divides A B.∀_:divides C A.divides C B.∀H9:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A B C.∀_:product A D C.eq Univ B D.∀H10:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.product B A C.∀H11:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product A B C.∀_:product D B E.∀_:product F D A.product F E C.∀H12:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product A B C.∀_:product D E B.∀_:product A D F.product F E C.∀H13:∀A:Univ.∀B:Univ.product A B (multiply A B).∃A:Univ.And (divides A c) (divides A b)
+ ∀Univ:Set.∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀a:Univ.∀b:Univ.∀c:Univ.∀d:Univ.∀divides:∀_:Univ.∀_:Univ.Prop.∀e:Univ.∀multiply:∀_:Univ.∀_:Univ.Univ.∀prime:∀_:Univ.Prop.∀product:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀second_divided_by_1st:∀_:Univ.∀_:Univ.Univ.∀H0:product a e d.∀H1:product c c e.∀H2:product b b d.∀H3:prime a.∀H4:∀A:Univ.∀B:Univ.∀C:Univ.∀_:prime A.∀_:product C C B.∀_:divides A B.divides A C.∀H5:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.divides A C.∀H6:∀A:Univ.∀B:Univ.∀_:divides A B.product A (second_divided_by_1st A B) B.∀H7:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A B D.∀_:product A B C.eq Univ D C.∀H8:∀A:Univ.∀B:Univ.∀C:Univ.∀_:divides C A.∀_:divides A B.divides C B.∀H9:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀_:product A D C.∀_:product A B C.eq Univ B D.∀H10:∀A:Univ.∀B:Univ.∀C:Univ.∀_:product A B C.product B A C.∀H11:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product F D A.∀_:product D B E.∀_:product A B C.product F E C.∀H12:∀A:Univ.∀B:Univ.∀C:Univ.∀D:Univ.∀E:Univ.∀F:Univ.∀_:product A D F.∀_:product D E B.∀_:product A B C.product F E C.∀H13:∀A:Univ.∀B:Univ.product A B (multiply A B).∃A:Univ.And (divides A b) (divides A c)
 .
 intros.
 exists[