Metamath

https://us.metamath.org/

Admin

Metamath is a simple, flexible, computer-processable language and proof assistant system designed...

Tokens:2,653,837

Snippets:47,556

Trust Score:8.8

Update:2 months ago

Show doc for...

Tokens:

Raw

### Install Metamath Site Mirror

Source: https://us.metamath.org/index.html

Execution command for the site installation script on Unix-like systems.

```bash
./install.sh
```

--------------------------------

### Completed Subproof Example

Source: https://us.metamath.org/other/completeusersproof/completeusersproof-read-me.txt

A completed subproof using the mpjaod metavariable deduction.

```text
  8:7:              |- (  (  Tr A /\ ( z e. y /\ y e. suc A ) )  ->  ( y e. A -> z e. suc A ) )
  ...
  ...
  12:11:            |- (             ( z e. y /\ y e. suc A )    ->  ( y = A -> z e. suc A ) )
  ...
  14:13:            |- (             ( z e. y /\ y e. suc A )    ->  ( y e. A \/ y = A ) )
  d3:12:adantl      |- (  (  Tr A /\ ( z e. y /\ y e. suc A ) )  ->  ( y = A -> z e. suc A ) )
  d4:14:adantl      |- (  (  Tr A /\ ( z e. y /\ y e. suc A ) )  ->  ( y e. A \/ y = A ) )
  15:8,d3,d4:mpjaod |- (  (  Tr A /\ ( z e. y /\ y e. suc A ) )  ->  z e. suc A )
```

--------------------------------

### Example Subproof of suctrALT4UP

Source: https://us.metamath.org/other/completeusersproof/completeusersproof-read-me.txt

The original form of the subproof for suctrALT4UP before unification theorem application.

```text
  8:7:                  |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. ( y e. A -> z e. suc A ) ).
  ...
  ...
  12:11:                |- (.            ( z e. y /\ y e. suc A )    ->. ( y = A -> z e. suc A ) ).
  ...
  14:13:                |- (.            ( z e. y /\ y e. suc A )    ->. ( y e. A \/ y = A ) ).
  15:8,12,14:           |- (. (. Tr A ,. ( z e. y /\ y e. suc A ) ). ->. z e. suc A ).
```

Tokens:

Raw