digama0
commented
1 year ago There is a ? proof at line 1251, so you can safely assume that anything after that has not been reviewed for correctness. This file is more or less unmaintained, but I will accept PRs that fix things up.
If I read
dtt.mmwith 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>