digama0/dtt.mm

Metamath database for dependent type theory

dtt.mm's Issues

Errors in dtt.mm

If I read dtt.mm with metamath.exe, these errors appear:

Metamath - Version 0.199.pre 29-Jan-2022      Type HELP for help, EXIT to exit.
MM> set scroll continuous
Continuous scrolling is now in effect.
MM> read dtt.mm
Reading source file "dtt.mm"... 56485 bytes
56485 bytes were read into the source buffer.
The source has 548 statements; 93 are $a and 85 are $p.

?Error on line 593 of file "dtt.mm" at statement 242, label "kcd", type "$p":
    kcd $p |- ( ph |= MA B : MB B ) $=
    ^^^
This label is declared more than once.  All labels must be unique.

?Error on line 1291 of file "dtt.mm" at statement 520, label "kcd", type "$a":
  kcd $a |- cond i : \ x : Type i , ( two -> ( x -> ( x -> x ) ) ) $.
  ^^^
This label is declared more than once.  All labels must be unique.

?Error on line 1291 of file "dtt.mm" at statement 520, label "kcd", type "$a":
  kcd $a |- cond i : \ x : Type i , ( two -> ( x -> ( x -> x ) ) ) $.
                                      ^^^
This math symbol was not declared (with a "$c" or "$v" statement).

?Error on line 1291 of file "dtt.mm" at statement 520, label "kcd", type "$a":
  kcd $a |- cond i : \ x : Type i , ( two -> ( x -> ( x -> x ) ) ) $.
The variable "two" does not appear in an active "$f" statement.

?Error on line 1325 of file "dtt.mm" at statement 533, label "t1st", type "$a":
  t1st $a term 1st i j $.
               ^^^
This math symbol was not declared (with a "$c" or "$v" statement).

?Error on line 1325 of file "dtt.mm" at statement 533, label "t1st", type "$a":
  t1st $a term 1st i j $.
The variable "1st" does not appear in an active "$f" statement.

?Error on line 1329 of file "dtt.mm" at statement 534, label "t2nd", type "$a":
  t2nd $a term 2nd i j $.
               ^^^
This math symbol was not declared (with a "$c" or "$v" statement).

?Error on line 1329 of file "dtt.mm" at statement 534, label "t2nd", type "$a":
  t2nd $a term 2nd i j $.
The variable "2nd" does not appear in an active "$f" statement.

?Error on line 1342 of file "dtt.mm" at statement 537, label "k1st", type "$a":
  k1st $a |- 1st i j : \ x : Type i , \ y : ( x -> Type j ) ,
             ^^^
This math symbol was not declared (with a "$c" or "$v" statement).

?Error on line 1342 of file "dtt.mm" at statement 537, label "k1st", type "$a":
  k1st $a |- 1st i j : \ x : Type i , \ y : ( x -> Type j ) ,
The variable "1st" does not appear in an active "$f" statement.

?Error on line 1347 of file "dtt.mm" at statement 538, label "k2nd", type "$a":
  k2nd $a |- 2nd i j : \ x : Type i , \ y : ( x -> Type j ) ,
             ^^^
This math symbol was not declared (with a "$c" or "$v" statement).

?Error on line 1347 of file "dtt.mm" at statement 538, label "k2nd", type "$a":
  k2nd $a |- 2nd i j : \ x : Type i , \ y : ( x -> Type j ) ,
The variable "2nd" does not appear in an active "$f" statement.

12 errors were found.
MM>

If I verify the proofs these errors appear:

MM> verify proof *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
......................................
?Error on line 984 of file "dtt.mm" at statement 426, label "kim", type "$p":
      IJKUAUBMABCHNOABCDEHFAHPJKBQCDQGRST $.
                                       ^
There is a disjoint variable ($d) violation at proof step 44.  Assertion "kim1"
requires that variables "x" and "ph" be disjoint.  But "x" was substituted with
"x" and "ph" was substituted with "ph".
Variables "ph" and "x" do not have a disjoint variable requirement in the
assertion being proved, "kim".

?Error on line 984 of file "dtt.mm" at statement 426, label "kim", type "$p":
      IJKUAUBMABCHNOABCDEHFAHPJKBQCDQGRST $.
                                       ^
There is a disjoint variable ($d) violation at proof step 44.  Assertion "kim1"
requires that variables "x" and "OC" be disjoint.  But "x" was substituted with
"x" and "OC" was substituted with "OC".
Variables "OC" and "x" do not have a disjoint variable requirement in the
assertion being proved, "kim".
.
?Error on line 994 of file "dtt.mm" at statement 431, label "kcim", type "$p":
      ( vx mc om tim mt to ol wde df-im a1i bd desymd kdetrd lde1d detrd kcd wk
                                                                         ^^^
The label "kcd" at proof step 16 is the label of a future statement (at line
1291 in file dtt.mm).  Only previous statements may be referenced.
.....
?Error on line 1151 of file "dtt.mm" at statement 483, label "tyld", type "$p":
      FOIJKLGABCUASDGHPBTEFQR $.
                      ^
There is a disjoint variable ($d) violation at proof step 38.  Assertion "kim1"
requires that variables "x" and "ph" be disjoint.  But "x" was substituted with
"x" and "ph" was substituted with "ph".
Variables "ph" and "x" do not have a disjoint variable requirement in the
assertion being proved, "tyld".

?Error on line 1151 of file "dtt.mm" at statement 483, label "tyld", type "$p":
      FOIJKLGABCUASDGHPBTEFQR $.
                      ^
There is a disjoint variable ($d) violation at proof step 38.  Assertion "kim1"
requires that variables "x" and "OA" be disjoint.  But "x" was substituted with
"x" and "OA" was substituted with "OA".
Variables "OA" and "x" do not have a disjoint variable requirement in the
assertion being proved, "tyld".

?Error on line 1151 of file "dtt.mm" at statement 483, label "tyld", type "$p":
      FOIJKLGABCUASDGHPBTEFQR $.
                      ^
There is a disjoint variable ($d) violation at proof step 38.  Assertion "kim1"
requires that variables "x" and "OC" be disjoint.  But "x" was substituted with
"x" and "OC" was substituted with "Type j".
Variables "j" and "x" do not have a disjoint variable requirement in the
assertion being proved, "tyld".
.
?Error on line 1210 of file "dtt.mm" at statement 500, label "0val", type "$p":
    wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM
                                     ^
At proof step 3, statement "ol" requires 3 hypotheses but the RPN stack
contains only 2 entries: "A" (step 1) and  "B" (step 2).
.
?Error on line 1244 of file "dtt.mm" at statement 507, label "k1s", type "$p":
    wk wa tyld tyde mp2an detr4i ) ABCDHEIJZKLMZNLMZABCDEIFADOLMBUCUDZCUKIKLM
                                   ^
At proof step 1, statement "ol" requires 3 hypotheses but the RPN stack is
empty.

?Error on line 1261 of file "dtt.mm" at statement 512, label "de1s", type "$p":
      ZGUKUMPULQRSUEUJUKPAUJUMUKUIITIUITUJUMPEUAUIUBUIIUFUGQUHRS $.
          ^^
This compressed label reference is outside the range of the label list.  The
compressed label value is 32 but the largest label defined is 31.
....
Warning: The following $p statement(s) were not proved:  k1r, kpaird
MM>