| vout |
|---|
PrQyi../48b90.. 5.31 barsTMTU9../dbb7f.. ownership of c6073.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMUXu../274f0.. ownership of 136a6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMLYb../93ba9.. ownership of e1ecf.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMJ2c../21860.. ownership of 295ea.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMUuy../792fb.. ownership of 913ca.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMVRz../5e8d0.. ownership of f6a7c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMYHA../03392.. ownership of be6eb.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMGH4../a1132.. ownership of 3644d.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMVfQ../0c3cd.. ownership of 9f9d1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMR6g../012a3.. ownership of 5ee0a.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMPrf../5f1b0.. ownership of 8aed1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMSi3../aecd6.. ownership of 1d4e9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMbPC../08480.. ownership of df932.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMYTD../d0b0d.. ownership of 1f104.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMa3S../d736a.. ownership of 6799e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMTSv../6d1be.. ownership of eae59.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMYAu../7f4bd.. ownership of 07080.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMasv../1a3ff.. ownership of 0cdc5.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMXTw../34853.. ownership of e4d70.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMcud../5c8c0.. ownership of 61b68.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TML9R../bbd45.. ownership of 76168.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMYLv../12b18.. ownership of 4329f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMZ9X../f0111.. ownership of 0ed40.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMbmY../b0a00.. ownership of 78e63.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMEhS../74a45.. ownership of 8dbd3.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMFp7../4e111.. ownership of 806a7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMR7j../14c93.. ownership of 36e27.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMLqv../22596.. ownership of 5a3c3.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMZ7B../c8ec0.. ownership of 8dc75.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMbcs../f8b18.. ownership of a257c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TML1B../4d0cb.. ownership of f3a4c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMKg3../ab08d.. ownership of f3a5c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMFHo../454ea.. ownership of 418c9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMFma../f7e7e.. ownership of 26856.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMN39../3cd51.. ownership of 8fef1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMGHp../fddec.. ownership of a9902.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMQcq../2768b.. ownership of efc7e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMEzg../1377d.. ownership of 96224.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMcMx../0e823.. ownership of 5ed8e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMJsa../2c767.. ownership of db5a6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMG4U../8d412.. ownership of ade95.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMYB7../32dbe.. ownership of a60a1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMW9L../beb12.. ownership of cc1e8.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMR6G../aae41.. ownership of 72bc1.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMGK7../35972.. ownership of b50f9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMLhA../3c415.. ownership of 99acd.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMMVH../5250b.. ownership of aec6c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMV8p../be4e6.. ownership of fc83f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMWLk../61c2c.. ownership of 0a04b.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMTFW../88345.. ownership of 4a3e7.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMNYi../7a3e2.. ownership of f1399.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMRby../83be7.. ownership of 74b7f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMKNm../45946.. ownership of 7f80f.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMZ1P../2db2a.. ownership of aa3d0.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMbB5../daeef.. ownership of ea5d0.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMHLF../37584.. ownership of a2a21.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMXpG../02497.. ownership of e5b9c.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMTvm../b6fbc.. ownership of 58ea6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMST2../d536e.. ownership of c7c61.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMTcm../1e388.. ownership of 06dd2.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMQ8e../fcc24.. ownership of 91ad9.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMN6y../b8f2f.. ownership of 9e278.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMXrZ../f9b2f.. ownership of 2e358.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMTGf../487ef.. ownership of 99e45.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMMTh../d50e4.. ownership of df3c6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMKmS../e5321.. ownership of 4332e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMNpN../a8d70.. ownership of 79b8d.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMZXP../b0104.. ownership of 168b8.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMaXX../48e38.. ownership of c1824.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMJz5../4a1da.. ownership of 6f381.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMPMF../2efcc.. ownership of 0e688.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMUXX../bb3f0.. ownership of 5c367.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMFxw../a0bd4.. ownership of 7aa0e.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMXZ7../dc871.. ownership of 30c12.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMF8o../f60f4.. ownership of f55c6.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMb4X../117be.. ownership of 14968.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMFqF../cc620.. ownership of fd9fb.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0TMH8e../e7b2d.. ownership of 6d71d.. as obj with payaddr Pr4zB.. rights free controlledby Pr4zB.. upto 0PUY9z../4bbf2.. doc published by Pr4zB..Param 87bb9.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οParam notnot : ο → οDefinition fd9fb.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (87bb9.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ x0 x4 x11 ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition f55c6.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (fd9fb.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ x0 x3 x12 ⟶ not (x0 x4 x12) ⟶ not (x0 x5 x12) ⟶ not (x0 x6 x12) ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Param f1c88.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 7aa0e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (f1c88.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 6f07c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 0e688.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (6f07c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition c1824.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (f1c88.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition 79b8d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (c1824.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ not (x0 x3 x12) ⟶ not (x0 x4 x12) ⟶ x0 x5 x12 ⟶ not (x0 x6 x12) ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Definition df3c6.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (f1c88.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition 2e358.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (df3c6.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ not (x0 x3 x12) ⟶ not (x0 x4 x12) ⟶ not (x0 x5 x12) ⟶ x0 x6 x12 ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Definition 91ad9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (df3c6.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ not (x0 x3 x12) ⟶ not (x0 x4 x12) ⟶ x0 x5 x12 ⟶ x0 x6 x12 ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Param d8b5d.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition c7c61.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (d8b5d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 55171.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition e5b9c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (55171.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 1465e.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition ea5d0.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (1465e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition 7f80f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (1465e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition f1399.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (1465e.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 97406.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 0a04b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (97406.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ x0 x4 x11 ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition aec6c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (97406.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ x0 x4 x11 ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 4b1cb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition b50f9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (4b1cb.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ x0 x4 x11 ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 6d791.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition cc1e8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (6d791.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ x0 x5 x11 ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition ade95.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (6f07c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ x0 x5 x11 ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 7c588.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 5ed8e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (7c588.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 133c1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition efc7e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (133c1.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ x0 x5 x11 ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 51ac7.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 8fef1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (51ac7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 15aa1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 418c9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (15aa1.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ not (x0 x3 x11) ⟶ x0 x4 x11 ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 7683c.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition f3a4c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (7683c.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 07f55.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 8dc75.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (07f55.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param e68b8.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 36e27.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (e68b8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 5bc1a.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 8dbd3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (5bc1a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ not (x0 x2 x11) ⟶ not (x0 x3 x11) ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 02f40.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 0ed40.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (02f40.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition 76168.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (5bc1a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ not (x0 x1 x11) ⟶ not (x0 x2 x11) ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition e4d70.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (76168.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ not (x0 x3 x12) ⟶ not (x0 x4 x12) ⟶ x0 x5 x12 ⟶ not (x0 x6 x12) ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Definition 07080.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 . ∀ x13 : ο . (76168.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ⟶ (x1 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x2 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x3 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x4 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x5 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x6 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x7 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x8 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x9 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x10 = x12 ⟶ ∀ x14 : ο . x14) ⟶ (x11 = x12 ⟶ ∀ x14 : ο . x14) ⟶ x0 x1 x12 ⟶ not (x0 x2 x12) ⟶ not (x0 x3 x12) ⟶ not (x0 x4 x12) ⟶ x0 x5 x12 ⟶ x0 x6 x12 ⟶ not (x0 x7 x12) ⟶ not (x0 x8 x12) ⟶ not (x0 x9 x12) ⟶ not (x0 x10 x12) ⟶ x0 x11 x12 ⟶ x13) ⟶ x13Definition 6799e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 . ∀ x14 : ο . (07080.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ⟶ (x1 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x2 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x3 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x4 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x5 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x6 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x7 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x8 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x9 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x10 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x11 = x13 ⟶ ∀ x15 : ο . x15) ⟶ (x12 = x13 ⟶ ∀ x15 : ο . x15) ⟶ x0 x1 x13 ⟶ x0 x2 x13 ⟶ not (x0 x3 x13) ⟶ x0 x4 x13 ⟶ not (x0 x5 x13) ⟶ not (x0 x6 x13) ⟶ not (x0 x7 x13) ⟶ not (x0 x8 x13) ⟶ not (x0 x9 x13) ⟶ not (x0 x10 x13) ⟶ x0 x11 x13 ⟶ not (x0 x12 x13) ⟶ x14) ⟶ x14Param b1def.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition df932.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (b1def.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Definition 8aed1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (5bc1a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 8befb.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 9f9d1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (8befb.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 3d118.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition be6eb.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (3d118.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 856bc.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition 913ca.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (856bc.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param 788a1.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition e1ecf.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (788a1.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12Param c9658.. : (ι → ι → ο) → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → οDefinition c6073.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (c9658.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ⟶ (x1 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x2 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x3 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x4 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x5 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x6 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x7 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x8 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x9 = x11 ⟶ ∀ x13 : ο . x13) ⟶ (x10 = x11 ⟶ ∀ x13 : ο . x13) ⟶ x0 x1 x11 ⟶ x0 x2 x11 ⟶ x0 x3 x11 ⟶ not (x0 x4 x11) ⟶ not (x0 x5 x11) ⟶ not (x0 x6 x11) ⟶ not (x0 x7 x11) ⟶ x0 x8 x11 ⟶ not (x0 x9 x11) ⟶ not (x0 x10 x11) ⟶ x12) ⟶ x12 |
|