c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../propositional/soundness/prop.elf".

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../proof_theory/sfol.elf".

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../model_theory/sfol.elf".

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "sifol.elf".

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundSFOL : SFOLPF -> SFOLMOD = {

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBaseSFOL.

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundSIFOL.

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundTND.

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder non_empty_universe := [S : Sort]

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder exists1 (existsE non_empty_universe ([x : Term S][p] existsI x true1)).

c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder}.

239352d9aec4bc3823511873533fa812cbe259c7Kristina Sojakova