(-a) × (-a) = a × a


121

Wszyscy wiemy, że (miejmy nadzieję), ale czy możesz to udowodnić?(a)×(a)=a×a

Twoim zadaniem jest udowodnienie tego faktu za pomocą aksjomatów pierścienia. Jakie są aksjomaty pierścieniowe? Aksjomaty pierścieniowe są listą reguł, których muszą przestrzegać dwie operacje binarne na zbiorze. Dwie operacje to dodawanie, i mnożenie, . Do tego wyzwania należą aksjomaty pierścieniowe, w których i są zamkniętymi operacjami binarnymi na pewnym zestawie , jest zamkniętą operacją jednoargumentową na , a , , są członami :+×+×SSabcS

  1. a+(b+c)=(a+b)+c

  2. a+0=a

  3. a+(a)=0

  4. a+b=b+a *

  5. a×(b×c)=(a×b)×c

  6. a×1=a

  7. 1×a=a

  8. a×(b+c)=(a×b)+(a×c)

  9. (b+c)×a=(b×a)+(c×a)

Twój dowód powinien być ciągiem równości, z których każdy jest zastosowaniem jednego aksjomatu.

Możesz zastosować aksjomaty do całego wyrażenia lub do niektórych podwyrażeń. Na przykład, jeśli mamy , możemy zastosować aksjomat 4 tylko do terminu terminu lub całego wyrażenia jako całości. Zmienne mogą również zastąpić dowolnie złożone wyrażenia, na przykład możemy zastosować aksjomat 4 do aby uzyskać . Na każdym etapie dowodu można zastosować tylko jeden aksjomat do jednego wyrażenia. Wszystkie aksjomaty są dwukierunkowe, co oznacza, że ​​podstawienie może iść w dowolnym kierunku. Takie rzeczy jak następujące nie są dozwolone(a+c)+(b+c)(b+c)(a+c)((a×c)+b)+((a)+1)((a)+1)+((a×c)+b)

(a + b) + (c + d) = (a + (b + c)) + d Ax. 1

Należy to zrobić w dwóch krokach:

(a + b) + (c + d) = ((a + b) + c) + d Ax. 1
                  = (a + (b + c)) + d Ax. 1

Nie można zakładać faktów, które normalnie można brać za pewnik, ale których nie ma na liście aksjomatów , na przykład jest prawdą, ale wymaga wielu kroków, aby wykonać formularz.(a)=(1)×a

Użytkownik Anthony uprzejmie zapewnił internetowy weryfikator poprawności, który można wykorzystać jako zamiennik TIO.

Przykładowy dowód

Oto przykładowy dowód, że przy użyciu aksjomatów oznaczonych po prawej stronie każdego kroku.(a)=a

 -(-a) = (-(-a)) + 0          Ax. 2
       = 0 + (-(-a))          Ax. 4
       = (a + (-a)) + (-(-a)) Ax. 3
       = a + ((-a) + (-(-a))) Ax. 1
       = a + 0                Ax. 3
       = a                    Ax. 2

Wypróbuj online!

Zostaniesz poproszony o udowodnienie pomocą sukcesywnego podstawiania, jak pokazano powyżej.(a)×(a)=a×a

Punktacja

To jest więc twoje odpowiedzi będą punktowane w liczbie kroków wykonanych, aby dostać się od do , przy czym niższy wynik jest lepszy.(a)×(a)a×a

Lemmy

Niektóre odpowiedzi wykorzystały lematy w swoich dowodach, więc opiszę, jak należy to oceniać, aby uniknąć nieporozumień. Dla niewtajemniczonych lematy są dowodami faktów, które wykorzystasz później w dowodzie. W prawdziwej matematyce mogą być pomocne w uporządkowaniu myśli lub jasnym przekazaniu czytelnikowi informacji. W tym wyzwaniu używanie lematów nie powinno mieć bezpośredniego wpływu na twój wynik. (Chociaż organizacja dowodów może ułatwić lub utrudnić grę w golfa)

Jeśli zdecydujesz się użyć lematów, będzie to kosztowało tyle kroków, ile trzeba, aby udowodnić, że lemma jest przede wszystkim za każdym razem, gdy go używasz. Na przykład tutaj jest podział wyniku na dowód wykorzystujący lematy.

Lemma:
a × 0 = 0

Proof (7 steps):
a × 0 = (a × 0) + 0                        Ax. 2 (1)
      = (a × 0) + ((a × b) + (-(a × b)))   Ax. 3 (1)
      = ((a × 0) + (a × b)) + (-(a × b))   Ax. 1 (1)
      = (a × (0 + b)) + (-(a × b))         Ax. 8 (1)
      = (a × (b + 0)) + (-(a × b))         Ax. 4 (1)
      = (a × b) + (-(a × b))               Ax. 2 (1)
      = 0                                  Ax. 3 (1)

Theorem:
(a × 0) + (b × 0) = 0

Proof (15 steps):
(a × 0) + (b × 0) = 0 + (b × 0)  Lemma (7)
                  = (b × 0) + 0  Ax. 4 (1)
                  = b × 0        Ax. 2 (1)
                  = 0            Lemma (7)

*: Zwrócono uwagę, że ten aksjomat nie jest absolutnie konieczny do udowodnienia tej właściwości, jednak nadal możesz go używać.

†: Ponieważ nie pojawia się w pożądanej równości, żaden dowód, który używa tych aksjomatów, nie jest minimalny. To znaczy, że te aksjomaty nie mogą pomóc w udowodnieniu pożądanego faktu. Zostały one włączone tylko ze względu na kompletność.1


8
Czy program, który piszemy, powinien to rozwiązać, czy po prostu wydrukować odpowiedź?
Tahg

