:: On SCM+FSA Programs
:: by Andrzej Trybulec
::
:: Received May 19, 2013
:: Copyright (c) 2014-2021 Association of Mizar Users


definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA ;
func if=0 (a,I) -> Program of equals :: SCMFSA_X:def 1
(((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);
correctness
coherence
(((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;
;
end;

:: deftheorem defines if=0 SCMFSA_X:def 1 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds if=0 (a,I) = (((a =0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA ;
func if>0 (a,I) -> Program of equals :: SCMFSA_X:def 2
(((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);
correctness
coherence
(((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA) is Program of ;
;
end;

:: deftheorem defines if>0 SCMFSA_X:def 2 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds if>0 (a,I) = (((a >0_goto 3) ";" (Goto ((card I) + 1))) ";" I) ";" (Stop SCM+FSA);

Lm1: card (Stop SCM+FSA) = 1
by AFINSQ_1:34;

Lm2: (Stop SCM+FSA) . 0 = halt SCM+FSA
;

Lm3: 0 in dom (Stop SCM+FSA)
by COMPOS_1:3;

theorem Th1: :: SCMFSA_X:1
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (if=0 (a,I)) = (card I) + 4
proof end;

theorem Th2: :: SCMFSA_X:2
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (if>0 (a,I)) = (card I) + 4
proof end;

definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA ;
:: in these definitions 'Goto 0' is only a place holder
:: after relocation in changed to 'goto(card 3 + I)
:: and must be substituted by the real 'goto 0'
func while=0 (a,I) -> Program of equals :: SCMFSA_X:def 3
(if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));
correctness
coherence
(if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;
;
func while>0 (a,I) -> Program of equals :: SCMFSA_X:def 4
(if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));
correctness
coherence
(if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)) is Program of ;
;
end;

:: deftheorem defines while=0 SCMFSA_X:def 3 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds while=0 (a,I) = (if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

:: deftheorem defines while>0 SCMFSA_X:def 4 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds while>0 (a,I) = (if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0));

theorem Th3: :: SCMFSA_X:3
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (while=0 (a,I)) = (card I) + 5
proof end;

theorem Th4: :: SCMFSA_X:4
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (while>0 (a,I)) = (card I) + 5
proof end;

theorem Th5: :: SCMFSA_X:5
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
k in dom (while=0 (a,I))
proof end;

theorem Th6: :: SCMFSA_X:6
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
(card I) + k in dom (while=0 (a,I))
proof end;

theorem Th7: :: SCMFSA_X:7
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
k in dom (while>0 (a,I))
proof end;

theorem Th8: :: SCMFSA_X:8
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < 5 holds
(card I) + k in dom (while>0 (a,I))
proof end;

theorem :: SCMFSA_X:9
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds
( 1 in dom (while=0 (a,I)) & 1 in dom (while>0 (a,I)) ) by Th5, Th7;

theorem :: SCMFSA_X:10
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds
( (while=0 (a,I)) . 0 = a =0_goto 3 & (while=0 (a,I)) . 1 = goto 2 & (while>0 (a,I)) . 0 = a >0_goto 3 & (while>0 (a,I)) . 1 = goto 2 )
proof end;

theorem :: SCMFSA_X:11
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 4) = halt SCM+FSA
proof end;

theorem :: SCMFSA_X:12
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . 2 = goto ((card I) + 4)
proof end;

theorem :: SCMFSA_X:13
canceled;

::$CT
theorem :: SCMFSA_X:14
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < (card I) + 5 holds
k in dom (while=0 (a,I))
proof end;

theorem :: SCMFSA_X:15
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while=0 (a,I)) . ((card I) + 2) = goto 0
proof end;

theorem :: SCMFSA_X:16
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 4) = halt SCM+FSA
proof end;

theorem :: SCMFSA_X:17
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . 2 = goto ((card I) + 4)
proof end;

theorem :: SCMFSA_X:18
canceled;

::$CT
theorem :: SCMFSA_X:19
for a being Int-Location
for I being MacroInstruction of SCM+FSA
for k being Nat st k < (card I) + 5 holds
k in dom (while>0 (a,I))
proof end;

theorem :: SCMFSA_X:20
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 2) = goto 0
proof end;

definition
let a be Int-Location;
let I be Program of ;
func if<0 (a,I) -> Program of equals :: SCMFSA_X:def 5
((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);
coherence
((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA) is Program of ;
end;

:: deftheorem defines if<0 SCMFSA_X:def 5 :
for a being Int-Location
for I being Program of holds if<0 (a,I) = ((a =0_goto ((card I) + 4)) ";" ((a >0_goto ((card I) + 2)) ";" I)) ";" (Stop SCM+FSA);

theorem Th19: :: SCMFSA_X:21
for I being Program of
for a being Int-Location holds card (if<0 (a,I)) = (card I) + 5
proof end;

definition
let a be Int-Location;
let I be MacroInstruction of SCM+FSA ;
func while<0 (a,I) -> Program of equals :: SCMFSA_X:def 6
(if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));
correctness
coherence
(if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0)) is Program of ;
;
end;

:: deftheorem defines while<0 SCMFSA_X:def 6 :
for a being Int-Location
for I being MacroInstruction of SCM+FSA holds while<0 (a,I) = (if<0 (a,(I ';' (goto 0)))) +* (((card I) + 1),(goto 0));

theorem :: SCMFSA_X:22
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds card (while<0 (a,I)) = (card I) + 6
proof end;

theorem Th21: :: SCMFSA_X:23
for I being MacroInstruction of SCM+FSA
for i being No-StopCode Instruction of SCM+FSA
for n being Nat st n + 1 < card I holds
I +* (n,i) is MacroInstruction of SCM+FSA
proof end;

registration
let I be MacroInstruction of SCM+FSA ;
let a be Int-Location;
cluster while=0 (a,I) -> halt-ending unique-halt ;
coherence
( while=0 (a,I) is halt-ending & while=0 (a,I) is unique-halt )
proof end;
cluster while>0 (a,I) -> halt-ending unique-halt ;
coherence
( while>0 (a,I) is halt-ending & while>0 (a,I) is unique-halt )
proof end;
end;

theorem Th22: :: SCMFSA_X:24
for I being really-closed MacroInstruction of SCM+FSA
for n, k being Nat st n < card I & k < card I holds
I +* (n,(goto k)) is really-closed
proof end;

theorem Th23: :: SCMFSA_X:25
for I being really-closed MacroInstruction of SCM+FSA holds I ';' (goto 0) is really-closed
proof end;

theorem Th24: :: SCMFSA_X:26
for I being really-closed Program of
for k being Nat st k <= card I holds
(Macro (goto k)) ';' I is really-closed
proof end;

theorem Th25: :: SCMFSA_X:27
for I being really-closed MacroInstruction of SCM+FSA
for k being Nat st k <= card I holds
(Goto k) ";" I is really-closed
proof end;

theorem Th26: :: SCMFSA_X:28
for I being really-closed Program of holds ((Goto ((card I) + 1)) ";" I) ";" (Stop SCM+FSA) is really-closed
proof end;

theorem Th27: :: SCMFSA_X:29
for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(Macro (a =0_goto k)) ';' I is really-closed
proof end;

Lm4: for i being No-StopCode Instruction of SCM+FSA holds Directed (Macro i) = (Macro i) ';' (Goto 1)
proof end;

Lm5: for I being Program of
for k being Nat holds stop (I ';' (Goto k)) = I ';' (Macro (goto k))
proof end;

theorem Th28: :: SCMFSA_X:30
for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(Macro (a >0_goto k)) ';' I is really-closed
proof end;

theorem Th29: :: SCMFSA_X:31
for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(a =0_goto k) ";" I is really-closed
proof end;

theorem Th30: :: SCMFSA_X:32
for I being really-closed MacroInstruction of SCM+FSA
for a being Int-Location
for k being Nat st k <= card I holds
(a >0_goto k) ";" I is really-closed
proof end;

registration
let I be really-closed MacroInstruction of SCM+FSA ;
let a be Int-Location;
cluster if=0 (a,I) -> really-closed ;
coherence
if=0 (a,I) is really-closed
proof end;
cluster if>0 (a,I) -> really-closed ;
coherence
if>0 (a,I) is really-closed
proof end;
end;

registration
let I be really-closed MacroInstruction of SCM+FSA ;
let a be Int-Location;
cluster while=0 (a,I) -> really-closed ;
coherence
while=0 (a,I) is really-closed
proof end;
cluster while>0 (a,I) -> really-closed ;
coherence
while>0 (a,I) is really-closed
proof end;
end;

theorem :: SCMFSA_X:33
for I, J, K being MacroInstruction of SCM+FSA holds (I ";" J) ';' K = I ";" (J ';' K) by COMPOS_1:29;

theorem :: SCMFSA_X:34
for I being MacroInstruction of SCM+FSA holds stop (Directed I) = I ";" (Stop SCM+FSA) ;

theorem :: SCMFSA_X:35
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds if=0 (a,(I ';' (goto 0))) = ((((a =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA) by COMPOS_1:29;

theorem :: SCMFSA_X:36
for I being MacroInstruction of SCM+FSA
for a being Int-Location holds if>0 (a,(I ';' (goto 0))) = ((((a >0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" I) ';' (goto 0)) ";" (Stop SCM+FSA) by COMPOS_1:29;