Logiweb diagnose of frozen

Up Help

Error in proof of H1 Metageneralization over metavariable that occurs free in some premise: ∀\underline{a}: ∀\underline{\underline{a}}: ∀\underline{\underline{b}}: Neg^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{a}} @ \underline{\underline{b}} @ frozen @ ¬\underline{a} ⇒ ¬¬\underline{a} ⇒ ¬\underline{a} ⇒ ¬\underline{a} ⇒ \underline{a}^{⊳} ^{⊳} ; ∀\underline{\underline{a}}: Repetition^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{a}} @ ¬\underline{a} ⇒ ¬\underline{a}^{⊳} ; ∀\underline{\underline{a}}: ∀\underline{\underline{b}}: ∀\underline{\underline{c}}: H0b^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{a}} @ \underline{\underline{b}} @ \underline{\underline{c}} @ ¬\underline{a} ⇒ ¬¬\underline{a} @ ¬\underline{a} ⇒ ¬\underline{a} @ \underline{a}^{⊳} ^{⊳} ; ∀\underline{\underline{a}}: ∀\underline{\underline{b}}: A1′^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{a}} @ \underline{\underline{b}} @ ¬¬\underline{a} @ ¬\underline{a}; ∀\underline{\underline{a}}: ∀\underline{\underline{b}}: ∀\underline{\underline{c}}: H0a^{I}^{⊳} ^{∗}^{⊳} @ \underline{\underline{a}} @ \underline{\underline{b}} @ \underline{\underline{c}} @ ¬¬\underline{a} @ ¬\underline{a} ⇒ ¬¬\underline{a} @ \underline{a}^{⊳} ^{⊳}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-26.UTC:09:52:11.033905 = MJD-53912.TAI:09:52:44.033905 = LGT-4658032364033905e-6