8
@Tahg Powinieneś to udowodnić i przedstawić dowód jako odpowiedź. Różni się to od większości (jeśli nie wszystkich) problemów, które tu zobaczysz.
HyperNeutrino,

8
Frustrująco się zbliżyłem, zanim zdałem sobie sprawę, że * 0 = 0 nie ma na liście aksjomatów.
Sparr

8
Emm ... Mogę się mylić, ale czy to nie jest poza tematem? Czy odpowiedzi nie powinny zawierać kodu?
całkowicie ludzki,

34
@icrieverytim, jeśli to pomaga, pomyśl o liście aksjomatów jako języku programowania z dziewięcioma wbudowanymi funkcjami podstawiania parametrów, a to jest golf golfowy dla funkcji, która zamienia określone wejście w określone wyjście.
Sparr

Odpowiedzi:


47

18 kroków

(-a)*(-a) = ((-a)*(-a))+0                                             Axiom 2
          = ((-a)*(-a))+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))        Axiom 3
          = (((-a)*(-a))+((a*a)+(a*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = (((a*a)+(a*(-a)))+((-a)*(-a)))+(-((a*a)+(a*(-a))))        Axiom 4
          = ((a*a)+((a*(-a))+((-a)*(-a))))+(-((a*a)+(a*(-a))))        Axiom 1
          = ((a*a)+((a+(-a))*(-a)))+(-((a*a)+(a*(-a))))               Axiom 9
          = ((a*a)+(0*(-a)))+(-((a*a)+(a*(-a))))                      Axiom 3
          = ((a*(a+0))+(0*(-a)))+(-((a*a)+(a*(-a))))                  Axiom 2
          = ((a*(a+(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))           Axiom 3
          = (((a*a)+(a*(a+(-a))))+(0*(-a)))+(-((a*a)+(a*(-a))))       Axiom 8
          = ((a*a)+((a*(a+(-a)))+(0*(-a))))+(-((a*a)+(a*(-a))))       Axiom 1
          = (a*a)+(((a*(a+(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))       Axiom 1
          = (a*a)+((((a*a)+(a*(-a)))+(0*(-a)))+(-((a*a)+(a*(-a)))))   Axiom 8
          = (a*a)+(((a*a)+((a*(-a))+(0*(-a))))+(-((a*a)+(a*(-a)))))   Axiom 1
          = (a*a)+(((a*a)+((a+0)*(-a)))+(-((a*a)+(a*(-a)))))          Axiom 9
          = (a*a)+(((a*a)+(a*(-a)))+(-((a*a)+(a*(-a)))))              Axiom 2
          = (a*a)+0                                                   Axiom 3
          = a*a                                                       Axiom 2

Napisałem program, aby sprawdzić moje rozwiązanie. Więc jeśli znajdziesz w tym błąd, mój program też się myli.


@Etlay Czy z ciekawości napisałeś swój program w Prologu?
Jalil Compaoré

23
Byłoby wspaniale, gdybyś mógł dołączyć swój program. Z pewnością może pomóc zweryfikować inne rozwiązania.
Sriotchilism O'Zaic

2
Jak dostałeś się od pierwszej linii do drugiej, stosując jeden aksjomat za jednym razem?
SztupY

4
@SztupY Aksjomat 3 jest v + (-v) = 0dać v = ((a*a)+(a*(-a))i dostać się tam w 1 kroku.
MT0,


29

18 kroków

Różni się od już opublikowanego 18-etapowego rozwiązania.

a*a = a*a + 0                                                 A2
    = a*a + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))        A3
    = (a*a + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))        A1
    = (a*a + a*((-a) + (-a))) + (-(a*(-a) + a*(-a)))          A8
    = a*(a + ((-a) + (-a))) + (-(a*(-a) + a*(-a)))            A8
    = a*((a + (-a)) + (-a)) + (-(a*(-a) + a*(-a)))            A1
    = a*(0 + (-a)) + (-(a*(-a) + a*(-a)))                     A3
    = a*((-a) + 0) + (-(a*(-a) + a*(-a)))                     A4
    = a*(-a) + (-(a*(-a) + a*(-a)))                           A2
    = (a + 0)*(-a) + (-(a*(-a) + a*(-a)))                     A2
    = (a + (a + (-a)))*(-a) + (-(a*(-a) + a*(-a)))            A3
    = ((a + a) + (-a))*(-a) + (-(a*(-a) + a*(-a)))            A1
    = ((-a) + (a + a))*(-a) + (-(a*(-a) + a*(-a)))            A4
    = ((-a)*(-a) + (a + a)*(-a)) + (-(a*(-a) + a*(-a)))       A9
    = ((-a)*(-a) + (a*(-a) + a*(-a))) + (-(a*(-a) + a*(-a)))  A9
    = (-a)*(-a) + ((a*(-a) + a*(-a)) + (-(a*(-a) + a*(-a))))  A1
    = (-a)*(-a) + 0                                           A3
    = (-a)*(-a)                                               A2

Ciekawe, że ktoś robi to wstecz. Wszystkie kroki są odwracalne, więc jest to dobry dowód.
Sriotchilism O'Zaic

To, że przewraca się do góry nogami, jest w większości przypadkowe. Dowód jest właściwie dość symetryczny: używam dwóch podobnych sekwencji kroków, aby przejść z jednego końca do drugiego terminu a*(-a) + stuff.
Emil Jeřábek


28

29 26 kroków

Żadnych lematów!

Skomentuj, jeśli zauważysz coś złego. (Bardzo łatwo jest popełnić błąd)

(-a) × (-a) = ((-a) + 0) × (-a)                                                  Ax. 2
            = ((-a) + (a + (-a))) × (-a)                                         Ax. 3
            = ((a + (-a)) + (-a)) × (-a)                                         Ax. 4
            = (a + ((-a) + (-a))) × (-a)                                         Ax. 1
            = (a × (-a)) + (((-a) + (-a)) × (-a))                                Ax. 9
            = (a × ((-a) + 0)) + (((-a) + (-a)) × (-a))                          Ax. 2
            = (a × ((-a) + (a + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 3
            = (a × ((a + (-a)) + (-a))) + (((-a) + (-a)) × (-a))                 Ax. 4
            = (a × (a + ((-a) + (-a)))) + (((-a) + (-a)) × (-a))                 Ax. 1
            = ((a × a) + (a × ((-a) + (-a)))) + (((-a) + (-a)) × (-a))           Ax. 8
            = (a × a) + ((a × ((-a) + (-a))) + (((-a) + (-a)) × (-a)))           Ax. 1
            = (a × a) + (((a × (-a)) + (a × (-a))) + (((-a) + (-a)) × (-a)))     Ax. 8
            = (a × a) + (((a + a) × (-a)) + (((-a) + (-a)) × (-a)))              Ax. 9
            = (a × a) + (((a + a) + ((-a) + (-a))) × (-a))                       Ax. 9
            = (a × a) + ((((a + a) + (-a)) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + (a + (-a))) + (-a)) × (-a))                       Ax. 1
            = (a × a) + (((a + 0) + (-a)) × (-a))                                Ax. 3
            = (a × a) + ((a + (-a)) × (-a))                                      Ax. 2
            = (a × a) + (0 × (-a))                                               Ax. 3
            = (a × a) + ((0 × (-a)) + 0)                                         Ax. 2
            = (a × a) + ((0 × (-a)) + ((0 × (-a)) + (-(0 × (-a)))))              Ax. 3
            = (a × a) + (((0 × (-a)) + (0 × (-a))) + (-(0 × (-a))))              Ax. 1
            = (a × a) + (((0 + 0) × (-a)) + (-(0 × (-a))))                       Ax. 9
            = (a × a) + ((0 × (-a)) + (-(0 × (-a))))                             Ax. 2
            = (a × a) + 0                                                        Ax. 3
            = (a × a)                                                            Ax. 2

Kredyt trafia do Maltysen za 0 × (-a) = 0



14

18 kroków

Nie pierwszy 18-krokowy dowód, ale jest prostszy niż inne.

(-a)*(-a)
= (-a)*(-a) + 0                             [Axiom 2]
= (-a)*(-a) + ((-a)*a + -((-a)*a))          [Axiom 3]
= ((-a)*(-a) + (-a)*a) + -((-a)*a)          [Axiom 1]
= ((-a)*(-a) + ((-a) + 0)*a) + -((-a)*a)    [Axiom 2]
= ((-a)*(-a) + ((-a)*a + 0*a)) + -((-a)*a)  [Axiom 9]
= (((-a)*(-a) + (-a)*a) + 0*a) + -((-a)*a)  [Axiom 1]
= ((-a)*((-a) + a) + 0*a) + -((-a)*a)       [Axiom 8]
= ((-a)*(a + (-a)) + 0*a) + -((-a)*a)       [Axiom 4]
= ((-a)*0 + 0*a) + -((-a)*a)                [Axiom 3]
= (0*a + (-a)*0) + -((-a)*a)                [Axiom 4]
= ((a + (-a))*a + (-a)*0) + -((-a)*a)       [Axiom 3]
= ((a*a + (-a)*a) + (-a)*0) + -((-a)*a)     [Axiom 9]
= (a*a + ((-a)*a + (-a)*0)) + -((-a)*a)     [Axiom 1]
= (a*a + (-a)*(a + 0)) + -((-a)*a)          [Axiom 8]
= (a*a + (-a)*a) + -((-a)*a)                [Axiom 2]
= a*a + ((-a)*a + -((-a)*a))                [Axiom 1]
= a*a + 0                                   [Axiom 3]
= a*a                                       [Axiom 2]

Uprawomocnić


9
A2: (-a) x (-a) = ((-a) + 0) x (-a)
A3:             = ((-a) + (a + (-a))) x (-a)
A9:             = ((-a) x (-a)) + ((a + (-a)) x (-a))
A4:             = ((-a) x (-a)) + (((-a) + a) x (-a))
A9:             = ((-a) x (-a)) + (((-a) x (-a)) + (a x (-a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x (-a))
A2:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + 0))
A3:             = (((-a) x (-a)) + ((-a) x (-a))) + (a x ((-a) + (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + (a x (a + (-a))))
A8:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x a) + (a x (-a))))
A4:             = (((-a) x (-a)) + ((-a) x (-a))) + ((a x (-a)) + ((a x (-a)) + (a x a)))
A1:             = (((-a) x (-a)) + ((-a) x (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + (((a x (-a)) + (a x (-a))) + (a x a))
A8:             = ((-a) x ((-a) + (-a))) + ((a x ((-a) + (-a))) + (a x a))
A1:             = (((-a) x ((-a) + (-a))) + (a x ((-a) + (-a)))) + (a x a)
A9:             = (((-a) + a) x ((-a) + (-a))) + (a x a)
A4:             = ((a + (-a)) x ((-a) + (-a))) + (a x a)
Lemma:          = (0 x ((-a) + (-a))) + (a x a)
A3:             = 0 + (a x a)
A4:             = (a x a) + 0
A2:             = (a x a)

Lemma: 0 = 0 x a

A3: 0 = (0 x a) + (-(0 x a))
A2:   = ((0 + 0) x a) + (-(0 x a))
A9:   = ((0 x a) + (0 x a)) + (-(0 x a))
A1:   = (0 x a) + ((0 x a) + (-(0 x a)))
A3:   = (0 x a) + 0
A2:   = (0 x a)

27 26 kroków Dziękujemy Funky Computer Man za zauważenie duplikatu.


1
Witamy na stronie! Nie jestem pewien, dlaczego tworzysz lemat tylko po to, by go użyć tylko raz, ale przypuszczam, że nie jest to sprzeczne z regułami.
Sriotchilism O'Zaic

@FunkyComputerMan Dziękujemy! Masz rację; Nie jestem pewien, o czym myślałem, kiedy napisałem ten lemat ^^. I dziękuję za edycję i uwagę.
Jalil Compaoré

1
@ JalilCompaoré Myślę, że możesz być w stanie uratować to ostatnie A3, zaczynając od podania A2drugiego (-a) zamiast pierwszego. Nie jestem jednak pewien, ponieważ nie mam teraz czasu, aby się tym zająć.
H.PWiz

7

6 + 7 + 7 + 6 + 3 = 29 kroków

Naprawdę mam nadzieję, że nic nie spieprzyłem, zostaw komentarz, jeśli myślisz, że tak.

Lemma 1. a*0=0 (6 steps)

0 = a*0 + -(a*0)  axiom 3
= a*(0+0) + -(a*0) axiom 2
= (a*0 + a*0) + -(a*0) axiom 8
= a*0 + (a*0 + -(a*0)) axiom 1
= a*0 + 0 axiom 3
= a*0 axiom 2

Lemma 2. a*(-b) = -(a*b) (7 steps)

a*(-b) = a*(-b) + 0 axiom 2
= a*(-b) + (a*b + -(a*b)) axiom 3
= (a*(-b) + a*b) + -(a*b) axiom 1
= a*(-b+b) + -(a*b) axiom 8
= a*0 + -(a*b) axiom 3
= 0 + -(a*b) lemma 1
= -(a*b) axiom 2

Lemma 3. (-a)*b = -(a*b) (7 steps)
    same as above

Lemma 4. -(-(a)) = a (6 steps)

 -(-a) = (-(-a)) + 0    axiom 2
 = 0 + (-(-a))          axiom 4
 = (a + (-a)) + (-(-a)) axiom 3
 = a + ((-a) + (-(-a))) axiom 1
 = a + 0                axiom 3
 = a                    axiom 2

Theorem. -a*-a=0 (3 steps)

-a*-a = -(a*(-a)) lemma 3
= -(-(a*a)) lemma 2
= a*a lemma 4

Q.E.D.

3
Nie sądzę, żebyś mógł robić lematy
HyperNeutrino,

11
„Twierdzenie. -A * -a = 0” powinno być = a * a?
Sparr

2
@ H.PWiz Nie mam problemu z ludźmi używającymi lematów, ale kosztują tyle kroków, ile są długie przy każdym użyciu. Odradzam ich używanie, ponieważ mogą przeszkadzać w optymalizacji, ale jeśli o mnie chodzi, ten post jest w porządku.
Sriotchilism O'Zaic

4
przejście z „0 + - (a * b)” na „- (a * b)” w jednym zastosowaniu aksjomatu 2 jest niewłaściwe. musisz użyć aksjomatu 4, aby zamienić boki + na pierwszym.
Sparr

2
Sposób, w jaki go czytam, to: lemat 2/3 to 6 kroków plus przykład lematu 1 na 12 kroków, lemat 4 to 6 kroków, w sumie 30 kroków. Czy coś mi umyka?
Tahg

6

23 kroki

(-a) * (-a) = ((-a) * (-a)) + 0                                 ✔ axiom 2
            = ((-a) * (-a)) + (((-a) * a) + -((-a) * a))        ✔ axiom 3
            = (((-a) * (-a)) + (-a) * a) + -((-a) * a)          ✔ axiom 1
            = (-a) * (-a + a) + -((-a) * a)                     ✔ axiom 8
            = (-a) * (a + (-a)) + -((-a) * a)                   ✔ axiom 4
            = ((-a) * 0) + -((-a) * a)                          ✔ axiom 3
            = (((-a) * 0) + 0) + -((-a) * a)                    ✔ axiom 2
            = ((-a) * 0 + ((-a)*0 + -((-a)*0))) + -((-a) * a)   ✔ axiom 3
            = (((-a) * 0 + (-a)*0) + -((-a)*0)) + -((-a) * a)   ✔ axiom 1
            = ((-a) * (0 + 0) + -((-a)*0)) + -((-a) * a)        ✔ axiom 8
            = ((-a) * 0 + -((-a)*0)) + -((-a) * a)              ✔ axiom 2
            = 0 + -((-a) * a)                                   ✔ axiom 3
            = (0* a) + -(0*a) + -((-a) * a)                     ✔ axiom 3
            = ((0+0)* a) + -(0*a) + -((-a) * a)                 ✔ axiom 2
            = ((0 * a ) + (0*a) + -(0*a)) + -((-a) * a)         ✔ axiom 9
            = ((0 * a ) + ((0*a) + -(0*a))) + -((-a) * a)       ✔ axiom 1
            = ((0 * a ) + 0) + -((-a) * a)                      ✔ axiom 3
            = (0 * a ) + -((-a) * a)                            ✔ axiom 2
            = ((a + -a) * a ) + -((-a) * a)                     ✔ axiom 3
            = ((a * a) + (-a) * a) + -((-a) * a)                ✔ axiom 9
            = (a * a) + (((-a) * a) + -((-a) * a))              ✔ axiom 1
            = (a * a) + 0                                       ✔ axiom 3
            = a * a                                             ✔ axiom 2

Wypróbuj online!

Tak, dobrze przeczytałeś, napisałem test sprawdzający dla tej układanki (oczywiście istnieje możliwość, że sam tester jest zły)


5

34 kroki

Lemma 1: 0=0*a (8 steps)
    0
A3: a*0 + -(a*0)
A4: -(a*0) + a*0
A2: -(a*0) + a*(0+0)
A8: -(a*0) + (a*0 + a*0)
A1: (-(a*0) + a*0) + a*0
A3: 0 + a*0
A4: a*0 + 0
A2: a*0

Theorem: -a*-a = a*a (49 steps)

    -a * -a
A2: (-a+0) * -a
A2: (-a+0) * (-a+0)
A3: (-a+(a+-a)) * (-a+0)
A3: (-a+(a+-a)) * (-a+(a+-a))
A8: -a*(-a+(a+-a)) + (a+-a)*(-a+(a+-a))
A8: -a*(-a+(a+-a)) + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+(a+-a)) + a*(-a+(a+-a))
A3: -a*(-a+0)      + -a*(-a+0)      + a*(-a+(a+-a))
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*(a+-a)
A8: -a*(-a+0)      + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*(-a+0)      + a*-a + a*a + a*-a
A2: -a*-a          + -a*-a          + a*-a + a*a + a*-a
A8: -a*-a          + (-a+a)*-a             + a*a + a*-a
A3: -a*-a          + 0*-a                  + a*a + a*-a
L1: -a*-a          + 0                     + a*a + a*-a
A2: -a*-a                                  + a*a + a*-a
A4: a*a + -a*-a + a*-a
A8: a*a + (-a+a)*-a
A3: a*a + 0*-a
L1: a*a + 0
A2: a*a

1
Po chwili zauważam brak parens. Ponieważ stowarzyszenie kosztuje kroki, myślę, że łatwiej byłoby zweryfikować twój dowód, gdybyś uwzględnił pareny.
Sriotchilism O'Zaic

Nadal ulepszam i aktualizuję. Spróbuję uwzględnić wszystkie pareny, kiedy skończę.
Sparr

5

25 kroków

Uwaga: w oparciu o pytanie zakładam, że reguły logiki (w tym równości) są implikowane i nie liczą się do całkowitej liczby kroków. Oznacza to, że rzeczy takie jak „jeśli x = y, a następnie y = x” i „jeśli ((P AND Q) AND R), a następnie (P AND (Q AND R))” mogą być używane niejawnie.

Lemat Z [6 stopni] : 0*a = 0:

0 = (0*a) + (-(0*a))       | Ax. 3
  = ((0+0)*a) + (-(0*a))   | Ax. 2
  = (0*a + 0*a) + (-(0*a)) | Ax. 9
  = 0*a + (0*a + (-(0*a))) | Ax. 1
  = 0*a + (0)              | Ax. 3
  = 0*a                    | Ax. 2

Lemma M [12 kroków] :(-a)*b = -(a*b)

(-a)*b = (-a)*b + 0                | Ax. 2
       = (-a)*b + (a*b + (-(a*b))) | Ax. 3
       = ((-a)*b + a*b) + (-(a*b)) | Ax. 5
       = ((-a)+a)*b + (-(a*b))     | Ax. 9
       = 0*b + (-(a*b))            | Ax. 3
       = 0 + (-(a*b))              | Lem. Z [6]
       = -(a*b)                    | Ax. 2

Twierdzenie [25 kroków] :(-a)*(-a) = a*a

(-a)*(-a) = (-a)*(-a) + 0                | Ax. 2
          = 0 + (-a)*(-a)                | Ax. 4
          = (a*a + (-(a*a))) + (-a)*(-a) | Ax. 3
          = a*a + ((-(a*a)) + (-a)*(-a)) | Ax. 1
          = a*a + ((-a)*a + (-a)*(-a))   | Lem. M [12]
          = a*a + ((-a)*(a + (-a)))      | Ax. 8
          = a*a + ((-a)*0)               | Ax. 3
          = a*a + 0                      | Lem. Z [6]
          = a*a                          | Ax. 2

Czuję, że jest tu miejsce na ulepszenia; na przykład używam przemiennej właściwości dodawania, chociaż wydaje się, że powinno to być niepotrzebne, ponieważ (-a)*(-a) = a*ajest to prawdą w strukturach algebraicznych, w których dodawanie nie jest przemienne. Z drugiej strony, w tych strukturach addytywna tożsamość jest przemienna i to wszystko, czego potrzebowałem na dowód. Nie wiem. Mówiąc bardziej ogólnie, struktura dowodu wydaje się raczej bezkierunkowa; Po prostu rzuciłem coś na problem, dopóki nie zadziałało, więc założę się, że jest jakaś optymalizacja do zrobienia.

To była zabawa - dziękuję za interesujące i kreatywne pytanie OP! Nie widziałem wcześniej takich wyzwań; mam nadzieję, że staje się rzeczywistością!


Widzę, jak podejście zastosowane w Lemma Z może stanowić równoważny dowód 0=(-a)*0w 6 krokach. Technicznie jednak zasługuje na swoją własną lemat, prawda?
SmileAndNod

4

22 23 kroki

Nowa odpowiedź, ponieważ moja poprzednia była wadliwa. Pozwól mi najpierw dodać kilka ogólnych komentarzy:

  • Problem nie pozwala dodawać terminów po obu stronach równania; raczej możemy zmodyfikować tylko początkowy ciąg.
  • Nie należy zakładać, że mnożenie jest przemienne.
  • Otrzymujemy jednostkę 1 , ale nie odgrywa ona żadnej roli w układance, ponieważ jest zaangażowana wyłącznie w reguły, które ją definiują.

Teraz dowód (zauważ, że definiuję n = (-a) w celu uproszczenia czytania):

(-a)×(-a) :=
n×n =
n×n + 0 =                                [Ax. 2]
n×n + [n×a + -(n×a)] =                   [Ax. 3]
[n×n + n×a] + -(n×a) =                   [Ax. 1]
[n×(n+a)] + -(n×a) =                     [Ax. 8]
[n×(n+a) + 0] + -(n×a) =                 [Ax. 2]
[n×(n+a) + (n×a + -(n×a))] + -(n×a) =    [Ax. 3]
[(n×(n+a) + n×a) + -(n×a)] + -(n×a) =    [Ax. 1]
[n×((n+a) + a) + -(n×a)] + -(n×a) =      [Ax. 8]
[n×((a+n) + a) + -(n×a)] + -(n×a) =      [Ax. 4]
[n×(0 + a) + -(n×a)] + -(n×a) =          [Ax. 3]
[n×(a + 0) + -(n×a)] + -(n×a) =          [Ax. 4]
[n×a + -(n×a)] + -(n×a) =                [Ax. 2]
[(n+0)×a + -(n×a)] + -(n×a) =            [Ax. 2]
[(0+n)×a + -(n×a)] + -(n×a) =            [Ax. 4]
[((a+n)+n)×a + -(n×a)] + -(n×a) =        [Ax. 3]
[((a+n)×a+n×a) + -(n×a)] + -(n×a) =      [Ax. 9]
[(a+n)×a+(n×a + -(n×a))] + -(n×a) =      [Ax. 1]
[(a+n)×a + 0] + -(n×a) =                 [Ax. 3]
[(a+n)×a] + -(n×a) =                     [Ax. 2]
[a×a+n×a] + -(n×a) =                     [Ax. 9]
a×a+[n×a + -(n×a)] =                     [Ax. 1]
a×a+0 =                                  [Ax. 3]
a×a                                      [Ax. 2]

@ H.PWiz, dlaczego nie możesz przejść od ndo 0 + njednego kroku? Czy to nie tylko A2? Reguły mówią, że zmienne mogą również
zastępować

@ jq170727 Axiom 2 stwierdza tylko, że a + 0 = anie to 0 + a = a. Musisz jeden dodatkowy krok przemienności dostać od ndo 0 + n.
Sriotchilism O'Zaic

@ H.PWiz nie umiesz odczytać aksjomatu w odwrotnej kolejności?
jq170727

1
@ jq170727 Nie, nie musisz do tego używać komutatywności.
Jalil Compaoré

4

304 kroki

Społeczność wiki, ponieważ ten dowód jest generowany przez funkcję FindEquationalProof firmy Mathematica .

Dowód jest dość długi. Mathematica nie umie grać w golfa.

Jest to kod Mathematica który generuje dowód (wymaga Mathematica 11.3), w której p, t, noznacza +, ×, -odpowiednio:

ringAxioms = {ForAll[{a, b, c}, p[a, p[b, c]] == p[p[a, b], c]],
   ForAll[a, p[a, 0] == a],
   ForAll[a, p[a, n[a]] == 0],
   ForAll[{a, b}, p[a, b] == p[b, a]],
   ForAll[{a, b, c}, t[a, t[b, c]] == t[t[a, b], c]],
   ForAll[a, t[a, 1] == a], ForAll[a, t[1, a] == a],
   ForAll[{a, b, c}, t[a, p[b, c]] == p[t[a, b], t[a, c]]],
   ForAll[{a, b, c}, t[p[b, c], a] == p[t[b, a], t[c, a]]]};

proof = FindEquationalProof[t[n[a], n[a]] == t[a, a], ringAxioms];

proof["ProofNotebook"]

Nie jest łatwo policzyć kroki bezpośrednio, więc obliczam je według liczby ścieżek od aksjomatów do wniosków na „wykresie dowodowym”.

graph = proof["ProofGraph"];
score = Sum[
  Length[FindPath[graph, axiom, "Conclusion 1", Infinity, 
    All]], {axiom, 
   Select[VertexList[graph], StringMatchQ["Axiom " ~~ __]]}]

Wypróbuj online!

Oto dowód wygenerowany przez kod:

Axiom 1

We are given that:

x1==p[x1, 0]

Axiom 2

We are given that:

x1==t[x1, 1]

Axiom 3

We are given that:

x1==t[1, x1]

Axiom 4

We are given that:

p[x1, x2]==p[x2, x1]

Axiom 5

We are given that:

p[x1, p[x2, x3]]==p[p[x1, x2], x3]

Axiom 6

We are given that:

p[x1, n[x1]]==0

Axiom 7

We are given that:

p[t[x1, x2], t[x3, x2]]==t[p[x1, x3], x2]

Axiom 8

We are given that:

p[t[x1, x2], t[x1, x3]]==t[x1, p[x2, x3]]

Axiom 9

We are given that:

t[x1, t[x2, x3]]==t[t[x1, x2], x3]

Hypothesis 1

We would like to show that:

t[n[a], n[a]]==t[a, a]

Critical Pair Lemma 1

The following expressions are equivalent:

p[0, x1]==x1

Proof

Note that the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Axiom 4 and Axiom 1 respectively.

Critical Pair Lemma 2

The following expressions are equivalent:

p[x1, p[n[x1], x2]]==p[0, x2]

Proof

Note that the input for the rule:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Axiom 5 and Axiom 6 respectively.

Critical Pair Lemma 3

The following expressions are equivalent:

t[p[1, x1], x2]==p[x2, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x3_, x2_]]->t[p[x1, x3], x2]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[1, x1_]->x1

where these rules follow from Axiom 7 and Axiom 3 respectively.

Critical Pair Lemma 4

The following expressions are equivalent:

t[x1, p[1, x2]]==p[x1, t[x1, x2]]

Proof

Note that the input for the rule:

p[t[x1_, x2_], t[x1_, x3_]]->t[x1, p[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 1]->x1

where these rules follow from Axiom 8 and Axiom 2 respectively.

Critical Pair Lemma 5

The following expressions are equivalent:

t[p[1, x1], 0]==t[x1, 0]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

p[x1_, t[x2_, x1_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 6

The following expressions are equivalent:

t[0, 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, 0]->x1

where these rules follow from Critical Pair Lemma 5 and Axiom 1 respectively.

Substitution Lemma 1

It can be shown that:

t[0, 0]==0

Proof

We start by taking Critical Pair Lemma 6, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 7

The following expressions are equivalent:

t[x1, 0]==t[p[x1, 1], 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 5 and Axiom 4 respectively.

Critical Pair Lemma 8

The following expressions are equivalent:

t[0, p[1, x1]]==t[0, x1]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

p[x1_, t[x1_, x2_]]

which can be unified with the input for the rule:

p[0, x1_]->x1

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 1 respectively.

Critical Pair Lemma 9

The following expressions are equivalent:

t[p[x1, 1], p[1, 0]]==p[p[x1, 1], t[x1, 0]]

Proof

Note that the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[p[x1_, 1], 0]->t[x1, 0]

where these rules follow from Critical Pair Lemma 4 and Critical Pair Lemma 7 respectively.

Substitution Lemma 2

It can be shown that:

t[p[x1, 1], 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Critical Pair Lemma 9, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 3

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[x1, 0]]

Proof

We start by taking Substitution Lemma 2, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Substitution Lemma 4

It can be shown that:

p[x1, 1]==p[x1, p[1, t[x1, 0]]]

Proof

We start by taking Substitution Lemma 3, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Critical Pair Lemma 10

The following expressions are equivalent:

t[0, x1]==t[0, p[x1, 1]]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[x1_, x2_]\[TwoWayRule]p[x2_, x1_]

where these rules follow from Critical Pair Lemma 8 and Axiom 4 respectively.

Critical Pair Lemma 11

The following expressions are equivalent:

t[p[1, 0], p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

Note that the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

contains a subpattern of the form:

t[x2_, x1_]

which can be unified with the input for the rule:

t[0, p[x1_, 1]]->t[0, x1]

where these rules follow from Critical Pair Lemma 3 and Critical Pair Lemma 10 respectively.

Substitution Lemma 5

It can be shown that:

t[1, p[x1, 1]]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Critical Pair Lemma 11, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Substitution Lemma 6

It can be shown that:

p[x1, 1]==p[p[x1, 1], t[0, x1]]

Proof

We start by taking Substitution Lemma 5, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Substitution Lemma 7

It can be shown that:

p[x1, 1]==p[x1, p[1, t[0, x1]]]

Proof

We start by taking Substitution Lemma 6, and apply the substitution:

p[p[x1_, x2_], x3_]->p[x1, p[x2, x3]]

which follows from Axiom 5.

Substitution Lemma 8

It can be shown that:

p[x1, p[n[x1], x2]]==x2

Proof

We start by taking Critical Pair Lemma 2, and apply the substitution:

p[0, x1_]->x1

which follows from Critical Pair Lemma 1.

Critical Pair Lemma 12

The following expressions are equivalent:

n[n[x1]]==p[x1, 0]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

p[n[x1_], x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Substitution Lemma 8 and Axiom 6 respectively.

Substitution Lemma 9

It can be shown that:

n[n[x1]]==x1

Proof

We start by taking Critical Pair Lemma 12, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 13

The following expressions are equivalent:

x1==p[n[x2], p[x2, x1]]

Proof

Note that the input for the rule:

p[x1_, p[n[x1_], x2_]]->x2

contains a subpattern of the form:

n[x1_]

which can be unified with the input for the rule:

n[n[x1_]]->x1

where these rules follow from Substitution Lemma 8 and Substitution Lemma 9 respectively.

Critical Pair Lemma 14

The following expressions are equivalent:

t[x1, x2]==p[n[x2], t[p[1, x1], x2]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x2_, x1_]]->t[p[1, x2], x1]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 3 respectively.

Critical Pair Lemma 15

The following expressions are equivalent:

t[x1, x2]==p[n[x1], t[x1, p[1, x2]]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, t[x1_, x2_]]->t[x1, p[1, x2]]

where these rules follow from Critical Pair Lemma 13 and Critical Pair Lemma 4 respectively.

Critical Pair Lemma 16

The following expressions are equivalent:

p[1, t[x1, 0]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[x1_, 0]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 4 respectively.

Substitution Lemma 10

It can be shown that:

p[1, t[x1, 0]]==1

Proof

We start by taking Critical Pair Lemma 16, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 17

The following expressions are equivalent:

t[t[x1, 0], 0]==t[1, 0]

Proof

Note that the input for the rule:

t[p[1, x1_], 0]->t[x1, 0]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[x1_, 0]]->1

where these rules follow from Critical Pair Lemma 5 and Substitution Lemma 10 respectively.

Substitution Lemma 11

It can be shown that:

t[x1, t[0, 0]]==t[1, 0]

Proof

We start by taking Critical Pair Lemma 17, and apply the substitution:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

which follows from Axiom 9.

Substitution Lemma 12

It can be shown that:

t[x1, 0]==t[1, 0]

Proof

We start by taking Substitution Lemma 11, and apply the substitution:

t[0, 0]->0

which follows from Substitution Lemma 1.

Substitution Lemma 13

It can be shown that:

t[x1, 0]==0

Proof

We start by taking Substitution Lemma 12, and apply the substitution:

t[1, x1_]->x1

which follows from Axiom 3.

Critical Pair Lemma 18

The following expressions are equivalent:

t[x1, t[0, x2]]==t[0, x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[x1_, 0]->0

where these rules follow from Axiom 9 and Substitution Lemma 13 respectively.

Critical Pair Lemma 19

The following expressions are equivalent:

p[1, t[0, x1]]==p[n[x1], p[x1, 1]]

Proof

Note that the input for the rule:

p[n[x1_], p[x1_, x2_]]->x2

contains a subpattern of the form:

p[x1_, x2_]

which can be unified with the input for the rule:

p[x1_, p[1, t[0, x1_]]]->p[x1, 1]

where these rules follow from Critical Pair Lemma 13 and Substitution Lemma 7 respectively.

Substitution Lemma 14

It can be shown that:

p[1, t[0, x1]]==1

Proof

We start by taking Critical Pair Lemma 19, and apply the substitution:

p[n[x1_], p[x1_, x2_]]->x2

which follows from Critical Pair Lemma 13.

Critical Pair Lemma 20

The following expressions are equivalent:

t[0, t[0, x1]]==t[0, 1]

Proof

Note that the input for the rule:

t[0, p[1, x1_]]->t[0, x1]

contains a subpattern of the form:

p[1, x1_]

which can be unified with the input for the rule:

p[1, t[0, x1_]]->1

where these rules follow from Critical Pair Lemma 8 and Substitution Lemma 14 respectively.

Substitution Lemma 15

It can be shown that:

t[0, x1]==t[0, 1]

Proof

We start by taking Critical Pair Lemma 20, and apply the substitution:

t[x1_, t[0, x2_]]->t[0, x2]

which follows from Critical Pair Lemma 18.

Substitution Lemma 16

It can be shown that:

t[0, x1]==0

Proof

We start by taking Substitution Lemma 15, and apply the substitution:

t[x1_, 1]->x1

which follows from Axiom 2.

Critical Pair Lemma 21

The following expressions are equivalent:

t[n[1], x1]==p[n[x1], t[0, x1]]

Proof

Note that the input for the rule:

p[n[x1_], t[p[1, x2_], x1_]]->t[x2, x1]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 14 and Axiom 6 respectively.

Substitution Lemma 17

It can be shown that:

t[n[1], x1]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 21, and apply the substitution:

t[0, x1_]->0

which follows from Substitution Lemma 16.

Substitution Lemma 18

It can be shown that:

t[n[1], x1]==n[x1]

Proof

We start by taking Substitution Lemma 17, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 22

The following expressions are equivalent:

t[n[1], t[x1, x2]]==t[n[x1], x2]

Proof

Note that the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

contains a subpattern of the form:

t[x1_, x2_]

which can be unified with the input for the rule:

t[n[1], x1_]->n[x1]

where these rules follow from Axiom 9 and Substitution Lemma 18 respectively.

Substitution Lemma 19

It can be shown that:

n[t[x1, x2]]==t[n[x1], x2]

Proof

We start by taking Critical Pair Lemma 22, and apply the substitution:

t[n[1], x1_]->n[x1]

which follows from Substitution Lemma 18.

Critical Pair Lemma 23

The following expressions are equivalent:

t[x1, n[1]]==p[n[x1], t[x1, 0]]

Proof

Note that the input for the rule:

p[n[x1_], t[x1_, p[1, x2_]]]->t[x1, x2]

contains a subpattern of the form:

p[1, x2_]

which can be unified with the input for the rule:

p[x1_, n[x1_]]->0

where these rules follow from Critical Pair Lemma 15 and Axiom 6 respectively.

Substitution Lemma 20

It can be shown that:

t[x1, n[1]]==p[n[x1], 0]

Proof

We start by taking Critical Pair Lemma 23, and apply the substitution:

t[x1_, 0]->0

which follows from Substitution Lemma 13.

Substitution Lemma 21

It can be shown that:

t[x1, n[1]]==n[x1]

Proof

We start by taking Substitution Lemma 20, and apply the substitution:

p[x1_, 0]->x1

which follows from Axiom 1.

Critical Pair Lemma 24

The following expressions are equivalent:

n[t[x1, x2]]==t[x1, t[x2, n[1]]]

Proof

Note that the input for the rule:

t[x1_, n[1]]->n[x1]

contains a subpattern of the form:

t[x1_, n[1]]

which can be unified with the input for the rule:

t[t[x1_, x2_], x3_]->t[x1, t[x2, x3]]

where these rules follow from Substitution Lemma 21 and Axiom 9 respectively.

Substitution Lemma 22

It can be shown that:

t[n[x1], x2]==t[x1, t[x2, n[1]]]

Proof

We start by taking Critical Pair Lemma 24, and apply the substitution:

n[t[x1_, x2_]]->t[n[x1], x2]

which follows from Substitution Lemma 19.

Substitution Lemma 23

It can be shown that:

t[n[x1], x2]==t[x1, n[x2]]

Proof

We start by taking Substitution Lemma 22, and apply the substitution:

t[x1_, n[1]]->n[x1]

which follows from Substitution Lemma 21.

Substitution Lemma 24

It can be shown that:

t[a, n[n[a]]]==t[a, a]

Proof

We start by taking Hypothesis 1, and apply the substitution:

t[n[x1_], x2_]->t[x1, n[x2]]

which follows from Substitution Lemma 23.

Conclusion 1

We obtain the conclusion:

True

Proof

Take Substitution Lemma 24, and apply the substitution:

n[n[x1_]]->x1

which follows from Substitution Lemma 9.
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.