X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fxml%2Fnuprl_stylesheets%2Fnuprl_mmlextension.xsl;fp=helm%2Fxml%2Fnuprl_stylesheets%2Fnuprl_mmlextension.xsl;h=f6c1590dfacc047dbb94b0df0a68677b93d226ae;hb=9a9c95ebabbb1d4d7dce627ed1baea130ea98766;hp=0000000000000000000000000000000000000000;hpb=76ad23ea1e83e8c187a4593027e9baed1bb022e3;p=helm.git diff --git a/helm/xml/nuprl_stylesheets/nuprl_mmlextension.xsl b/helm/xml/nuprl_stylesheets/nuprl_mmlextension.xsl new file mode 100644 index 000000000..f6c1590df --- /dev/null +++ b/helm/xml/nuprl_stylesheets/nuprl_mmlextension.xsl @@ -0,0 +1,3046 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Sequent + + + + + + + + + + + + + + ) + + __ + + + : + + + + + + + + + + + + |- + + + + + + + + + + + Rule: + + + + + + NESSUNA REGOLA + + + + + + + + + + + + + + + + + + + + Sequent + + + + + + + + + + + + + + ) + + __ + + + : + + + + + + + + + + + + |- + + + + + + + + + + + Rule: + + + + + + NESSUNA REGOLA + + + + + + + + + + + + + + + Subgoal + + + Subgoals + + + + + + + + + + + + + + + + + + + + + + + + + + + + := + + + + + + + + + + + + + + DEFINITION () OF TYPE + + + + + + + __ + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + AXIOM () OF TYPE + + + + + + + __ + + + + + + + + + + + + + + + + + UNFINISHED PROOF () + + + + + + + THESIS: + + + + + + + __ + + + + + + + + CONJECTURES: + + + + + + + + __ + + + + + + + + + + _ + + + : + + + + + + + + + + + _ + + + := + + + + + + _ + :? + _ + + + + + ; + + + |- + ? + : + + + + + + + + + PROOF: + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + INDUCTIVE DEFINITION + + + COINDUCTIVE DEFINITION + + + + + AND + + + _ + () + + + + + + + __ + [ + + + + + + + + + : + + + + + + + + + ] + + + + + + + ] + + + + + + + + + OF ARITY + + + + + + + __ + + + + + + + + BUILT FROM + + + + + + + + + + __ + + + | + _ + + + OF + _ + + + + + + + + + + + + + + + + + + + VARIABLE OF TYPE + + + + + + + __ + + + + + + + + + AS + + + + + + + __ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + + + + + + + + + + + + ⇒ + + + + + + + + + ⇒ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ∀ + + + + + + + + . + + + + + + + + ∀ + + : + + . + + + + + + + + + + + + + LET + _ + + + + + + + + = + + + + + + + + IN + _ + + + + + + + + LET + _ + + = + + _ + IN + _ + + + + + + + + + + + + + Π + + + + + + + + . + + + + + + + + Π + + : + + . + + + + + + + + + + + + + + ( + + + + + + + + + → + + + + + + + + + + + + + + + + + + + + + + + + ) + + + + + + + + + ( + + + → + + + + + + + + + + + + + + + + + + ) + + + + + + + + + + + + + + : + + + + + + + + + + + + + + + + : + + + + + + + + + + + + + + Σ + + : + + + + + + + + . + + + + + + + + + Σ + + : + + . + + + + + + + + + + + + + + ( + + + + + + + + x + + ) + + + + + + + + ( + + x + + ) + + + + + + + + + + + + + < + + , + + + + + + + + > + + + + + + + + < + + , + + > + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + inl( + + ) + + + + + + inr( + + ) + + + + + Ax + + + + Void + + + + Atom + + + + + U + + + + + + + P + + + + + + + + + + + + + + + + + = + + + + + + + + ∈ + + + + + + + + + + = + + ∈ + + + + + + + + + " + + " + + + + + [] + + + + + + + + + + + + + + + :: + + + + + + + + + + :: + + + + + + + + + + + + + + + rectype + + + + + + + + = + + + + + + + + + rectype + + = + + + + + + + + + + + + + + + { + + + + : + + + + + + + + + + + + + | + + } + + + + + + + + { + + + + : + + + + + + + | + + } + + + + + + + + + + + + + + Ç + + : + + + + + + + + . + + + + + + + + + Ç + + : + + . + + + + + + + + + + + + + + + , + + : + + + + + + + + // + + + + + + + + + + , + + : + + // + + + + + + + + + + + + + + + + atom_eq ( + + + int_eq ( + + + less ( + + + + ; + + + + + + + + ; + + + + + + + + ; + + + + + + + + ) + + + + + + + + + + atom_eq ( + + + int_eq ( + + + less ( + + + + ; + + ; + + ; + + ) + + + + + + + + + + + + + λ + + + + + + + + . + + + + + + + + + λ + + . + + + + + + + + + + + + + + ( + + + + + + + + + + + ( + + + + + + + + + + + ) + + + + + + +( + + + + + _ + + + + +) + + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + + + + + + + + ( + + + + + + + + + + + + ( + + + + + + + + + + + + ) + + + + + + + ( + + + + + + _ + + + + + + ) + + + + + + + + + + + + ( + + + + + + + + :> + + + + + + + + ) + + + + + + + ( + + :> + + ) + + + + + + + + + + + + + + + + + + + < + + + > + CASES + _ + + + + + + + + + + > + CASES + _ + + + + + + + + + OF + + + + + + + + + + + | + + + | + + + _ + + + ⇒ + + + + + + + + + + |_ + ⇒ + + + + + + + + + + END + + + + + + + <> + CASES + _ + + _ + OF + + + + | + + + + ⇒ + + + _ + END + + + + + + + + + + + + FIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + FIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + COFIX + _ + + { + + + + + + + __ + + + + + + + + : + + + + + + + + + + + := + + + + + + + + + := + + + + + + + + + + + + + } + + + + + + + COFIX + + { + + + + + + + : + + := + + + } + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We can prove + _ + + + + + _ + (explain) + + + + + + + + + + + + + + + + + + + + + _ + + + (hide details) + + + + + + + we proved + _ + + + + + + + + + + + + that is equivalent to + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + We prove + _ + + + + + + + + by induction on + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + Case + _ + + + + + + + + _ + + + + + + By induction hypothesis, we have: + + + + + + + _ + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + + _ + + : + + + ) + + + + + + + + + + + + + + + + + + Contradiction. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + ( + + ) + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + Rewrite + _ + + _ + with + _ + + _ + by + _ + + + + + + + + + + + + + + + + + + + + + Then apply it to + _ + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + In particular, we have + + + + + + + ( + + ) + _ + + + + + + + + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + We proceed by cases to prove + _ + + + + + + + + Left: suppose + _ + ( + + ) + _ + + + + + + + + _ + + + + + + + + Right: suppose + _ + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + We prove + _ + + _ + by cases: + + + + + + + Left + + + + + + + + Right + + + + + + + + + + + + + + + + + + Consider + _ + + + + + + + + + + Let + _ + + : + + _ + such that + _ + ( + + ) + _ + + + + + + + + + + + + + + + + + + + + We have the following equality chain: + + + + + + + + + + + + _ + = + + + = + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + We have the following disequality chain: + + + + + + + + + + + + _ + + + + + _ + + + + + + + + + + + __ + + + + + + + + + + + + + + + + [ + + + + + ← + + ] + + + + + + + + ↑ + + + + ( + + ) + + + + + + + + + ↑ + + + + + ( + + ) + + + + + + + + + + → + β + + + + + + + + + + + → + β + * + + + + + + + + + + + ⇒ + β + + + + + + + + + + + ⇒ + β + * + + + + + + + + + + + + + + + + + + + ≅ + + + + + + + + + + + + + + + ERROR + + + + + + + + + + + + + + + + + + + + + + + + λ + + + + + + + + + . + + + + + + + + λ + + + . + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +