X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FGRP417-1.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_TPTP%2FGRP417-1.ma;h=bf844f5c1676b8f6f79587876a8e3d54ee98a2a9;hb=0639dda9142d1cf047b07e61fb557e8877aba4d8;hp=8c972ced5da5d18b09f66edd3065602f2fe8fb68;hpb=c40f28fe5bfa74fc1fcef986c03fc960793902a5;p=helm.git diff --git a/helm/software/matita/contribs/ng_TPTP/GRP417-1.ma b/helm/software/matita/contribs/ng_TPTP/GRP417-1.ma index 8c972ced5..bf844f5c1 100644 --- a/helm/software/matita/contribs/ng_TPTP/GRP417-1.ma +++ b/helm/software/matita/contribs/ng_TPTP/GRP417-1.ma @@ -44,25 +44,25 @@ include "logic/equality.ma". (* -------------------------------------------------------------------------- *) ntheorem prove_these_axioms_3: - ∀Univ:Type.∀A:Univ.∀B:Univ.∀C:Univ. + (∀Univ:Type.∀A:Univ.∀B:Univ.∀C:Univ. ∀a3:Univ. ∀b3:Univ. ∀c3:Univ. ∀inverse:∀_:Univ.Univ. ∀multiply:∀_:Univ.∀_:Univ.Univ. -∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (inverse (multiply A (inverse (multiply (inverse (multiply (inverse (multiply B A)) (multiply B (inverse C)))) (inverse (multiply (inverse A) A)))))) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3)) +∀H0:∀A:Univ.∀B:Univ.∀C:Univ.eq Univ (inverse (multiply A (inverse (multiply (inverse (multiply (inverse (multiply B A)) (multiply B (inverse C)))) (inverse (multiply (inverse A) A)))))) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))) . -#Univ. -#A. -#B. -#C. -#a3. -#b3. -#c3. -#inverse. -#multiply. -#H0. -nauto by H0; +#Univ ##. +#A ##. +#B ##. +#C ##. +#a3 ##. +#b3 ##. +#c3 ##. +#inverse ##. +#multiply ##. +#H0 ##. +nauto by H0 ##; nqed. (* -------------------------------------------------------------------------- *)